awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (Icc b c)
x : α
hx : x ∈ Icc 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 (Icc b c)
x : α
hx : x ∈ Icc 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 (Icc b c)
x : α
hx : x ∈ Icc 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 (Icc b c)
x : α
hx : x ∈ Icc 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 (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc 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 (Icc a b)
h₁ : MonotoneOn f (Icc b c)
⊢ IsMinOn f (Icc a c) b

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

Premises used: IsMinFilter, IsMinOn, isMaxOn_Icc_of_mono_anti
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
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 : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

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

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

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

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

Tactic:
h₁ self_mem_Ici g₀.le g₀.le

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

Tactic:
exact h₁ self_mem_Ici g₀.le g₀.le

Premises used: LT.lt.le, Set.self_mem_Ici
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : AntitoneOn f (Ioc a b)
h₁ : MonotoneOn f (Ici b)
⊢ IsMinOn f (Ioi a) b

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

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

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

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

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

Premises used: Iff.mpr, Set.right_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 : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
g₀ : b < x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
h₁ self_mem_Ici g₀.le g₀.le

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

Tactic:
exact h₁ self_mem_Ici g₀.le g₀.le

Premises used: LT.lt.le, Set.self_mem_Ici
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : AntitoneOn f (Icc a b)
h₁ : MonotoneOn f (Ici b)
⊢ IsMinOn f (Ici a) b

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

Premises used: IsMinFilter, isMaxOn_Ici_of_mono_anti, IsMinOn
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
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 : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
h₀ g₀ self_mem_Iic g₀

Premises used: Set.self_mem_Iic, Set.Mem, setOf
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
exact h₀ g₀ self_mem_Iic g₀

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

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

Premises used: Iff.mpr, Set.left_mem_Ico, Set.Mem, setOf, LT.lt.le, And.intro, LT.lt.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
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)) ⟨g₀.le, hx⟩ g₀.le

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

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

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

Tactic:
h₀ g₀ self_mem_Iic g₀

Premises used: Set.self_mem_Iic, Set.Mem, setOf
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
g₀ : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
exact h₀ g₀ self_mem_Iic g₀

Premises used: Set.self_mem_Iic
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
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)) ⟨g₀.le, hx⟩ g₀.le

Premises used: Iff.mpr, Set.Mem, setOf, LT.lt.le, 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 : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
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)) ⟨g₀.le, hx⟩ g₀.le

Premises used: Iff.mpr, LT.lt.le, 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 : α
f : α → β
h₀ : AntitoneOn f (Iic b)
h₁ : MonotoneOn f (Icc b a)
⊢ IsMinOn f (Iic a) b

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

Premises used: IsMinFilter, IsMinOn, isMaxOn_Iic_of_mono_anti
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
h : Membership.mem (γ := Set α) univ x
inl : x ≤ b → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
inr : 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:
rcases le_total x b

Premises used: le_total
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
h : Membership.mem (γ := Set α) univ x
h_1 : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
aesop
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
h : Membership.mem (γ := Set α) univ x
h_1 : b ≤ x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
aesop
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
b : α
f : α → β
h₀ : AntitoneOn f (Iic b)
h₁ : MonotoneOn f (Ici b)
⊢ IsMinOn f univ b

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

Premises used: IsMinFilter, IsMinOn, isMaxOn_univ_of_mono_anti
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : 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

Tactic:
hle.mp (h.mono fun x hf hgf => ?_)

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : 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
refine : ∀ (x : α) (hf : f x ≤ f a) (hgf : g x ≤ f x), g x ≤ g a
⊢ IsMaxFilter g l a

Tactic:
refine hle.mp (h.mono fun x hf hgf => ?_)

Premises used: Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : 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
rw : g x ≤ f a
⊢ g x ≤ g a

Tactic:
rw [← hfga]
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : 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

Tactic:
le_trans hgf hf

Premises used: le_trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : 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

Tactic:
exact le_trans hgf hf

Premises used: le_trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
h : IsMaxFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMaxFilter g l a

Tactic:
heq.symm.le.isMaxFilter hfga h

Premises used: Filter.EventuallyLE.isMaxFilter, Filter.EventuallyEq.le, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMaxFilter f l a ↔ IsMaxFilter g l a

