awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
⊢ HasBasis (α := α) (⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |b / a|ₘ < r}) (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦
    {b : α | |b / a|ₘ < ε}
have refine : ∀ (x : α) (hx : x > 1) (y : α) (hy : y > 1),
  ∃ k > 1,
    Subset.{u_1} (α := Set α) {b : α | |b / a|ₘ < k} {b : α | |b / a|ₘ < x} ∧
      Subset.{u_1} (α := Set α) {b : α | |b / a|ₘ < k} {b : α | |b / a|ₘ < y}
Tactic: refine hasBasis_biInf_principal' (fun x hx y hy => ?_) (exists_gt _)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦ Ioo (a / ε) (a * ε)
have h : ∀ (x : α), Ioo (a / x) (a * x) = {b : α | |b / a|ₘ < x}
Tactic: convert! nhds_basis_mabs_div_lt a
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ Ioo (a / min a ε) (a * min a ε) ⊆ Ioo (a / ε) (a * ε)
have ha₁ : min a ε ≤ ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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 : α
⊢ BoundedLENhdsClass (α × β)
have refine : ∀ (x : α × β), IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)
Tactic: refine ⟨fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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 : α
x : α × β
⊢ IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)
have obtain : ∀ (a : α) (ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a), IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)
Tactic: obtain ⟨a, ha⟩ := isBounded_le_nhds x.1
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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_1 : α
x : α × β
a : α
ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a
⊢ IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)
have obtain : ∀ (b : β) (hb : ∀ᶠ (x : β) in 𝓝 x.2, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b), IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)
Tactic: obtain ⟨b, hb⟩ := isBounded_le_nhds x.2
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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_1 : α
x : α × β
a : α
ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a
b : β
hb : ∀ᶠ (x : β) in 𝓝 x.2, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
⊢ IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)
have rw : IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x.1 ×ˢ 𝓝 x.2)
Tactic: rw [← @Prod.mk.eta _ _ x, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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)
⊢ BoundedLENhdsClass ((i : ι) → π i)
have refine : ∀ (x : (i : ι) → π i), IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (𝓝 x)
Tactic: refine ⟨fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (𝓝 x)
have rw : IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (pi (α := π) fun (i : ι) ↦ 𝓝 (x i))
Tactic: rw [nhds_pi]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (pi (α := π) fun (i : ι) ↦ 𝓝 (x i))
have 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))
Tactic: choose f hf using fun i ↦ isBounded_le_nhds (x i)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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.limsSup f
have pos : ∀ (hn : Nontrivial α), ClusterPt f.limsSup f
Tactic: by_cases! hn : Nontrivial α
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ ClusterPt f.limsSup f
have neg : ∀ (hn : Subsingleton α), ClusterPt f.limsSup f
Tactic: by_cases! hn : Nontrivial α
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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 α
⊢ ClusterPt f.limsSup f
have pos : ∀ (htop : ∀ (x : α), x ≤ f.limsSup), ClusterPt f.limsSup f
Tactic: by_cases! htop : ∀ x, x ≤ f.limsSup
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ ClusterPt f.limsSup f
have neg : ∀ (htop : ∃ (x : α), f.limsSup < x), ClusterPt f.limsSup f
Tactic: by_cases! htop : ∀ x, x ≤ f.limsSup
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ ClusterPt f.limsSup f
have pos : ∀ (hbot : ∀ (x : α), f.limsSup ≤ x), ClusterPt f.limsSup f
Tactic: by_cases! hbot : ∀ x, f.limsSup ≤ x
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ ClusterPt f.limsSup f
have neg : ∀ (hbot : ∃ (x : α), x < f.limsSup), ClusterPt f.limsSup f
Tactic: by_cases! hbot : ∀ x, f.limsSup ≤ x
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
have pos : ∀ (a : α) (h : ⊥ < a), ∃ᶠ (x : α) in f, x ∈ Set.Iio a
Tactic: refine nhds_bot_basis.clusterPt_iff_frequently |>.mpr fun a h => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
have 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
Tactic: refine (nhds_basis_Ioo' hbot htop).clusterPt_iff_frequently |>.mpr fun a ⟨hl, hg⟩ => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
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
have this : (𝓝 x ⊓ f).limsSup = x
Tactic: have : (𝓝 x ⊓ f).limsSup = x := limsSup_eq_of_le_nhds inf_le_left
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
have refine : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (𝓝 x ⊓ f)
Tactic: refine this ▸ limsSup_le_limsSup_of_le inf_le_right ?_ hb
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ Tendsto u f (𝓝 a)
have 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)
Tactic: rcases f.eq_or_neBot with rfl | _
Cleared hypotheses: f, hinf, hsup, h, h'
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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)
⊢ Tendsto u f (𝓝 a)
have inr : f.NeBot → Tendsto u f (𝓝 a)
Tactic: rcases f.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ ∃ (c : α), Tendsto u f (𝓝 c)
have 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)
Tactic: rcases f.eq_or_neBot with rfl | hbot
Cleared hypotheses: f, H, h, h'
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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)
⊢ ∃ (c : α), Tendsto u f (𝓝 c)
have inr : ∀ (hbot : f.NeBot), ∃ (c : α), Tendsto u f (𝓝 c)
Tactic: rcases f.eq_or_neBot with rfl | hbot
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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)
have inr : Tendsto u f (𝓝 (limsup u f))
Tactic: refine ⟨limsup u f, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ Tendsto u f (𝓝 (limsup u f))
have apply : limsup u f ≤ liminf u f
Tactic: apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h'
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ limsup u f ≤ liminf u f
have by_contra! : ∀ (hlt : liminf u f < limsup u f), False
Tactic: by_contra! hlt
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ False
have obtain : ∀ (a : α) (as : a ∈ s) (la : liminf u f < a) (au : a < limsup u f), 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)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ False
have obtain : ∀ (b : α) (bs : b ∈ s) (ab : a < b) (bu : b < limsup u f), 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)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
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
⊢ False
have A : ∃ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
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
⊢ False
have B : ∃ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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, u b ≤ limsup u f
have rw : ∀ (b : α), limsup u f < b → ∀ᶠ (x : β) in f, u x < b
Tactic: rw [eventually_le_const_iff_forall_gt_eventually_lt_const]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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] ⊥
⊢ limsup u f = ⊥
have rw : Eq.{u_2 + 1} (α := α) (limsup ⊥ f) ⊥
Tactic: rw [limsup_congr h]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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)
⊢ Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)
have inl : ∀ (hι : IsEmpty ι), Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)
Tactic: rcases isEmpty_or_nonempty ι with hι | ⟨⟨n0⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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)
⊢ Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)
have inr : ∀ (n0 : ι), Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)
Tactic: rcases isEmpty_or_nonempty ι with hι | ⟨⟨n0⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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)
have inr : ∀ (b : β) (hb : b < c), ∀ᶠ (b_1 : α) in atTop, b < ⨆ (i : ι), u i b_1
Tactic: refine tendsto_order.mpr ⟨fun b hb ↦ ?_, fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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 : ι
inr : ∀ (b : β) (hb : b < c), ∀ᶠ (b_1 : α) in atTop, b < ⨆ (i : ι), u i b_1
⊢ Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)
have inr₁ : ∀ (b : β) (hb : b > c), ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
Tactic: refine tendsto_order.mpr ⟨fun b hb ↦ ?_, fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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 : ι
b : β
hb : b < c
⊢ ∀ᶠ (b_1 : α) in atTop, b < ⨆ (i : ι), u i b_1
have inr : ∀ (r : α), b < ⨆ (i : ι), u i r
Tactic: filter_upwards with r
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
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 : ι
b : β
hb : b < c
r : α
⊢ b < ⨆ (i : ι), u i r
have this : c ≤ u n0 r
Tactic: have : c ≤ u n0 r := (h_anti n0).le_of_tendsto (h_all n0) r
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
⊢ (if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c) < b
have pos : ∀ (h : (Set.Ioo c b).Nonempty), h.some (s := Set.Ioo c b) < b
Tactic: split_ifs with h