awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x : R | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ liminf f F ≤ f m

Tactic:
have B : F.liminf f ≤ f m := by
      apply liminf_le_of_frequently_le _ _
      · apply (frequently_lt_of_lt_limsSup cobdd m_lt).mono
        exact fun x hx ↦ f_decr hx.le
      · exact IsBounded.isBoundedUnder f_decr bdd_above
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x : R | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
B : liminf f F ≤ f m
⊢ f m < liminf f F

Tactic:
have I : f m < F.liminf f := h'l ⟨l_m, m_lt.le⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x : R | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
B : liminf f F ≤ f m
I : f m < liminf f F
⊢ False

Tactic:
lt_irrefl _ (B.trans_lt I)

Premises used: lt_irrefl, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x : R | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
B : liminf f F ≤ f m
I : f m < liminf f F
⊢ False

Tactic:
exact lt_irrefl _ (B.trans_lt I)

Premises used: lt_irrefl, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
S : Type u_5
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder R
inst_2 : TopologicalSpace R
inst_3 : OrderTopology R
inst_4 : ConditionallyCompleteLinearOrder S
inst_5 : TopologicalSpace S
inst_6 : OrderTopology S
f : R → S
f_decr : Antitone f
a : ι → R
f_cont : ContinuousAt f (limsup a F)
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F a
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F a
⊢ f (limsup a F) = liminf (f ∘ a) F

Tactic:
f_decr.map_limsSup_of_continuousAt f_cont bdd_above cobdd

Premises used: Filter.liminf, Set.Mem, Antitone.map_limsSup_of_continuousAt, Filter.map, setOf, Filter.limsup, Set.preimage
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsInf
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≥ x2) F
bdd_below : IsBounded (fun (x1 x2 : R) ↦ x1 ≥ x2) F
⊢ f F.limsInf = limsup f F

Tactic:
Antitone.map_limsSup_of_continuousAt (R := Rᵒᵈ) (S := Sᵒᵈ) f_decr.dual f_cont bdd_below cobdd

Premises used: Filter.limsSup, Filter.limsInf, Antitone.map_limsSup_of_continuousAt, setOf, Antitone.dual, Filter.limsup, OrderDual
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
S : Type u_5
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder R
inst_2 : TopologicalSpace R
inst_3 : OrderTopology R
inst_4 : ConditionallyCompleteLinearOrder S
inst_5 : TopologicalSpace S
inst_6 : OrderTopology S
f : R → S
f_decr : Antitone f
a : ι → R
f_cont : ContinuousAt f (liminf a F)
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F a
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F a
⊢ f (liminf a F) = limsup (f ∘ a) F

Tactic:
f_decr.map_limsInf_of_continuousAt f_cont cobdd bdd_below

Premises used: Filter.liminf, Set.Mem, Filter.map, setOf, Filter.limsup, Set.preimage, Antitone.map_limsInf_of_continuousAt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_incr : Monotone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
⊢ f F.limsSup = limsup f F

Tactic:
Antitone.map_limsSup_of_continuousAt (S := Sᵒᵈ) f_incr f_cont bdd_above cobdd

Premises used: Filter.limsSup, Antitone.map_limsSup_of_continuousAt, setOf, Filter.limsup, OrderDual
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
S : Type u_5
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder R
inst_2 : TopologicalSpace R
inst_3 : OrderTopology R
inst_4 : ConditionallyCompleteLinearOrder S
inst_5 : TopologicalSpace S
inst_6 : OrderTopology S
f : R → S
f_incr : Monotone f
a : ι → R
f_cont : ContinuousAt f (limsup a F)
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F a
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F a
⊢ f (limsup a F) = limsup (f ∘ a) F

Tactic:
f_incr.map_limsSup_of_continuousAt f_cont bdd_above cobdd

