awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
inst_6 : Finite ι
inst_7 : (i : ι) → Preorder (π i)
inst_8 : (i : ι) → TopologicalSpace (π i)
inst_9 : ∀ (i : ι), BoundedLENhdsClass.{u_6} (π i)
x : (i : ι) → π i
rw : IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (pi (α := π) fun (i : ι) ↦ 𝓝 (x i))
⊢ IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (𝓝 x)

Tactic:
rw [nhds_pi]

Premises used: nhds_pi
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
inst_6 : Finite ι
inst_7 : (i : ι) → Preorder (π i)
inst_8 : (i : ι) → TopologicalSpace (π i)
inst_9 : ∀ (i : ι), BoundedLENhdsClass.{u_6} (π i)
x : (i : ι) → π i
choose :
  ∀ (f : (i : ι) → π i) (hf : ∀ (i : ι), ∀ᶠ (x : π i) in 𝓝 (x i), (fun (x1 x2 : π i) ↦ x1 ≤ x2) x (f i)),
    IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (pi (α := π) fun (i : ι) ↦ 𝓝 (x i))
⊢ IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (pi (α := π) fun (i : ι) ↦ 𝓝 (x i))

Tactic:
choose f hf using fun i ↦ isBounded_le_nhds (x i)

Premises used: isBounded_le_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f_1 : Filter ι
u : ι → α
a : α
inst_6 : Finite ι
inst_7 : (i : ι) → Preorder (π i)
inst_8 : (i : ι) → TopologicalSpace (π i)
inst_9 : ∀ (i : ι), BoundedLENhdsClass.{u_6} (π i)
x f : (i : ι) → π i
hf : ∀ (i : ι), ∀ᶠ (x : π i) in 𝓝 (x i), (fun (x1 x2 : π i) ↦ x1 ≤ x2) x (f i)
⊢ IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (pi (α := π) fun (i : ι) ↦ 𝓝 (x i))

Tactic:
⟨f, eventually_pi hf⟩

Premises used: Filter.eventually_pi, Filter.IsBounded, Exists.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f_1 : Filter ι
u : ι → α
a : α
inst_6 : Finite ι
inst_7 : (i : ι) → Preorder (π i)
inst_8 : (i : ι) → TopologicalSpace (π i)
inst_9 : ∀ (i : ι), BoundedLENhdsClass.{u_6} (π i)
x f : (i : ι) → π i
hf : ∀ (i : ι), ∀ᶠ (x : π i) in 𝓝 (x i), (fun (x1 x2 : π i) ↦ x1 ≤ x2) x (f i)
⊢ IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (pi (α := π) fun (i : ι) ↦ 𝓝 (x i))

Tactic:
exact ⟨f, eventually_pi hf⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedGENhdsClass α
a : α
⊢ IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (𝓝 a)

Tactic:
BoundedGENhdsClass.isBounded_ge_nhds _

Premises used: BoundedGENhdsClass.isBounded_ge_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedGENhdsClass α
f : Filter ι
u : ι → α
a : α
h : Tendsto u f (𝓝 a)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u

Tactic:
(isBounded_ge_nhds a).mono h

Premises used: Filter.IsBounded.mono, isBounded_ge_nhds, Filter.IsBoundedUnder
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedGENhdsClass α
u : ι → α
a : α
inst_3 : IsCodirectedOrder α
h : Tendsto u cofinite (𝓝 a)
⊢ BddBelow (Set.range u)

Tactic:
h.isBoundedUnder_ge.bddBelow_range_of_cofinite

Premises used: Filter.Tendsto.isBoundedUnder_ge, Filter.IsBoundedUnder.bddBelow_range_of_cofinite
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedGENhdsClass α
a : α
inst_3 : IsCodirectedOrder α
u : ℕ → α
h : Tendsto u atTop (𝓝 a)
⊢ BddBelow (Set.range u)

Tactic:
h.isBoundedUnder_ge.bddBelow_range

Premises used: Filter.Tendsto.isBoundedUnder_ge, Filter.IsBoundedUnder.bddBelow_range
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedGENhdsClass α
a : α
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (𝓝 a)

Tactic:
(isBounded_ge_nhds a).isCobounded_flip

