awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)
⊢ leftLim f c ∈ id s
have neg : ∀ᶠ (x : α) in 𝓝[<] c, f x ∈ s
Tactic: apply s_closed.mem_of_tendsto (tendsto_leftLim_of_tendsto h''c)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)
⊢ ∀ᶠ (x : α) in 𝓝[<] c, f x ∈ s
have h₁ : ∀ (a_1 : α),
  Membership.mem (γ := Set α) {x : α | x ∈ Ioo u a → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x}
    a_1
Tactic: filter_upwards [Ioo_mem_nhdsLT_of_mem ⟨hc.1, hc.2.le⟩] with d hd using hu hd
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α | x ∈ Ioo u a → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x} a_1
⊢ ∀ᶠ (x : α) in 𝓝[<] c, f x ∈ s
have h₂ : ∀ a_1 ∈ Ioo u a, f a_1 ∈ s
Tactic: filter_upwards [Ioo_mem_nhdsLT_of_mem ⟨hc.1, hc.2.le⟩] with d hd using hu hd
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
⊢ leftLim (rightLim f) a = leftLim f a
have obtain : ∀ (b : α) (hb : b ∈ Iio a), leftLim (rightLim f) a = leftLim f a
Tactic: obtain ⟨b, hb⟩ : (Iio a).Nonempty := Filter.nonempty_of_mem (self_mem_nhdsWithin (a := a))
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
⊢ leftLim (rightLim f) a = leftLim f a
have apply : Tendsto (rightLim f) (𝓝[<] a) (𝓝 (leftLim f a))
Tactic: apply leftLim_eq_of_tendsto (neBot_iff.mp h')
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
⊢ Tendsto (rightLim f) (𝓝[<] a) (𝓝 (leftLim f a))
have apply : ∀ (i : Set β), i ∈ 𝓝 (leftLim f a) ∧ IsClosed[inst_1] i → ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id i
Tactic: apply (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.2
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
⊢ ∃ u < a, Ioo u a ⊆ {x : α | f x ∈ s}
have this : ∀ᶠ (x : α) in 𝓝[<] a, f x ∈ id s
Tactic: have := (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.1 h s ⟨s_mem, s_closed⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id s
have obtain : ∀ (u : α) (au : u < a) (hu : Ioo u a ⊆ {x : α | f x ∈ s}), ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id s
Tactic: obtain ⟨u, au, hu⟩ : ∃ u, u < a ∧ Ioo u a ⊆ {x | f x ∈ s} := by
    have := (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.1 h s ⟨s_mem, s_closed⟩
    simpa using (mem_nhdsLT_iff_exists_Ioo_subset' hb).1 this
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
⊢ ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id s
have h₁ : ∀ (c : α) (hc : c ∈ Ioo u a), rightLim f c ∈ id s
Tactic: filter_upwards [Ioo_mem_nhdsLT au] with c hc
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
⊢ rightLim f c ∈ id s
have h₁ : ∀ (h'c : 𝓝[>] c = ⊥), rightLim f c ∈ id s
Tactic: rcases eq_or_neBot (𝓝[>] c) with h'c | h'c
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h₁ : ∀ (h'c : 𝓝[>] c = ⊥), rightLim f c ∈ id s
⊢ rightLim f c ∈ id s
have h₂ : ∀ (h'c : (𝓝[>] c).NeBot), rightLim f c ∈ id s
Tactic: rcases eq_or_neBot (𝓝[>] c) with h'c | h'c
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
⊢ rightLim f c ∈ id s
have pos : ∀ (h''c : ¬∃ (y : β), Tendsto f (𝓝[>] c) (𝓝 y)), rightLim f c ∈ id s
Tactic: by_cases! h''c : ¬ ∃ y, Tendsto f (𝓝[>] c) (𝓝 y)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
pos : ∀ (h''c : ¬∃ (y : β), Tendsto f (𝓝[>] c) (𝓝 y)), rightLim f c ∈ id s
⊢ rightLim f c ∈ id s
have neg : ∀ (h''c : ∃ (y : β), Tendsto f (𝓝[>] c) (𝓝 y)), rightLim f c ∈ id s
Tactic: by_cases! h''c : ¬ ∃ y, Tendsto f (𝓝[>] c) (𝓝 y)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
h''c : ∃ (y : β), Tendsto f (𝓝[>] c) (𝓝 y)
⊢ rightLim f c ∈ id s
have neg : ∀ᶠ (x : α) in 𝓝[>] c, f x ∈ s
Tactic: apply s_closed.mem_of_tendsto (tendsto_rightLim_of_tendsto h''c)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
h''c : ∃ (y : β), Tendsto f (𝓝[>] c) (𝓝 y)
⊢ ∀ᶠ (x : α) in 𝓝[>] c, f x ∈ s
have h₁ : ∀ (a_1 : α),
  Membership.mem (γ := Set α) {x : α | x ∈ Ioo u a → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x}
    a_1
Tactic: filter_upwards [Ioo_mem_nhdsGT_of_mem ⟨hc.1.le, hc.2⟩] with d hd using hu hd
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
h''c : ∃ (y : β), Tendsto f (𝓝[>] c) (𝓝 y)
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α | x ∈ Ioo u a → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x} a_1
⊢ ∀ᶠ (x : α) in 𝓝[>] c, f x ∈ s
have h₂ : ∀ a_1 ∈ Ioo u a, f a_1 ∈ s
Tactic: filter_upwards [Ioo_mem_nhdsGT_of_mem ⟨hc.1.le, hc.2⟩] with d hd using hu hd
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
⊢ Tendsto g atTop (𝓝 b)
have inl : ∀ (hα : IsEmpty α), Tendsto g atTop (𝓝 b)
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
inl : ∀ (hα : IsEmpty α), Tendsto g atTop (𝓝 b)
⊢ Tendsto g atTop (𝓝 b)
have inr : ∀ (hα : Nonempty α), Tendsto g atTop (𝓝 b)
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
⊢ Tendsto g atTop (𝓝 b)
have inr : ∀ (i : Set β), i ∈ 𝓝 b ∧ IsClosed[inst_1] i → ∀ᶠ (x : α) in atTop, g x ∈ id i
Tactic: apply (closed_nhds_basis b).tendsto_right_iff.2
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
⊢ ∀ᶠ (x : α) in atTop, g x ∈ id s
have inr : ∀ (u : α) (hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s), ∀ᶠ (x : α) in atTop, g x ∈ id s
Tactic: obtain ⟨u, hu⟩ : ∃ a, ∀ (b : α), a ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s := by
    simpa [eventually_atTop] using h'.and (h s_mem)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
⊢ a ∈ Ioi u → g a ∈ id s
have h₁ : ∀ (ha : u < a), g a ∈ id s
Tactic: (ha : u < a)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
⊢ ∀ᶠ (x : α) in atTop, g x ∈ id s
have h₁ : ∀ (a : α) (ha : u < a), g a ∈ id s
Tactic: filter_upwards [Ioi_mem_atTop u] with a (ha : u < a)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
⊢ g a ∈ id s
have h₁ : ∀ᶠ (x : α) in 𝓝 a, f x ∈ s
Tactic: apply s_closed.mem_of_mapClusterPt (hu a ha.le).1
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
⊢ ∀ᶠ (x : α) in 𝓝 a, f x ∈ s
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α) {x : α | x ∈ Ici u → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x} a
Tactic: filter_upwards [Ici_mem_nhds ha] with y hy using (hu y hy).2
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α) {x : α | x ∈ Ici u → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x}
      a
⊢ ∀ᶠ (x : α) in 𝓝 a, f x ∈ s
have h₂ : ∀ a ∈ Ici u, f a ∈ s
Tactic: filter_upwards [Ici_mem_nhds ha] with y hy using (hu y hy).2
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : NoTopOrder α
inst_5 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
⊢ Tendsto (leftLim f) atTop (𝓝 b)
have apply : ∀ (x : α), MapClusterPt (leftLim f x) (𝓝 x) f
Tactic: apply tendsto_atTop_of_mapClusterPt h (Eventually.of_forall (fun x ↦ ?_))
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
⊢ Tendsto (rightLim f) atTop (𝓝 b)
have inl : ∀ (val : OrderTop α), Tendsto (rightLim f) atTop (𝓝 b)
Tactic: cases topOrderOrNoTopOrder α
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
inl : ∀ (val : OrderTop α), Tendsto (rightLim f) atTop (𝓝 b)
⊢ Tendsto (rightLim f) atTop (𝓝 b)
have inr : NoTopOrder α → Tendsto (rightLim f) atTop (𝓝 b)
Tactic: cases topOrderOrNoTopOrder α
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
val : OrderTop α
⊢ Tendsto (rightLim f) atTop (𝓝 b)
have inl : ∀ (h : Tendsto f (pure ⊤) (𝓝 b)), Tendsto (rightLim f) (pure ⊤) (𝓝 b)
Tactic: simp only [OrderTop.atTop_eq α] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
b : β
val : OrderTop α
h : Tendsto f (pure ⊤) (𝓝 b)
⊢ Tendsto (rightLim f) (pure ⊤) (𝓝 b)
have this : rightLim f ⊤ = f ⊤
Tactic: have : f.rightLim ⊤ = f ⊤ := rightLim_eq_of_isTop isTop_top
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
b : β
val : OrderTop α
h : Tendsto f (pure ⊤) (𝓝 b)
this : rightLim f ⊤ = f ⊤
⊢ Tendsto (rightLim f) (pure ⊤) (𝓝 b)
have inl : Tendsto (rightLim f) (pure ⊤) (𝓝 (rightLim f ⊤))
Tactic: rw [tendsto_nhds_unique h (tendsto_pure_nhds f ⊤), ← this]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
val : NoTopOrder α
⊢ Tendsto (rightLim f) atTop (𝓝 b)
have apply : ∀ (x : α), MapClusterPt (rightLim f x) (𝓝 x) f
Tactic: apply tendsto_atTop_of_mapClusterPt h (Eventually.of_forall (fun x ↦ ?_))
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this : TopologicalSpace α := Preorder.topology α
⊢ leftLim f x ≤ f y
have this₁ : OrderTopology α
Tactic: haveI : OrderTopology α := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ leftLim f x ≤ f y
have inl : ∀ (h' : 𝓝[<] x = ⊥), leftLim f x ≤ f y
Tactic: rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
inl : ∀ (h' : 𝓝[<] x = ⊥), leftLim f x ≤ f y
⊢ leftLim f x ≤ f y
have inr : ∀ (h' : 𝓝[<] x ≠ ⊥), leftLim f x ≤ f y
Tactic: rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
⊢ leftLim f x ≤ f y
have A : (𝓝[<] x).NeBot
Tactic: haveI A : NeBot (𝓝[<] x) := neBot_iff.2 h'
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
⊢ leftLim f x ≤ f y
have inr : sSup (f '' Iio x) ≤ f y
Tactic: rw [leftLim_eq_sSup hf h']
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
⊢ sSup (f '' Iio x) ≤ f y
have inr : (f '' Iio x).Nonempty
Tactic: refine csSup_le ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
inr : (f '' Iio x).Nonempty
⊢ sSup (f '' Iio x) ≤ f y
have inr₁ : ∀ b ∈ f '' Iio x, b ≤ f y
Tactic: refine csSup_le ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
⊢ (f '' Iio x).Nonempty
have inr : (Iio x).Nonempty
Tactic: simp only [image_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
⊢ ∀ b ∈ f '' Iio x, b ≤ f y
have inr : ∀ a < x, f a ≤ f y
Tactic: simp only [mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this : TopologicalSpace α := Preorder.topology α
⊢ f x ≤ leftLim f y
have this₁ : OrderTopology α
Tactic: haveI : OrderTopology α := ⟨rfl⟩