Premises used: Set.Mem, Filter.map, setOf, Filter.limsup, Monotone.map_limsSup_of_continuousAt, Set.preimage
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_incr : Monotone f
f_cont : ContinuousAt f F.limsInf
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≥ x2) F
bdd_below : IsBounded (fun (x1 x2 : R) ↦ x1 ≥ x2) F
⊢ f F.limsInf = liminf f F

Tactic:
Antitone.map_limsSup_of_continuousAt (R := Rᵒᵈ) f_incr.dual f_cont bdd_below cobdd

Premises used: Filter.limsInf, Antitone.map_limsSup_of_continuousAt, setOf, Monotone.dual, OrderDual
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
S : Type u_5
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder R
inst_2 : TopologicalSpace R
inst_3 : OrderTopology R
inst_4 : ConditionallyCompleteLinearOrder S
inst_5 : TopologicalSpace S
inst_6 : OrderTopology S
f : R → S
f_incr : Monotone f
a : ι → R
f_cont : ContinuousAt f (liminf a F)
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F a
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F a
⊢ f (liminf a F) = liminf (f ∘ a) F

Tactic:
f_incr.map_limsInf_of_continuousAt f_cont cobdd bdd_below

Premises used: Filter.liminf, Set.Mem, Filter.map, setOf, Set.preimage, Monotone.map_limsInf_of_continuousAt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), a < b
rw : Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : a < i), ⨅ a_1 ∈ Set.Ioo a i, f a_1) (⨆ (r : α), ⨆ (_ : r > a), f r)
⊢ liminf f (𝓝[>] a) = ⨆ (r : α), ⨆ (_ : r > a), f r

Tactic:
rw [(nhdsGT_basis_of_exists_gt hb).liminf_eq_iSup_iInf]

Premises used: nhdsGT_basis_of_exists_gt, Filter.HasBasis.liminf_eq_iSup_iInf
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), a < b
⊢ Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : a < i), ⨅ a_1 ∈ Set.Ioo a i, f a_1) (⨆ (r : α), ⨆ (_ : r > a), f r)

Tactic:
le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).2.le⟩)

Premises used: Set.mem_Ioo, LT.lt.le, le_iInf₂, iSup₂_mono', le_antisymm, And.right, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), a < b
refine : ∀ (r : α) (hr : a < r), ∃ (i' : α) (_ : i' > a), ⨅ a_1 ∈ Set.Ioo a r, f a_1 ≤ f i'
⊢ Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : a < i), ⨅ a_1 ∈ Set.Ioo a i, f a_1) (⨆ (r : α), ⨆ (_ : r > a), f r)

Tactic:
refine le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).2.le⟩)

Premises used: Set.mem_Ioo, LT.lt.le, le_iInf₂, iSup₂_mono', le_antisymm, And.right, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), a < b
r : α
hr : a < r
obtain : ∀ (b : α) (hb : a < b ∧ b < r), ∃ (i' : α) (_ : i' > a), ⨅ a_1 ∈ Set.Ioo a r, f a_1 ≤ f i'
⊢ ∃ (i' : α) (_ : i' > a), ⨅ a_1 ∈ Set.Ioo a r, f a_1 ≤ f i'

Tactic:
obtain ⟨b, hb⟩ := exists_between hr

Premises used: exists_between
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb_1 : ∃ (b : α), a < b
r : α
hr : a < r
b : α
hb : a < b ∧ b < r
⊢ ∃ (i' : α) (_ : i' > a), ⨅ a_1 ∈ Set.Ioo a r, f a_1 ≤ f i'

Tactic:
⟨b, hb.1, iInf₂_le b hb⟩

Premises used: iInf₂_le, And.left, Exists.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb_1 : ∃ (b : α), a < b
r : α
hr : a < r
b : α
hb : a < b ∧ b < r
⊢ ∃ (i' : α) (_ : i' > a), ⨅ a_1 ∈ Set.Ioo a r, f a_1 ≤ f i'

