awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : Preorder β
inst_1 : Preorder γ
f : α → β
l : Filter α
a : α
inst_2 : Preorder δ
op : β → γ → δ
hop : ((fun (x1 x2 : β) ↦ x1 ≤ x2) ⇒ (fun (x1 x2 : γ) ↦ x1 ≤ x2) ⇒ fun (x1 x2 : δ) ↦ x1 ≤ x2) op op
hf : IsMinFilter f l a
g : α → γ
hg : IsMinFilter g l a
⊢ IsMinFilter.{u, x} (β := δ) (fun (x : α) ↦ op (f x) (g x)) l a

Tactic:
mem_of_superset (inter_mem hf hg) fun _x ⟨hfx, hgx⟩ => hop hfx hgx

Premises used: Filter.Eventually, Filter.inter_mem, _private.0.IsMinFilter.bicomp_mono.match_1, setOf, IsMinFilter, Membership.mem, LE.le, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : Preorder β
inst_1 : Preorder γ
f : α → β
l : Filter α
a : α
inst_2 : Preorder δ
op : β → γ → δ
hop : ((fun (x1 x2 : β) ↦ x1 ≤ x2) ⇒ (fun (x1 x2 : γ) ↦ x1 ≤ x2) ⇒ fun (x1 x2 : δ) ↦ x1 ≤ x2) op op
hf : IsMaxFilter f l a
g : α → γ
hg : IsMaxFilter g l a
⊢ IsMaxFilter.{u, x} (β := δ) (fun (x : α) ↦ op (f x) (g x)) l a

Tactic:
mem_of_superset (inter_mem hf hg) fun _x ⟨hfx, hgx⟩ => hop hfx hgx

Premises used: Filter.Eventually, Filter.inter_mem, setOf, Membership.mem, LE.le, _private.0.IsMaxFilter.bicomp_mono.match_1, IsMaxFilter, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : Preorder β
inst_1 : Preorder γ
f : α → β
s : Set α
a : α
inst_2 : Preorder δ
op : β → γ → δ
hop : ((fun (x1 x2 : β) ↦ x1 ≤ x2) ⇒ (fun (x1 x2 : γ) ↦ x1 ≤ x2) ⇒ fun (x1 x2 : δ) ↦ x1 ≤ x2) op op
hf : IsMinOn f s a
g : α → γ
hg : IsMinOn g s a
⊢ IsMinOn.{u, x} (β := δ) (fun (x : α) ↦ op (f x) (g x)) s a

Tactic:
IsMinFilter.bicomp_mono hop hf hg

Premises used: IsMinFilter.bicomp_mono, IsMinOn
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : Preorder β
inst_1 : Preorder γ
f : α → β
s : Set α
a : α
inst_2 : Preorder δ
op : β → γ → δ
hop : ((fun (x1 x2 : β) ↦ x1 ≤ x2) ⇒ (fun (x1 x2 : γ) ↦ x1 ≤ x2) ⇒ fun (x1 x2 : δ) ↦ x1 ≤ x2) op op
hf : IsMaxOn f s a
g : α → γ
hg : IsMaxOn g s a
⊢ IsMaxOn.{u, x} (β := δ) (fun (x : α) ↦ op (f x) (g x)) s a

Tactic:
IsMaxFilter.bicomp_mono hop hf hg

Premises used: IsMaxOn, IsMaxFilter.bicomp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
δ : Type x
inst : Preorder β
f : α → β
l : Filter α
g : δ → α
l' : Filter δ
b : δ
hf : IsMinFilter f l (g b)
hg : Tendsto g l' l
⊢ IsMinFilter (f ∘ g) l' b

Tactic:
hg hf

Premises used: Set.Mem, Filter.Eventually, setOf, IsMinFilter, Set.preimage
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
δ : Type x
inst : Preorder β
f : α → β
l : Filter α
g : δ → α
l' : Filter δ
b : δ
hf : IsMaxFilter f l (g b)
hg : Tendsto g l' l
⊢ IsMaxFilter (f ∘ g) l' b