Premises used: isBounded_ge_nhds, Filter.IsBounded.isCobounded_flip
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedGENhdsClass α
f : Filter ι
u : ι → α
a : α
inst_3 : f.NeBot
h : Tendsto u f (𝓝 a)
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u

Tactic:
h.isBoundedUnder_ge.isCobounded_flip

Premises used: Filter.Tendsto.isBoundedUnder_ge, Filter.IsCoboundedUnder, Filter.IsBounded.isCobounded_flip
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedGENhdsClass α
inst_5 : BoundedGENhdsClass β
f : Filter ι
u : ι → α
a : α
⊢ BoundedLENhdsClass.{u_2} αᵒᵈ

Tactic:
⟨@isBounded_ge_nhds α _ _ _⟩

Premises used: isBounded_ge_nhds, BoundedLENhdsClass.mk
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedGENhdsClass α
inst_5 : BoundedGENhdsClass β
f : Filter ι
u : ι → α
a : α
⊢ BoundedGENhdsClass (α × β)

Tactic:
⟨(Prod.instBoundedLENhdsClass (α := αᵒᵈ) (β := βᵒᵈ)).isBounded_le_nhds⟩

Premises used: BoundedLENhdsClass.isBounded_le_nhds, BoundedGENhdsClass.mk
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedGENhdsClass α
inst_5 : BoundedGENhdsClass β
f : Filter ι
u : ι → α
a : α
inst_6 : Finite ι
inst_7 : (i : ι) → Preorder (π i)
inst_8 : (i : ι) → TopologicalSpace (π i)
inst_9 : ∀ (i : ι), BoundedGENhdsClass.{u_6} (π i)
⊢ BoundedGENhdsClass ((i : ι) → π i)

Tactic:
⟨(Pi.instBoundedLENhdsClass (π := fun i ↦ (π i)ᵒᵈ)).isBounded_le_nhds⟩

Premises used: BoundedLENhdsClass.isBounded_le_nhds, BoundedGENhdsClass.mk
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTop α
⊢ BoundedLENhdsClass α

Tactic:
⟨fun _a ↦ isBounded_le_of_top⟩

Premises used: Filter.isBounded_le_of_top, BoundedLENhdsClass.mk
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderBot α
⊢ BoundedGENhdsClass α

Tactic:
⟨fun _a ↦ isBounded_ge_of_bot⟩

Premises used: BoundedGENhdsClass.mk, Filter.isBounded_ge_of_bot
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIciTopology α
⊢ BoundedLENhdsClass α

Tactic:
⟨fun a ↦ ((isTop_or_exists_gt a).elim fun h ↦ ⟨a, Eventually.of_forall h⟩) <|
    Exists.imp fun _b ↦ eventually_le_nhds⟩

Premises used: isTop_or_exists_gt, Exists.imp, eventually_le_nhds, BoundedLENhdsClass.mk, Or.elim
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
⊢ BoundedGENhdsClass α

Tactic:
inferInstanceAs <| BoundedGENhdsClass αᵒᵈᵒᵈ

Premises used: _private.0.BoundedGENhdsClass.of_closedIicTopology._proof_1
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
a : α
hl : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hg : IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
hs : f.limsSup = a
hi : f.limsInf = a
⊢ f ≤ 𝓝 a

Tactic:
tendsto_order.2 ⟨fun _ hb ↦ gt_mem_sets_of_limsInf_gt hg <| hi.symm ▸ hb,
    fun _ hb ↦ lt_mem_sets_of_limsSup_lt hl <| hs.symm ▸ hb⟩

Premises used: Iff.mpr, Set.Mem, setOf, tendsto_order, Eq.rec, Set.preimage, Filter.Tendsto, And.intro, Eq.symm, Filter.lt_mem_sets_of_limsSup_lt, Filter.gt_mem_sets_of_limsInf_gt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
⊢ (𝓝 a).limsSup = a