Tactic:
exact ⟨b, hb.1, iInf₂_le b hb⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
inst_5 : NoMaxOrder α
hf : Antitone f
a : α
⊢ liminf f (𝓝[>] a) = ⨆ (r : α), ⨆ (_ : r > a), f r

Tactic:
hf.liminf_nhdsGT_eq_iSup₂_of_exists_gt a (exists_gt a)

Premises used: NoMaxOrder.exists_gt, Antitone.liminf_nhdsGT_eq_iSup₂_of_exists_gt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), b < a
rw : Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : i < a), ⨅ a_1 ∈ Set.Ioo i a, f a_1) (⨆ (r : α), ⨆ (_ : r < a), f r)
⊢ liminf f (𝓝[<] a) = ⨆ (r : α), ⨆ (_ : r < a), f r

Tactic:
rw [(nhdsLT_basis_of_exists_lt hb).liminf_eq_iSup_iInf]

Premises used: nhdsLT_basis_of_exists_lt, Filter.HasBasis.liminf_eq_iSup_iInf
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), b < a
⊢ Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : i < a), ⨅ a_1 ∈ Set.Ioo i a, f a_1) (⨆ (r : α), ⨆ (_ : r < a), f r)

Tactic:
le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).1.le⟩)

Premises used: Set.mem_Ioo, LT.lt.le, le_iInf₂, iSup₂_mono', le_antisymm, And.left, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), b < a
refine : ∀ (r : α) (hr : r < a), ∃ (i' : α) (_ : i' < a), ⨅ a_1 ∈ Set.Ioo r a, f a_1 ≤ f i'
⊢ Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : i < a), ⨅ a_1 ∈ Set.Ioo i a, f a_1) (⨆ (r : α), ⨆ (_ : r < a), f r)

Tactic:
refine le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).1.le⟩)

Premises used: Set.mem_Ioo, LT.lt.le, le_iInf₂, iSup₂_mono', le_antisymm, And.left, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), b < a
r : α
hr : r < a
obtain : ∀ (b : α) (hb : r < b ∧ b < a), ∃ (i' : α) (_ : i' < a), ⨅ a_1 ∈ Set.Ioo r a, f a_1 ≤ f i'
⊢ ∃ (i' : α) (_ : i' < a), ⨅ a_1 ∈ Set.Ioo r a, f a_1 ≤ f i'

Tactic:
obtain ⟨b, hb⟩ := exists_between hr

Premises used: exists_between
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb_1 : ∃ (b : α), b < a
r : α
hr : r < a
b : α
hb : r < b ∧ b < a
⊢ ∃ (i' : α) (_ : i' < a), ⨅ a_1 ∈ Set.Ioo r a, f a_1 ≤ f i'

Tactic:
⟨b, hb.2, iInf₂_le b hb⟩

Premises used: iInf₂_le, And.right, Exists.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb_1 : ∃ (b : α), b < a
r : α
hr : r < a
b : α
hb : r < b ∧ b < a
⊢ ∃ (i' : α) (_ : i' < a), ⨅ a_1 ∈ Set.Ioo r a, f a_1 ≤ f i'

Tactic:
exact ⟨b, hb.2, iInf₂_le b hb⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
inst_5 : NoMinOrder α
hf : Monotone f
a : α
⊢ liminf f (𝓝[<] a) = ⨆ (r : α), ⨆ (_ : r < a), f r

Tactic:
hf.liminf_nhdsLT_eq_iSup₂_of_exists_lt a (exists_lt a)

Premises used: NoMinOrder.exists_lt, Monotone.liminf_nhdsLT_eq_iSup₂_of_exists_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), a < b
rw : Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : a < i), ⨆ a_1 ∈ Set.Ioo a i, f a_1) (⨅ (r : α), ⨅ (_ : r > a), f r)
⊢ limsup f (𝓝[>] a) = ⨅ (r : α), ⨅ (_ : r > a), f r

