[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
s : Set α
l : Filter α
a : α
t✝ : Set α
l' : Filter α
t : Set δ
g : δ → α
b : δ
hf : IsMinOn f s a
hg : MapsTo g t s
ha : g b = a
y : δ
hy : y ∈ t
⊢ y ∈ {x | (fun x => (f ∘ g) b ≤ (f ∘ g) x) x}
[PROOFSTEP]
simpa only [ha, (· ∘ ·)] using hf (hg hy)
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
l : Filter α
hf : IsMinFilter f l a
hg : IsMaxFilter g l a
⊢ IsMinFilter (fun x => f x - g x) l a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMinFilter g l a
⊢ IsMaxFilter (fun x => f x - g x) l a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
l : Filter α
hf : IsMinOn f s a
hg : IsMaxOn g s a
⊢ IsMinOn (fun x => f x - g x) s a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
l : Filter α
hf : IsMaxOn f s a
hg : IsMinOn g s a
⊢ IsMaxOn (fun x => f x - g x) s a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
⊢ IsMaxFilter g l a
[PROOFSTEP]
refine' hle.mp (h.mono fun x hf hgf => _)
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ g a
[PROOFSTEP]
rw [← hfga]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ f a
[PROOFSTEP]
exact le_trans hgf hf
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
h : IsExtrFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsExtrFilter g l a
[PROOFSTEP]
rw [IsExtrFilter] at *
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
h : IsMinFilter f l a ∨ IsMaxFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMinFilter g l a ∨ IsMaxFilter g l a
[PROOFSTEP]
rwa [← heq.isMaxFilter_iff hfga, ← heq.isMinFilter_iff hfga]