Tactic:
csInf_eq_of_forall_ge_of_forall_gt_exists_lt (isBounded_le_nhds a)
    (fun a' (h : { n : α | n ≤ a' } ∈ 𝓝 a) ↦ show a ≤ a' from @mem_of_mem_nhds _ _ a _ h)
    fun b (hba : a < b) ↦
    show ∃ c, { n : α | n ≤ c } ∈ 𝓝 a ∧ c < b from
      match dense_or_discrete a b with
      | Or.inl ⟨c, hac, hcb⟩ => ⟨c, ge_mem_nhds hac, hcb⟩
      | Or.inr ⟨_, h⟩ => ⟨a, (𝓝 a).sets_of_superset (gt_mem_nhds hba) h, hba⟩

Premises used: Filter.limsSup, gt_mem_nhds, csInf_eq_of_forall_ge_of_forall_gt_exists_lt, setOf, Membership.mem, Exists, nhds, _private.0.limsSup_nhds.match_1, LE.le, mem_of_mem_nhds, Filter.sets_of_superset, ge_mem_nhds, And, And.intro, LT.lt, Exists.intro, dense_or_discrete, isBounded_le_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
⊢ (𝓝 a).limsInf = a

Tactic:
limsSup_nhds (α := αᵒᵈ) a

Premises used: Filter.limsInf, setOf, OrderDual, limsSup_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
a : α
inst_3 : f.NeBot
h : f ≤ 𝓝 a
⊢ f.limsInf = a

Tactic:
have hb_ge : IsBounded (· ≥ ·) f := (isBounded_ge_nhds a).mono h
  have hb_le : IsBounded (· ≤ ·) f := (isBounded_le_nhds a).mono h
  le_antisymm
    (calc
      f.limsInf ≤ f.limsSup := limsInf_le_limsSup hb_le hb_ge
      _ ≤ (𝓝 a).limsSup := limsSup_le_limsSup_of_le h hb_ge.isCobounded_flip (isBounded_le_nhds a)
      _ = a := limsSup_nhds a)
    (calc
      a = (𝓝 a).limsInf := (limsInf_nhds a).symm
      _ ≤ f.limsInf := limsInf_le_limsInf_of_le h (isBounded_ge_nhds a) hb_le.isCobounded_flip)

Premises used: Filter.limsInf_le_limsSup, Trans.trans, Filter.limsInf_le_limsInf_of_le, Filter.IsBounded.mono, isBounded_ge_nhds, le_antisymm, limsInf_nhds, Filter.IsBounded.isCobounded_flip, Eq.symm, isBounded_le_nhds, Filter.limsSup_le_limsSup_of_le, limsSup_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
a : α
inst_3 : f.NeBot
h : f ≤ 𝓝 a
⊢ f.limsSup = a

Tactic:
limsInf_eq_of_le_nhds (α := αᵒᵈ) h

Premises used: Filter.limsSup, limsInf_eq_of_le_nhds, setOf, OrderDual
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter β
u : β → α
a : α
inst_3 : f.NeBot
h : Tendsto u f (𝓝 a)
⊢ limsup u f = a

Tactic:
limsSup_eq_of_le_nhds h

Premises used: limsSup_eq_of_le_nhds, Filter.limsup
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter β
u : β → α
a : α
inst_3 : f.NeBot
h : Tendsto u f (𝓝 a)
⊢ liminf u f = a

Tactic:
limsInf_eq_of_le_nhds h

Premises used: Filter.liminf, limsInf_eq_of_le_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
pos : ∀ (hn : Nontrivial α), ClusterPt f.limsSup f
neg : ∀ (hn : Subsingleton α), ClusterPt f.limsSup f
⊢ ClusterPt f.limsSup f

Tactic:
by_cases! hn : Nontrivial α

Premises used: Nontrivial
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
pos : ∀ (htop : ∀ (x : α), x ≤ f.limsSup), ClusterPt f.limsSup f
neg : ∀ (htop : ∃ (x : α), f.limsSup < x), ClusterPt f.limsSup f
⊢ ClusterPt f.limsSup f

Tactic:
by_cases! htop : ∀ x, x ≤ f.limsSup
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∀ (x : α), x ≤ f.limsSup
this : OrderTop α := { top := f.limsSup, le_top := htop }
⊢ ClusterPt f.limsSup f

Tactic:
nhds_top_basis.clusterPt_iff_frequently |>.mpr fun a => frequently_lt_of_lt_limsSup hc