Tactic:
rw [(nhdsGT_basis_of_exists_gt hb).limsup_eq_iInf_iSup]

Premises used: nhdsGT_basis_of_exists_gt, Filter.HasBasis.limsup_eq_iInf_iSup
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), a < b
⊢ Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : a < i), ⨆ a_1 ∈ Set.Ioo a i, f a_1) (⨅ (r : α), ⨅ (_ : r > a), f r)

Tactic:
le_antisymm
    (iInf₂_mono' fun r hr ↦ ⟨r, hr, iSup₂_le fun i hi ↦ hf (Set.mem_Ioo.1 hi).2.le⟩)
    (iInf₂_mono' fun r hr ↦ ?_)

Premises used: iSup₂_le, Set.mem_Ioo, LT.lt.le, le_antisymm, iInf₂_mono', And.right, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), a < b
refine : ∀ (r : α) (hr : a < r), ∃ (i' : α) (_ : i' > a), f i' ≤ ⨆ a_1 ∈ Set.Ioo a r, f a_1
⊢ Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : a < i), ⨆ a_1 ∈ Set.Ioo a i, f a_1) (⨅ (r : α), ⨅ (_ : r > a), f r)

Tactic:
refine le_antisymm
    (iInf₂_mono' fun r hr ↦ ⟨r, hr, iSup₂_le fun i hi ↦ hf (Set.mem_Ioo.1 hi).2.le⟩)
    (iInf₂_mono' fun r hr ↦ ?_)

Premises used: iSup₂_le, Set.mem_Ioo, LT.lt.le, le_antisymm, iInf₂_mono', And.right, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), a < b
r : α
hr : a < r
obtain : ∀ (b : α) (hb : a < b ∧ b < r), ∃ (i' : α) (_ : i' > a), f i' ≤ ⨆ a_1 ∈ Set.Ioo a r, f a_1
⊢ ∃ (i' : α) (_ : i' > a), f i' ≤ ⨆ a_1 ∈ Set.Ioo a r, f a_1

Tactic:
obtain ⟨b, hb⟩ := exists_between hr

Premises used: exists_between
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb_1 : ∃ (b : α), a < b
r : α
hr : a < r
b : α
hb : a < b ∧ b < r
⊢ ∃ (i' : α) (_ : i' > a), f i' ≤ ⨆ a_1 ∈ Set.Ioo a r, f a_1

Tactic:
⟨b, hb.1, le_iSup₂_of_le b hb le_rfl⟩

Premises used: le_rfl, And.left, Exists.intro, le_iSup₂_of_le
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb_1 : ∃ (b : α), a < b
r : α
hr : a < r
b : α
hb : a < b ∧ b < r
⊢ ∃ (i' : α) (_ : i' > a), f i' ≤ ⨆ a_1 ∈ Set.Ioo a r, f a_1

Tactic:
exact ⟨b, hb.1, le_iSup₂_of_le b hb le_rfl⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
inst_5 : NoMaxOrder α
hf : Monotone f
a : α
⊢ limsup f (𝓝[>] a) = ⨅ (r : α), ⨅ (_ : r > a), f r

Tactic:
hf.limsup_nhdsGT_eq_iInf₂_of_exists_gt a (exists_gt a)

Premises used: NoMaxOrder.exists_gt, Monotone.limsup_nhdsGT_eq_iInf₂_of_exists_gt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), b < a
rw : Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : i < a), ⨆ a_1 ∈ Set.Ioo i a, f a_1) (⨅ (r : α), ⨅ (_ : r < a), f r)
⊢ limsup f (𝓝[<] a) = ⨅ (r : α), ⨅ (_ : r < a), f r

Tactic:
rw [(nhdsLT_basis_of_exists_lt hb).limsup_eq_iInf_iSup]

Premises used: nhdsLT_basis_of_exists_lt, Filter.HasBasis.limsup_eq_iInf_iSup
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), b < a
⊢ Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : i < a), ⨆ a_1 ∈ Set.Ioo i a, f a_1) (⨅ (r : α), ⨅ (_ : r < a), f r)