Tactic:
hg hf

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
δ : Type x
inst : Preorder β
f : α → β
l : Filter α
g : δ → α
l' : Filter δ
b : δ
hf : IsExtrFilter f l (g b)
hg : Tendsto g l' l
⊢ IsExtrFilter (f ∘ g) l' b

Tactic:
hf.elim (fun hf => (hf.comp_tendsto hg).isExtr) fun hf => (hf.comp_tendsto hg).isExtr

Premises used: IsMinFilter.comp_tendsto, IsMinFilter.isExtr, IsMaxFilter.isExtr, Or.elim, IsMaxFilter.comp_tendsto
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
δ : Type x
inst : Preorder β
f : α → β
s : Set α
g : δ → α
b : δ
hf : IsMinOn f s (g b)
⊢ IsMinOn (f ∘ g) (g ⁻¹' s) b

Tactic:
hf.comp_tendsto (tendsto_principal_principal.mpr <| Subset.refl _)

Premises used: Iff.mpr, Set.Subset.refl, IsMinFilter.comp_tendsto, IsMinOn, Filter.tendsto_principal_principal
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
δ : Type x
inst : Preorder β
f : α → β
s : Set α
g : δ → α
b : δ
hf : IsMaxOn f s (g b)
⊢ IsMaxOn (f ∘ g) (g ⁻¹' s) b

Tactic:
hf.comp_tendsto (tendsto_principal_principal.mpr <| Subset.refl _)

Premises used: Iff.mpr, Set.Subset.refl, IsMaxOn, IsMaxFilter.comp_tendsto, Filter.tendsto_principal_principal
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
δ : Type x
inst : Preorder β
f : α → β
s : Set α
g : δ → α
b : δ
hf : IsExtrOn f s (g b)
⊢ IsExtrOn (f ∘ g) (g ⁻¹' s) b

Tactic:
hf.elim (fun hf => (hf.on_preimage g).isExtr) fun hf => (hf.on_preimage g).isExtr

Premises used: IsMaxOn.isExtr, IsMaxOn.on_preimage, IsMinOn.isExtr, IsExtrOn.elim, IsMinOn.on_preimage
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
δ : Type x
inst : Preorder β
f : α → β
s : Set α
a : α
t : Set δ
g : δ → α
b : δ
hf : IsMinOn f s a
hg : MapsTo g t s
ha : g b = a
y : δ
hy : y ∈ t
⊢ Membership.mem (γ := Set δ) {x : δ | (fun (x : δ) ↦ (f ∘ g) b ≤ (f ∘ g) x) x} y

Tactic:
simpa only [ha, (· ∘ ·)] using hf (hg hy)

Premises used: Function.comp
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
δ : Type x
inst : Preorder β
f : α → β
s : Set α
a : α
t : Set δ
g : δ → α
b : δ
hf : IsMaxOn f s a
hg : MapsTo g t s
ha : g b = a
⊢ IsMaxOn (f ∘ g) t b

Tactic:
hf.dual.comp_mapsTo hg ha

Premises used: IsMinOn.comp_mapsTo, IsMaxOn, IsMaxOn.dual, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
δ : Type x
inst : Preorder β
f : α → β
s : Set α
a : α
t : Set δ
g : δ → α
b : δ
hf : IsExtrOn f s a
hg : MapsTo g t s
ha : g b = a
⊢ IsExtrOn (f ∘ g) t b

Tactic:
hf.elim (fun h => Or.inl <| h.comp_mapsTo hg ha) fun h => Or.inr <| h.comp_mapsTo hg ha

Premises used: IsMinOn.comp_mapsTo, IsMaxOn.comp_mapsTo, IsExtrOn.elim, Or.inl, Or.inr
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommMonoid β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMinFilter g l a
⊢ IsMinFilter.{u, v} (β := β) (fun (x : α) ↦ f x + g x) l a

Tactic:
show IsMinFilter (fun x => f x + g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => add_le_add hx hy) hg

Premises used: add_le_add, IsMinFilter.bicomp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommMonoid β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMaxFilter g l a
⊢ IsMaxFilter.{u, v} (β := β) (fun (x : α) ↦ f x + g x) l a

Tactic:
show IsMaxFilter (fun x => f x + g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => add_le_add hx hy) hg

Premises used: add_le_add, IsMaxFilter.bicomp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommMonoid β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMinOn g s a
⊢ IsMinOn.{u, v} (β := β) (fun (x : α) ↦ f x + g x) s a

Tactic:
IsMinFilter.add hf hg

Premises used: IsMinFilter.add, IsMinOn
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommMonoid β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMaxOn g s a
⊢ IsMaxOn.{u, v} (β := β) (fun (x : α) ↦ f x + g x) s a

Tactic:
IsMaxFilter.add hf hg

Premises used: IsMaxOn, IsMaxFilter.add
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
⊢ IsMaxFilter.{u, v} (β := β) (fun (x : α) ↦ -f x) l a

Tactic:
hf.comp_antitone fun _x _y hx => neg_le_neg hx

Premises used: IsMinFilter.comp_antitone, neg_le_neg
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
⊢ IsMinFilter.{u, v} (β := β) (fun (x : α) ↦ -f x) l a

Tactic:
hf.comp_antitone fun _x _y hx => neg_le_neg hx

Premises used: IsMaxFilter.comp_antitone, neg_le_neg
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f : α → β
a : α
l : Filter α
hf : IsExtrFilter f l a
⊢ IsExtrFilter.{u, v} (β := β) (fun (x : α) ↦ -f x) l a

Tactic:
hf.elim (fun hf => hf.neg.isExtr) fun hf => hf.neg.isExtr

Premises used: IsMaxFilter.neg, IsMinFilter.neg, IsMinFilter.isExtr, IsMaxFilter.isExtr, Or.elim
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f : α → β
a : α
s : Set α
hf : IsMinOn f s a
⊢ IsMaxOn.{u, v} (β := β) (fun (x : α) ↦ -f x) s a

Tactic:
hf.comp_antitone fun _x _y hx => neg_le_neg hx

Premises used: IsMinOn.comp_antitone, neg_le_neg
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f : α → β
a : α
s : Set α
hf : IsMaxOn f s a
⊢ IsMinOn.{u, v} (β := β) (fun (x : α) ↦ -f x) s a

Tactic:
hf.comp_antitone fun _x _y hx => neg_le_neg hx

Premises used: IsMaxOn.comp_antitone, neg_le_neg
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f : α → β
a : α
s : Set α
hf : IsExtrOn f s a
⊢ IsExtrOn.{u, v} (β := β) (fun (x : α) ↦ -f x) s a

Tactic:
hf.elim (fun hf => hf.neg.isExtr) fun hf => hf.neg.isExtr

Premises used: IsMaxOn.isExtr, IsMinOn.isExtr, IsMaxOn.neg, IsExtrOn.elim, IsMinOn.neg
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMaxFilter g l a
⊢ IsMinFilter.{u, v} (β := β) (fun (x : α) ↦ f x - g x) l a

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: IsMinFilter.add, sub_eq_add_neg, IsMaxFilter.neg
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMinFilter g l a
⊢ IsMaxFilter.{u, v} (β := β) (fun (x : α) ↦ f x - g x) l a

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: IsMaxFilter.add, sub_eq_add_neg, IsMinFilter.neg
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMaxOn g s a
⊢ IsMinOn.{u, v} (β := β) (fun (x : α) ↦ f x - g x) s a

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: sub_eq_add_neg, IsMaxOn.neg, IsMinOn.add
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMinOn g s a
⊢ IsMaxOn.{u, v} (β := β) (fun (x : α) ↦ f x - g x) s a

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: sub_eq_add_neg, IsMaxOn.add, IsMinOn.neg
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMinFilter g l a
⊢ IsMinFilter.{u, v} (β := β) (fun (x : α) ↦ f x ⊔ g x) l a

Tactic:
show IsMinFilter (fun x => f x ⊔ g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => sup_le_sup hx hy) hg

Premises used: sup_le_sup, IsMinFilter.bicomp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMaxFilter g l a
⊢ IsMaxFilter.{u, v} (β := β) (fun (x : α) ↦ f x ⊔ g x) l a

Tactic:
show IsMaxFilter (fun x => f x ⊔ g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => sup_le_sup hx hy) hg

Premises used: sup_le_sup, IsMaxFilter.bicomp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMinOn g s a
⊢ IsMinOn.{u, v} (β := β) (fun (x : α) ↦ f x ⊔ g x) s a

Tactic:
IsMinFilter.sup hf hg

Premises used: IsMinFilter.sup, IsMinOn
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMaxOn g s a
⊢ IsMaxOn.{u, v} (β := β) (fun (x : α) ↦ f x ⊔ g x) s a

Tactic:
IsMaxFilter.sup hf hg

Premises used: IsMaxOn, IsMaxFilter.sup
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeInf β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMinFilter g l a
⊢ IsMinFilter.{u, v} (β := β) (fun (x : α) ↦ f x ⊓ g x) l a

Tactic:
show IsMinFilter (fun x => f x ⊓ g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => inf_le_inf hx hy) hg

Premises used: inf_le_inf, IsMinFilter.bicomp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeInf β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMaxFilter g l a
⊢ IsMaxFilter.{u, v} (β := β) (fun (x : α) ↦ f x ⊓ g x) l a

Tactic:
show IsMaxFilter (fun x => f x ⊓ g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => inf_le_inf hx hy) hg

Premises used: inf_le_inf, IsMaxFilter.bicomp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeInf β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMinOn g s a
⊢ IsMinOn.{u, v} (β := β) (fun (x : α) ↦ f x ⊓ g x) s a

Tactic:
IsMinFilter.inf hf hg

Premises used: IsMinFilter.inf, IsMinOn
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeInf β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMaxOn g s a
⊢ IsMaxOn.{u, v} (β := β) (fun (x : α) ↦ f x ⊓ g x) s a

Tactic:
IsMaxFilter.inf hf hg

Premises used: IsMaxOn, IsMaxFilter.inf
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : LinearOrder β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMinFilter g l a
⊢ IsMinFilter.{u, v} (β := β) (fun (x : α) ↦ Min.min (f x) (g x)) l a

Tactic:
show IsMinFilter (fun x => Min.min (f x) (g x)) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => min_le_min hx hy) hg

Premises used: IsMinFilter.bicomp_mono, min_le_min
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : LinearOrder β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMaxFilter g l a
⊢ IsMaxFilter.{u, v} (β := β) (fun (x : α) ↦ Min.min (f x) (g x)) l a

Tactic:
show IsMaxFilter (fun x => Min.min (f x) (g x)) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => min_le_min hx hy) hg

Premises used: IsMaxFilter.bicomp_mono, min_le_min
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : LinearOrder β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMinOn g s a
⊢ IsMinOn.{u, v} (β := β) (fun (x : α) ↦ Min.min (f x) (g x)) s a

Tactic:
IsMinFilter.min hf hg

Premises used: IsMinFilter.min, IsMinOn
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : LinearOrder β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMaxOn g s a
⊢ IsMaxOn.{u, v} (β := β) (fun (x : α) ↦ Min.min (f x) (g x)) s a

Tactic:
IsMaxFilter.min hf hg

Premises used: IsMaxOn, IsMaxFilter.min
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : LinearOrder β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMinFilter g l a
⊢ IsMinFilter.{u, v} (β := β) (fun (x : α) ↦ Max.max (f x) (g x)) l a

Tactic:
show IsMinFilter (fun x => Max.max (f x) (g x)) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => max_le_max hx hy) hg

Premises used: IsMinFilter.bicomp_mono, max_le_max
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : LinearOrder β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMaxFilter g l a
⊢ IsMaxFilter.{u, v} (β := β) (fun (x : α) ↦ Max.max (f x) (g x)) l a

Tactic:
show IsMaxFilter (fun x => Max.max (f x) (g x)) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => max_le_max hx hy) hg

Premises used: IsMaxFilter.bicomp_mono, max_le_max
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : LinearOrder β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMinOn g s a
⊢ IsMinOn.{u, v} (β := β) (fun (x : α) ↦ Max.max (f x) (g x)) s a

Tactic:
IsMinFilter.max hf hg

Premises used: IsMinOn, IsMinFilter.max
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : LinearOrder β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMaxOn g s a
⊢ IsMaxOn.{u, v} (β := β) (fun (x : α) ↦ Max.max (f x) (g x)) s a

Tactic:
IsMaxFilter.max hf hg

Premises used: IsMaxOn, IsMaxFilter.max
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
by_cases! g₀ : x ≤ b
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀

Premises used: Iff.mpr, Set.Mem, setOf, LE.le.trans_lt', And.left, And.intro, Set.right_mem_Ioc
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
exact h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀

Premises used: Iff.mpr, LE.le.trans_lt', And.left, And.intro, Set.right_mem_Ioc
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : b < x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le

Premises used: Iff.mpr, Set.left_mem_Ico, Set.Mem, setOf, LT.lt.le, And.right, And.intro, LT.lt.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : b < x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
refine h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le

Premises used: Iff.mpr, Set.left_mem_Ico, LT.lt.le, And.right, And.intro, LT.lt.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : AntitoneOn f (Ioc a b)
h₁ : MonotoneOn f (Ico b c)
⊢ IsMinOn f (Ioo a c) b

Tactic:
isMaxOn_Ioo_of_mono_anti (β := βᵒᵈ) h₀ h₁

Premises used: IsMinFilter, IsMinOn, isMaxOn_Ioo_of_mono_anti
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
by_cases! g₀ : x ≤ b
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Mem, setOf, And.left, And.intro, LE.le.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
exact h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀

Premises used: Iff.mpr, Set.right_mem_Icc, And.left, And.intro, LE.le.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : b < x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le

Premises used: Iff.mpr, Set.left_mem_Ico, Set.Mem, setOf, LT.lt.le, And.right, And.intro, LT.lt.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : b < x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
exact h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le

Premises used: Iff.mpr, Set.left_mem_Ico, LT.lt.le, And.right, And.intro, LT.lt.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : AntitoneOn f (Icc a b)
h₁ : MonotoneOn f (Ico b c)
⊢ IsMinOn f (Ico a c) b