Premises used: Iff.mpr, Filter.HasBasis.clusterPt_iff_frequently, Filter.frequently_lt_of_lt_limsSup, nhds_top_basis
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∀ (x : α), x ≤ f.limsSup
this : OrderTop α := { top := f.limsSup, le_top := htop }
⊢ ClusterPt f.limsSup f

Tactic:
exact nhds_top_basis.clusterPt_iff_frequently |>.mpr fun a => frequently_lt_of_lt_limsSup hc

Premises used: Iff.mpr, Filter.HasBasis.clusterPt_iff_frequently, Filter.frequently_lt_of_lt_limsSup, nhds_top_basis
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ (x : α), f.limsSup < x
pos : ∀ (hbot : ∀ (x : α), f.limsSup ≤ x), ClusterPt f.limsSup f
neg : ∀ (hbot : ∃ (x : α), x < f.limsSup), ClusterPt f.limsSup f
⊢ ClusterPt f.limsSup f

Tactic:
by_cases! hbot : ∀ x, f.limsSup ≤ x
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ (x : α), f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
this : OrderBot α := { bot := f.limsSup, bot_le := hbot }
⊢ ClusterPt f.limsSup f

Tactic:
nhds_bot_basis.clusterPt_iff_frequently |>.mpr fun a h => ?_

Premises used: Iff.mpr, nhds_bot_basis, Filter.HasBasis.clusterPt_iff_frequently
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ (x : α), f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
this : OrderBot α := { bot := f.limsSup, bot_le := hbot }
pos : ∀ (a : α) (h : ⊥ < a), ∃ᶠ (x : α) in f, x ∈ Set.Iio a
⊢ ClusterPt f.limsSup f

Tactic:
refine nhds_bot_basis.clusterPt_iff_frequently |>.mpr fun a h => ?_

Premises used: Iff.mpr, nhds_bot_basis, Filter.HasBasis.clusterPt_iff_frequently
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ (x : α), f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
this : OrderBot α := { bot := f.limsSup, bot_le := hbot }
a : α
h : ⊥ < a
⊢ ∃ᶠ (x : α) in f, x ∈ Set.Iio a

Tactic:
lt_mem_sets_of_limsSup_lt hb h |>.frequently

Premises used: Set.Mem, setOf, Filter.Eventually.frequently, Set.Iio, Filter.lt_mem_sets_of_limsSup_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ (x : α), f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
this : OrderBot α := { bot := f.limsSup, bot_le := hbot }
a : α
h : ⊥ < a
⊢ ∃ᶠ (x : α) in f, x ∈ Set.Iio a

Tactic:
exact lt_mem_sets_of_limsSup_lt hb h |>.frequently

Premises used: Filter.Eventually.frequently, Filter.lt_mem_sets_of_limsSup_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ (x : α), f.limsSup < x
hbot : ∃ (x : α), x < f.limsSup
⊢ ClusterPt f.limsSup f