Tactic:
le_antisymm
    (iInf₂_mono' fun r hr ↦ ⟨r, hr, iSup₂_le fun i hi ↦ hf (Set.mem_Ioo.1 hi).1.le⟩)
    (iInf₂_mono' fun r hr ↦ ?_)

Premises used: iSup₂_le, Set.mem_Ioo, LT.lt.le, le_antisymm, iInf₂_mono', And.left, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), b < a
refine : ∀ (r : α) (hr : r < a), ∃ (i' : α) (_ : i' < a), f i' ≤ ⨆ a_1 ∈ Set.Ioo r a, f a_1
⊢ Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : i < a), ⨆ a_1 ∈ Set.Ioo i a, f a_1) (⨅ (r : α), ⨅ (_ : r < a), f r)

Tactic:
refine le_antisymm
    (iInf₂_mono' fun r hr ↦ ⟨r, hr, iSup₂_le fun i hi ↦ hf (Set.mem_Ioo.1 hi).1.le⟩)
    (iInf₂_mono' fun r hr ↦ ?_)

Premises used: iSup₂_le, Set.mem_Ioo, LT.lt.le, le_antisymm, iInf₂_mono', And.left, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), b < a
r : α
hr : r < a
obtain : ∀ (b : α) (hb : r < b ∧ b < a), ∃ (i' : α) (_ : i' < a), f i' ≤ ⨆ a_1 ∈ Set.Ioo r a, f a_1
⊢ ∃ (i' : α) (_ : i' < a), f i' ≤ ⨆ a_1 ∈ Set.Ioo r a, f a_1

Tactic:
obtain ⟨b, hb⟩ := exists_between hr

Premises used: exists_between
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb_1 : ∃ (b : α), b < a
r : α
hr : r < a
b : α
hb : r < b ∧ b < a
⊢ ∃ (i' : α) (_ : i' < a), f i' ≤ ⨆ a_1 ∈ Set.Ioo r a, f a_1

Tactic:
⟨b, hb.2, le_iSup₂_of_le b hb le_rfl⟩

Premises used: le_rfl, And.right, Exists.intro, le_iSup₂_of_le
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb_1 : ∃ (b : α), b < a
r : α
hr : r < a
b : α
hb : r < b ∧ b < a
⊢ ∃ (i' : α) (_ : i' < a), f i' ≤ ⨆ a_1 ∈ Set.Ioo r a, f a_1

Tactic:
exact ⟨b, hb.2, le_iSup₂_of_le b hb le_rfl⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
inst_5 : NoMinOrder α
hf : Antitone f
a : α
⊢ limsup f (𝓝[<] a) = ⨅ (r : α), ⨅ (_ : r < a), f r

Tactic:
hf.limsup_nhdsLT_eq_iInf₂_of_exists_lt a (exists_lt a)

Premises used: NoMinOrder.exists_lt, Antitone.limsup_nhdsLT_eq_iInf₂_of_exists_lt
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
p : Prop
⊢ IsLocalExtrOn f s a → (IsLocalMinOn f s a → p) → (IsLocalMaxOn f s a → p) → p

Tactic:
Or.elim

Premises used: IsLocalMinOn, IsLocalExtrOn, IsLocalMaxOn, IsExtrFilter, Or.elim
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
a : α
p : Prop
⊢ IsLocalExtr f a → (IsLocalMin f a → p) → (IsLocalMax f a → p) → p

Tactic:
Or.elim

Premises used: IsLocalMax, IsLocalExtr, IsLocalMin, IsExtrFilter, Or.elim
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
a : α
h : IsLocalMin f a
s : Set α
⊢ IsLocalMinOn f s a

Tactic:
h.filter_inf _

Premises used: nhdsWithin, IsLocalMinOn, IsMinFilter.filter_inf