awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ IsLeast {x : α | ClusterPt x f} f.limsInf

Tactic:
isGreatest_clusterPt_limsSup (α := αᵒᵈ)

Premises used: Filter.limsInf, lowerBounds, Set.Mem, setOf, IsLeast, isGreatest_clusterPt_limsSup, OrderDual
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
u : β → α
f : Filter β
inst_3 : f.NeBot
hc : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
hb : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ MapClusterPt (Filter.limsup u f) f u

Tactic:
ClusterPt.limsSup

Premises used: ClusterPt.limsSup, Filter.limsup, MapClusterPt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
u : β → α
f : Filter β
inst_3 : f.NeBot
hc : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hb : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ MapClusterPt (Filter.liminf u f) f u

Tactic:
ClusterPt.limsInf

Premises used: Filter.liminf, ClusterPt.limsInf, MapClusterPt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
u : β → α
f : Filter β
x : α
hx : MapClusterPt x f u
hb : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ x ≤ Filter.limsup u f

Tactic:
hx.le_limsSup

Premises used: ClusterPt.le_limsSup, Filter.limsup
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
u : β → α
f : Filter β
x : α
hx : MapClusterPt x f u
hb : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ Filter.liminf u f ≤ x

Tactic:
hx.limsInf_le

Premises used: Filter.liminf, ClusterPt.limsInf_le
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
u : β → α
f : Filter β
inst_3 : f.NeBot
hc : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
hb : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ IsGreatest {x : α | MapClusterPt x f u} (limsup u f)

Tactic:
isGreatest_clusterPt_limsSup

Premises used: setOf, Filter.limsup, isGreatest_clusterPt_limsSup, MapClusterPt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
u : β → α
f : Filter β
inst_3 : f.NeBot
hc : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hb : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ IsLeast {x : α | MapClusterPt x f u} (liminf u f)

Tactic:
isLeast_clusterPt_limsInf

Premises used: Filter.liminf, setOf, MapClusterPt, isLeast_clusterPt_limsInf
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : liminf u f = a
hsup : limsup u f = a
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ Tendsto u f (𝓝 a)

Tactic:
le_nhds_of_limsSup_eq_limsInf h h' hsup hinf

Premises used: Filter.Tendsto, le_nhds_of_limsSup_eq_limsInf
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
inl :
  ∀ (hinf : a ≤ liminf u ⊥) (hsup : limsup u ⊥ ≤ a) (h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) ⊥ u)
    (h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) ⊥ u), Tendsto u ⊥ (𝓝 a)
inr : f.NeBot → Tendsto u f (𝓝 a)
⊢ Tendsto u f (𝓝 a)

Tactic:
rcases f.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
u : β → α
a : α
hinf : a ≤ liminf u ⊥
hsup : limsup u ⊥ ≤ a
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) ⊥ u
⊢ Tendsto u ⊥ (𝓝 a)

Tactic:
tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
u : β → α
a : α
hinf : a ≤ liminf u ⊥
hsup : limsup u ⊥ ≤ a
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) ⊥ u
⊢ Tendsto u ⊥ (𝓝 a)

Tactic:
exact tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h_1 : f.NeBot
⊢ Tendsto u f (𝓝 a)