Tactic:
⟨fun h => h.congr heq hfga, fun h => h.congr heq.symm hfga.symm⟩

Premises used: IsMaxFilter.congr, Iff.intro, Eq.symm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
hle : f ≤ᶠ[l] g
hfga : f a = g a
h : IsMinFilter f l a
⊢ IsMinFilter g l a

Tactic:
@Filter.EventuallyLE.isMaxFilter _ βᵒᵈ _ _ _ _ _ hle hfga h

Premises used: Filter.EventuallyLE.isMaxFilter, IsMinFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
h : IsMinFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMinFilter g l a

Tactic:
heq.le.isMinFilter hfga h

Premises used: Filter.EventuallyLE.isMinFilter, Filter.EventuallyEq.le
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMinFilter f l a ↔ IsMinFilter g l a

Tactic:
⟨fun h => h.congr heq hfga, fun h => h.congr heq.symm hfga.symm⟩

Premises used: IsMinFilter.congr, Iff.intro, Eq.symm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : 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
⊢ IsMinFilter f l a ∨ IsMaxFilter f l a

Tactic:
rw [IsExtrFilter] at *

Premises used: IsExtrFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : 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
h₁ : IsMinFilter f l a ∨ IsMaxFilter f l a
⊢ f =ᶠ[l] g

Tactic:
rw [IsExtrFilter] at *

Premises used: IsExtrFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : 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
h₁ : IsMinFilter f l a ∨ IsMaxFilter f l a
heq₁ : f =ᶠ[l] g
⊢ f a = g a

Tactic:
rw [IsExtrFilter] at *

Premises used: IsExtrFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : 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
rwa : IsMinFilter g l a ∨ IsMaxFilter f l a
rwa₁ rwa₂ rwa₃ rwa₄ : IsMinFilter f l a ∨ IsMaxFilter f l a
⊢ IsMinFilter g l a ∨ IsMaxFilter g l a

Tactic:
rwa [← heq.isMaxFilter_iff hfga, ← heq.isMinFilter_iff hfga]

Premises used: Filter.EventuallyEq.isMaxFilter_iff, Filter.EventuallyEq.isMinFilter_iff
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsExtrFilter f l a ↔ IsExtrFilter g l a

Tactic:
⟨fun h => h.congr heq hfga, fun h => h.congr heq.symm hfga.symm⟩

Premises used: IsExtrFilter.congr, Iff.intro, Eq.symm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : ConditionallyCompleteLinearOrder α
f : β → α
s : Set β
x₀ : β
hx₀ : x₀ ∈ s
h : IsMaxOn f s x₀
⊢ ⨆ (x : (↑s : Type v)), f (↑x : β) = f x₀

Tactic:
haveI : Nonempty s := ⟨⟨x₀, hx₀⟩⟩
  ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun x => h x.2) fun _w hw => ⟨⟨x₀, hx₀⟩, hw⟩

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt, Subtype.mk, Exists.intro, Subtype.property
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : ConditionallyCompleteLinearOrder α
f : β → α
s : Set β
x₀ : β
hx₀ : x₀ ∈ s
h : IsMinOn f s x₀
⊢ ⨅ (x : (↑s : Type v)), f (↑x : β) = f x₀

Tactic:
@IsMaxOn.iSup_eq αᵒᵈ β _ _ _ _ hx₀ h

Premises used: iInf, IsMaxOn.iSup_eq, OrderDual
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
a : α
hmem : a ∈ s
hmax : IsMaxOn D (↑s : Set α) a
⊢ s.sup D = D a

Tactic:
(Finset.sup_le hmax).antisymm (Finset.le_sup hmem)

Premises used: LE.le.antisymm, Finset.sup_le, Finset.le_sup
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
inst_2 : Nonempty α
b : β
hb : b ∈ range D
hmem : Function.invFun D b ∈ s
hmax : ∀ a ∈ s, D a ≤ b
obtain : ∀ (a : α) (hmem : Function.invFun D (D a) ∈ s) (hmax : ∀ a_1 ∈ s, D a_1 ≤ D a), s.sup D = D a
⊢ s.sup D = b

Tactic:
obtain ⟨a, rfl⟩ := hb

Premises used: rfl
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
inst_2 : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
rw : s.sup D = D (Function.invFun D (D a))
⊢ s.sup D = D a

Tactic:
rw [← Function.apply_invFun_apply (f := D)]

Premises used: Function.apply_invFun_apply
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
inst_2 : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
apply : IsMaxOn D (↑s : Set α) (Function.invFun D (D a))
⊢ s.sup D = D (Function.invFun D (D a))

Tactic:
apply sup_eq_of_isMaxOn hmem

Premises used: sup_eq_of_isMaxOn
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
inst_2 : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_2 ∈ s, D a_2 ≤ D a
a_1 : α
rw : a_1 ∈ (↑s : Set α) → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ D x ≤ D a) x} a_1
⊢ a_1 ∈ (↑s : Set α) → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ D x ≤ D (Function.invFun D (D a))) x} a_1

Tactic:
rw [Function.apply_invFun_apply (f := D)]

Premises used: Function.apply_invFun_apply
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
inst_2 : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_2 ∈ s, D a_2 ≤ D a
a_1 : α
⊢ a_1 ∈ (↑s : Set α) → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ D x ≤ D a) x} a_1

Tactic:
apply hmax
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeInf β
inst_1 : OrderTop β
D : α → β
s : Finset α
a : α
hmem : a ∈ s
hmax : IsMinOn D (↑s : Set α) a
⊢ s.inf D = D a

Tactic:
sup_eq_of_isMaxOn (α := αᵒᵈ) (β := βᵒᵈ) hmem hmax.dual

Premises used: OrderDual, sup_eq_of_isMaxOn, Finset.inf, IsMinOn.dual
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : SemilatticeInf β
inst_1 : OrderTop β
D : α → β
s : Finset α
inst_2 : Nonempty α
b : β
hb : b ∈ range D
hmem : Function.invFun D b ∈ s
hmin : ∀ a ∈ s, b ≤ D a
⊢ s.inf D = b

Tactic:
sup_eq_of_max (α := αᵒᵈ) (β := βᵒᵈ) hb hmem hmin

Premises used: OrderDual, sup_eq_of_max, Finset.inf
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : GroupWithZero β
⊢ EventuallyEq.{u, v} (β := β) (↑φ : Filter α) ((fun (x : α → β) ↦ Inv.inv ∘ x) fun (x : α) ↦ 0) fun (x : α) ↦ 0

Tactic:
simp only [Function.comp_def, inv_zero, EventuallyEq.rfl]

Premises used: inv_zero, Function.comp_def, Filter.EventuallyEq.rfl
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : Preorder β
f g : α → β
⊢ LT.lt (α := (↑φ : Filter α).Germ β) (↑f : (↑φ : Filter α).Germ β) (↑g : (↑φ : Filter α).Germ β) ↔
    ∀* (x : α), f x < g x

Tactic:
simp only [lt_iff_le_not_ge, eventually_and, coe_le, eventually_not, EventuallyLE]

Premises used: Filter.eventually_and, Ultrafilter.eventually_not, lt_iff_le_not_ge, Filter.Germ.coe_le, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : Preorder β
inst_1 : Zero β
f : α → β
⊢ LT.lt (α := (↑φ : Filter α).Germ β) 0 (↑f : (↑φ : Filter α).Germ β) ↔ ∀* (x : α), 0 < f x

Tactic:
coe_lt

Premises used: Filter.Germ.ofFun, Filter.Germ.coe_lt, Filter.Germ.const, Quotient.mk'
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : Preorder β
x y : β
⊢ x < y → LT.lt (α := (↑φ : Filter α).Germ β) (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β)

Tactic:
coe_lt.mpr ∘ liftRel_const

Premises used: Iff.mpr, Filter.Germ.coe_lt, Function.comp, Filter.Germ.liftRel_const
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : Preorder β
x y : β
⊢ LT.lt (α := (↑φ : Filter α).Germ β) (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β) ↔ x < y

Tactic:
coe_lt.trans liftRel_const_iff

Premises used: Filter.Germ.coe_lt, Filter.Germ.liftRel_const_iff, Filter.Germ.const, Iff.trans