Tactic:
(nhds_basis_Ioo' hbot htop).clusterPt_iff_frequently |>.mpr fun a ⟨hl, hg⟩ => ?_

Premises used: Iff.mpr, Filter.HasBasis.clusterPt_iff_frequently, Membership.mem, Prod.fst, Filter.Frequently, nhds_basis_Ioo', _private.0.ClusterPt.limsSup.match_1, Prod.snd, Set.Ioo
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ (x : α), f.limsSup < x
hbot : ∃ (x : α), x < f.limsSup
neg :
  ∀ (a : α × α),
    a.1 < f.limsSup ∧ f.limsSup < a.2 →
      ∀ (hl : a.1 < f.limsSup) (hg : f.limsSup < a.2), ∃ᶠ (x : α) in f, x ∈ Set.Ioo a.1 a.2
⊢ ClusterPt f.limsSup f

Tactic:
refine (nhds_basis_Ioo' hbot htop).clusterPt_iff_frequently |>.mpr fun a ⟨hl, hg⟩ => ?_

Premises used: Iff.mpr, Filter.HasBasis.clusterPt_iff_frequently, Membership.mem, Prod.fst, Filter.Frequently, nhds_basis_Ioo', _private.0.ClusterPt.limsSup.match_1, Prod.snd, Set.Ioo
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ (x : α), f.limsSup < x
hbot : ∃ (x : α), x < f.limsSup
a : α × α
h : a.1 < f.limsSup ∧ f.limsSup < a.2
hl : a.1 < f.limsSup
hg : f.limsSup < a.2
⊢ ∃ᶠ (x : α) in f, x ∈ Set.Ioo a.1 a.2

Tactic:
frequently_lt_of_lt_limsSup hc hl |>.and_eventually <| lt_mem_sets_of_limsSup_lt hb hg

Premises used: Set.Mem, setOf, Filter.Frequently.and_eventually, Filter.frequently_lt_of_lt_limsSup, Set.Ioo, Filter.lt_mem_sets_of_limsSup_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ (x : α), f.limsSup < x
hbot : ∃ (x : α), x < f.limsSup
a : α × α
h : a.1 < f.limsSup ∧ f.limsSup < a.2
hl : a.1 < f.limsSup
hg : f.limsSup < a.2
⊢ ∃ᶠ (x : α) in f, x ∈ Set.Ioo a.1 a.2

Tactic:
exact frequently_lt_of_lt_limsSup hc hl |>.and_eventually <| lt_mem_sets_of_limsSup_lt hb hg

Premises used: Filter.Frequently.and_eventually, Filter.frequently_lt_of_lt_limsSup, Filter.lt_mem_sets_of_limsSup_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hn : Subsingleton α
⊢ ClusterPt f.limsSup f

Tactic:
simp_all [ClusterPt, Filter.eq_top_of_neBot]

Premises used: ClusterPt, Filter.eq_top_of_neBot
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
⊢ ClusterPt f.limsInf f

Tactic:
ClusterPt.limsSup (α := αᵒᵈ) hc hb

Premises used: Filter.limsInf, ClusterPt.limsSup, setOf, OrderDual
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
x : α
hx : (𝓝 x ⊓ f).NeBot
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ (𝓝 x ⊓ f).limsSup = x

Tactic:
have : (𝓝 x ⊓ f).limsSup = x := limsSup_eq_of_le_nhds inf_le_left
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
x : α
hx : (𝓝 x ⊓ f).NeBot
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
this : (𝓝 x ⊓ f).limsSup = x
⊢ x ≤ f.limsSup

Tactic:
this ▸ limsSup_le_limsSup_of_le inf_le_right ?_ hb

Premises used: inf_le_right, Eq.rec, Filter.limsSup_le_limsSup_of_le
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
x : α
hx : (𝓝 x ⊓ f).NeBot
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
this : (𝓝 x ⊓ f).limsSup = x
refine : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (𝓝 x ⊓ f)
⊢ x ≤ f.limsSup

Tactic:
refine this ▸ limsSup_le_limsSup_of_le inf_le_right ?_ hb
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
x : α
hx : (𝓝 x ⊓ f).NeBot
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
this : (𝓝 x ⊓ f).limsSup = x
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (𝓝 x ⊓ f)

Tactic:
(IsBounded.mono inf_le_left (isBounded_ge_nhds x)).isCobounded_le

Premises used: Filter.IsBounded.mono, isBounded_ge_nhds, Filter.IsBounded.isCobounded_le, inf_le_left
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
x : α
hx : (𝓝 x ⊓ f).NeBot
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
this : (𝓝 x ⊓ f).limsSup = x
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (𝓝 x ⊓ f)

Tactic:
exact (IsBounded.mono inf_le_left (isBounded_ge_nhds x)).isCobounded_le

Premises used: Filter.IsBounded.mono, isBounded_ge_nhds, Filter.IsBounded.isCobounded_le, inf_le_left
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
x : α
hx : ClusterPt x f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
⊢ f.limsInf ≤ x

Tactic:
hx.le_limsSup (α := αᵒᵈ)

Premises used: Filter.limsInf, setOf, ClusterPt.le_limsSup, OrderDual
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter α
inst_3 : f.NeBot
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ IsGreatest {x : α | ClusterPt x f} f.limsSup

Tactic:
⟨ClusterPt.limsSup, fun a ha => ha.le_limsSup⟩

Premises used: ClusterPt.limsSup, ClusterPt.le_limsSup, IsGreatest, And.intro