Tactic:
isMaxOn_Ico_of_mono_anti (β := βᵒᵈ) h₀ h₁

Premises used: IsMinFilter, IsMinOn, isMaxOn_Ico_of_mono_anti
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
by_cases! g₀ : x ≤ b
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀

Premises used: Iff.mpr, Set.Mem, setOf, LE.le.trans_lt', And.left, And.intro, Set.right_mem_Ioc
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
exact h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀

Premises used: Iff.mpr, LE.le.trans_lt', And.left, And.intro, Set.right_mem_Ioc
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : b < x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
h₁ (left_mem_Icc.2 (g₀.le.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le

Premises used: Iff.mpr, Set.Mem, setOf, LT.lt.le, And.right, Set.left_mem_Icc, And.intro, LE.le.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : b < x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
exact h₁ (left_mem_Icc.2 (g₀.le.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le

Premises used: Iff.mpr, LT.lt.le, And.right, Set.left_mem_Icc, And.intro, LE.le.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : AntitoneOn f (Ioc a b)
h₁ : MonotoneOn f (Icc b c)
⊢ IsMinOn f (Ioc a c) b

Tactic:
isMaxOn_Ioc_of_mono_anti (β := βᵒᵈ) h₀ h₁

Premises used: IsMinFilter, IsMinOn, isMaxOn_Ioc_of_mono_anti