Tactic:
tendsto_of_liminf_eq_limsup (le_antisymm (le_trans (liminf_le_limsup h h') hsup) hinf)
      (le_antisymm hsup (le_trans hinf (liminf_le_limsup h h'))) h h'

Premises used: tendsto_of_liminf_eq_limsup, le_antisymm, Filter.liminf_le_limsup, le_trans
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h_1 : f.NeBot
⊢ Tendsto u f (𝓝 a)

Tactic:
exact tendsto_of_liminf_eq_limsup (le_antisymm (le_trans (liminf_le_limsup h h') hsup) hinf)
      (le_antisymm hsup (le_trans hinf (liminf_le_limsup h h'))) h h'

Premises used: tendsto_of_liminf_eq_limsup, le_antisymm, Filter.liminf_le_limsup, le_trans
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
inl :
  ∀ (H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n))
    (h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) ⊥ u) (h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) ⊥ u),
    ∃ (c : α), Tendsto u ⊥ (𝓝 c)
inr : ∀ (hbot : f.NeBot), ∃ (c : α), Tendsto u f (𝓝 c)
⊢ ∃ (c : α), Tendsto u f (𝓝 c)

Tactic:
rcases f.eq_or_neBot with rfl | hbot

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) ⊥ u
⊢ ∃ (c : α), Tendsto u ⊥ (𝓝 c)

Tactic:
⟨sInf ∅, tendsto_bot⟩

Premises used: Filter.tendsto_bot, Exists.intro, EmptyCollection.emptyCollection, InfSet.sInf
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) ⊥ u
⊢ ∃ (c : α), Tendsto u ⊥ (𝓝 c)

Tactic:
exact ⟨sInf ∅, tendsto_bot⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
⊢ ∃ (c : α), Tendsto u f (𝓝 c)

Tactic:
⟨limsup u f, ?_⟩

Premises used: Filter.limsup, Exists.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
inr : Tendsto u f (𝓝 (limsup u f))
⊢ ∃ (c : α), Tendsto u f (𝓝 c)

Tactic:
refine ⟨limsup u f, ?_⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
apply : limsup u f ≤ liminf u f
⊢ Tendsto u f (𝓝 (limsup u f))

Tactic:
apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h'

Premises used: le_rfl, tendsto_of_le_liminf_of_limsup_le
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
by_contra! : ∀ (hlt : liminf u f < limsup u f), False
⊢ limsup u f ≤ liminf u f

Tactic:
by_contra! hlt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
⊢ ∃ (a : α), (liminf u f < a ∧ a < limsup u f) ∧ a ∈ s

Tactic:
dense_iff_inter_open.1 hs (Set.Ioo (f.liminf u) (f.limsup u)) isOpen_Ioo
      (Set.nonempty_Ioo.2 hlt)

Premises used: Iff.mpr, Filter.liminf, Set.Mem, isOpen_Ioo, setOf, Set.nonempty_Ioo, Set.inter, Filter.limsup, Set.Nonempty, dense_iff_inter_open, Iff.mp, Set.Ioo
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
obtain : ∀ (a : α) (as : a ∈ s) (la : liminf u f < a) (au : a < limsup u f), False
⊢ False

Tactic:
obtain ⟨a, ⟨⟨la, au⟩, as⟩⟩ : ∃ a, (f.liminf u < a ∧ a < f.limsup u) ∧ a ∈ s :=
    dense_iff_inter_open.1 hs (Set.Ioo (f.liminf u) (f.limsup u)) isOpen_Ioo
      (Set.nonempty_Ioo.2 hlt)

Premises used: Iff.mpr, Filter.liminf, isOpen_Ioo, Set.nonempty_Ioo, Filter.limsup, dense_iff_inter_open, Iff.mp, Set.Ioo
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
⊢ ∃ (b : α), (a < b ∧ b < limsup u f) ∧ b ∈ s

Tactic:
dense_iff_inter_open.1 hs (Set.Ioo a (f.limsup u)) isOpen_Ioo (Set.nonempty_Ioo.2 au)

Premises used: Iff.mpr, Set.Mem, isOpen_Ioo, setOf, Set.nonempty_Ioo, Set.inter, Filter.limsup, Set.Nonempty, dense_iff_inter_open, Iff.mp, Set.Ioo
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
obtain : ∀ (b : α) (bs : b ∈ s) (ab : a < b) (bu : b < limsup u f), False
⊢ False

Tactic:
obtain ⟨b, ⟨⟨ab, bu⟩, bs⟩⟩ : ∃ b, (a < b ∧ b < f.limsup u) ∧ b ∈ s :=
    dense_iff_inter_open.1 hs (Set.Ioo a (f.limsup u)) isOpen_Ioo (Set.nonempty_Ioo.2 au)

Premises used: Iff.mpr, isOpen_Ioo, Set.nonempty_Ioo, Filter.limsup, dense_iff_inter_open, Iff.mp, Set.Ioo
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
⊢ ∃ᶠ (n : β) in f, u n < a

Tactic:
have A : ∃ᶠ n in f, u n < a := frequently_lt_of_liminf_lt (IsBounded.isCobounded_ge h) la
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
⊢ ∃ᶠ (n : β) in f, b < u n

Tactic:
have B : ∃ᶠ n in f, b < u n := frequently_lt_of_lt_limsup (IsBounded.isCobounded_le h') bu
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
B : ∃ᶠ (n : β) in f, b < u n
⊢ False

Tactic:
H a as b bs ab ⟨A, B⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
B : ∃ᶠ (n : β) in f, b < u n
⊢ False

Tactic:
exact H a as b bs ab ⟨A, B⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
f : Filter α
inst_4 : f.NeBot
inst_5 : f.IsCountablyGenerated
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ ∃ (x : ℕ → α), Tendsto x atTop (𝓝 f.limsSup) ∧ Tendsto x atTop f

Tactic:
(ClusterPt.limsSup).exists_seq_tendsto

Premises used: ClusterPt.limsSup, ClusterPt.exists_seq_tendsto
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
f : Filter α
inst_4 : f.NeBot
inst_5 : f.IsCountablyGenerated
hc : IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
hb : IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
⊢ ∃ (x : ℕ → α), Tendsto x atTop (𝓝 f.limsInf) ∧ Tendsto x atTop f

Tactic:
(ClusterPt.limsInf).exists_seq_tendsto

Premises used: ClusterPt.exists_seq_tendsto, ClusterPt.limsInf
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
f : Filter β
inst_4 : f.NeBot
inst_5 : f.IsCountablyGenerated
u : β → α
hc : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
hb : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ ∃ (x : ℕ → β), Tendsto (u ∘ x) atTop (𝓝 (limsup u f)) ∧ Tendsto x atTop f

Tactic:
(MapClusterPt.limsup).exists_seq_tendsto

Premises used: MapClusterPt.limsup, MapClusterPt.exists_seq_tendsto
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
f : Filter β
inst_4 : f.NeBot
u : β → α
inst_5 : f.IsCountablyGenerated
hc : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
hb : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ ∃ (x : ℕ → β), Tendsto (u ∘ x) atTop (𝓝 (liminf u f)) ∧ Tendsto x atTop f

Tactic:
(MapClusterPt.liminf).exists_seq_tendsto

Premises used: MapClusterPt.exists_seq_tendsto, MapClusterPt.liminf
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
f : Filter β
inst_4 : CountableInterFilter f
u : β → α
hf : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
rw : ∀ (b : α), limsup u f < b → ∀ᶠ (x : β) in f, u x < b
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f

Tactic:
rw [eventually_le_const_iff_forall_gt_eventually_lt_const]

Premises used: eventually_le_const_iff_forall_gt_eventually_lt_const
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
f : Filter β
inst_4 : CountableInterFilter f
u : β → α
hf : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ ∀ (b : α), limsup u f < b → ∀ᶠ (x : β) in f, u x < b

Tactic:
fun _ hc ↦ eventually_lt_of_limsup_lt hc

Premises used: Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
f : Filter β
inst_4 : CountableInterFilter f
u : β → α
hf : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ ∀ (b : α), limsup u f < b → ∀ᶠ (x : β) in f, u x < b

Tactic:
exact fun _ hc ↦ eventually_lt_of_limsup_lt hc

Premises used: Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
f : Filter β
inst_4 : CountableInterFilter f
u : β → α
hf : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ ∀ᶠ (b : β) in f, liminf u f ≤ u b

Tactic:
eventually_le_limsup (α := αᵒᵈ) hf

Premises used: Filter.limsInf, Filter.liminf, setOf, eventually_le_limsup, OrderDual
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : FirstCountableTopology α
inst_3 : OrderTopology α
f : Filter β
inst_4 : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
rw : Eq.{u_2 + 1} (α := α) (limsup ⊥ f) ⊥
⊢ limsup u f = ⊥

Tactic:
rw [limsup_congr h]

Premises used: Filter.limsup_congr
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : FirstCountableTopology α
inst_3 : OrderTopology α
f : Filter β
inst_4 : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ Eq.{u_2 + 1} (α := α) (limsup ⊥ f) ⊥

Tactic:
limsup_const_bot

Premises used: Filter.limsup_const_bot
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : FirstCountableTopology α
inst_3 : OrderTopology α
f : Filter β
inst_4 : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ Eq.{u_2 + 1} (α := α) (limsup ⊥ f) ⊥

Tactic:
exact limsup_const_bot

Premises used: Filter.limsup_const_bot
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : FirstCountableTopology α
inst_3 : OrderTopology α
f : Filter β
inst_4 : CountableInterFilter f
u : β → α
⊢ liminf u f = ⊤ ↔ u =ᶠ[f] ⊤

Tactic:
limsup_eq_bot (α := αᵒᵈ)

Premises used: Filter.limsInf, Filter.liminf, setOf, limsup_eq_bot, OrderDual
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
inl : ∀ (hι : IsEmpty ι), Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)
inr : ∀ (n0 : ι), Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)
⊢ Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)

Tactic:
rcases isEmpty_or_nonempty ι with hι | ⟨⟨n0⟩⟩

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
hι : IsEmpty ι
⊢ Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)

Tactic:
simpa using h_limsup
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
⊢ Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)

Tactic:
tendsto_order.mpr ⟨fun b hb ↦ ?_, fun b hb ↦ ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro