awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
a : α
f : α → β
rw : ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ici a) a
rw₁ : ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a
have rw₂ : ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a ↔
  ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
Tactic: rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic,
    continuousAt_iff_continuous_left_right]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
s : Set α
a : α
f : α → β
⊢ ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ioi a) a
have rw : ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
Tactic: rw [continuousWithinAt_inter_Ioi_iff_Ici, continuousWithinAt_inter_Iio_iff_Iic,
    continuousWithinAt_iff_continuous_left_right]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
s : Set α
a : α
f : α → β
rw : ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
⊢ ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ioi a) a
have rw₁ : ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
Tactic: rw [continuousWithinAt_inter_Ioi_iff_Ici, continuousWithinAt_inter_Iio_iff_Iic,
    continuousWithinAt_iff_continuous_left_right]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRight (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
s : Set α
a : α
f : α → β
rw : ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
rw₁ : ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
⊢ ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ioi a) a
have rw₂ : ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a ↔
  ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
Tactic: rw [continuousWithinAt_inter_Ioi_iff_Ici, continuousWithinAt_inter_Iio_iff_Iic,
    continuousWithinAt_iff_continuous_left_right]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
⊢ β
have haveI : (this : Nonempty β) → β
Tactic: haveI : Nonempty β := ⟨f a⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
⊢ β
have haveI : (this : Nonempty β) → β
Tactic: classical
  haveI : Nonempty β := ⟨f a⟩
  letI : TopologicalSpace α := Preorder.topology α
  exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = y
have h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
Tactic: have h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y) := ⟨y, h'⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = y
have h₁ : 𝓝[<] a ≠ ⊥
Tactic: rw [h'α.topology_eq_generate_intervals] at h h' h''
Cleared hypotheses: h, h', h''
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h₁ : 𝓝[<] a ≠ ⊥
⊢ leftLim f a = y
have h'₁ : Tendsto f (𝓝[<] a) (𝓝 y)
Tactic: rw [h'α.topology_eq_generate_intervals] at h h' h''
Cleared hypotheses: h, h', h''
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h₁ : 𝓝[<] a ≠ ⊥
h'₁ : Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = y
have h''₁ : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
Tactic: rw [h'α.topology_eq_generate_intervals] at h h' h''
Cleared hypotheses: h, h', h''
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = y
have simp : (𝓝[<] a).limUnder f = y
Tactic: simp only [leftLim, h, h'', not_true, or_self_iff, if_false]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ (𝓝[<] a).limUnder f = y
have this : (𝓝[<] a).NeBot
Tactic: haveI := neBot_iff.2 h
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[<] a = ⊥
⊢ leftLim f a = f a
have h₁ : 𝓝[<] a = ⊥
Tactic: rw [h'α.topology_eq_generate_intervals] 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 β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ¬∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = f a
have h₁ : ¬∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
Tactic: rw [h'α.topology_eq_generate_intervals] 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 β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
⊢ leftLim f a = f a
have this : OrderTopology α
Tactic: have : OrderTopology α := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ leftLim f a = f a
have h : 𝓝[<] a = ⊥
Tactic: apply leftLim_eq_of_eq_bot
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ Iio a = ∅
have simp : IsMin a
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ 𝓝[<] a = ⊥
have this₁ : Iio a = ∅
Tactic: have : Iio a = ∅ := by simp; grind [IsBot, IsMin]
-- 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 : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
⊢ leftLim f a = f a
have inl : ∀ (h' : 𝓝[<] a = ⊥), leftLim f a = f a
Tactic: rcases eq_or_ne (𝓝[<] a) ⊥ 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 : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
inl : ∀ (h' : 𝓝[<] a = ⊥), leftLim f a = f a
⊢ leftLim f a = f a
have inr : ∀ (h' : 𝓝[<] a ≠ ⊥), leftLim f a = f a
Tactic: rcases eq_or_ne (𝓝[<] a) ⊥ 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 : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
h' : 𝓝[<] a ≠ ⊥
⊢ leftLim f a = f a
have inr : Tendsto f (𝓝[<] a) (𝓝 (f a))
Tactic: apply leftLim_eq_of_tendsto 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 α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
have inl : ∀ (h' : 𝓝[<] a = ⊥), Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
Tactic: rcases eq_or_neBot (𝓝[<] a) 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 α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
inl : ∀ (h' : 𝓝[<] a = ⊥), Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
have inr : ∀ (h' : (𝓝[<] a).NeBot), Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
Tactic: rcases eq_or_neBot (𝓝[<] a) 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 α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h' : (𝓝[<] a).NeBot
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
have inr : ∀ (h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)) (h' : (𝓝[<] a).NeBot), Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
Tactic: rw [h'α.topology_eq_generate_intervals] at h h' ⊢
Cleared hypotheses: 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 α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h' : (𝓝[<] a).NeBot
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
have inr : Tendsto f (𝓝[<] a) (𝓝 ((𝓝[<] a).limUnder f))
Tactic: simp only [leftLim, neBot_iff.1 h', h, not_true_eq_false, or_self, ↓reduceIte]
-- 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 α
f : α → β
a : α
⊢ (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
have refine : ∀ (s : Set β) (hs : s ∈ 𝓝 (f a)) (s' : Set β) (hs' : s' ∈ map f (𝓝[≤] a)), (s ∩ s').Nonempty
Tactic: refine inf_neBot_iff.mpr (fun s hs s' hs' ↦ ?_)
-- 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 α
f : α → β
a : α
s : Set β
hs : s ∈ 𝓝 (f a)
s' : Set β
hs' : s' ∈ map f (𝓝[≤] a)
⊢ (s ∩ s').Nonempty
have refine : f a ∈ s'
Tactic: refine ⟨f a, mem_of_mem_nhds hs, ?_⟩
-- 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 α
f : α → β
a : α
s : Set β
hs : s ∈ 𝓝 (f a)
s' : Set β
hs' : s' ∈ map f (𝓝[≤] a)
⊢ f a ∈ s'
have hs'₁ : f ⁻¹' s' ∈ 𝓝[≤] a
Tactic: simp only [mem_map] at hs'
Cleared hypotheses: hs'
-- 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 α
f : α → β
a : α
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f
have A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
Tactic: have A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot := by
    refine inf_neBot_iff.mpr (fun s hs s' hs' ↦ ?_)
    refine ⟨f a, mem_of_mem_nhds hs, ?_⟩
    simp only [mem_map] at hs'
    apply mem_of_mem_nhdsWithin self_mem_Iic hs'
-- 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 α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f
have inl : ∀ (h' : 𝓝[<] a = ⊥), MapClusterPt (leftLim f a) (𝓝[≤] a) f
Tactic: rcases eq_or_neBot (𝓝[<] a) 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 α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
inl : ∀ (h' : 𝓝[<] a = ⊥), MapClusterPt (leftLim f a) (𝓝[≤] a) f
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f
have inr : ∀ (h' : (𝓝[<] a).NeBot), MapClusterPt (leftLim f a) (𝓝[≤] a) f
Tactic: rcases eq_or_neBot (𝓝[<] a) 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 α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
h' : (𝓝[<] a).NeBot
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f
have pos : ∀ (H : ¬∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)), MapClusterPt (leftLim f a) (𝓝[≤] a) f
Tactic: by_cases! H : ¬ ∃ y, Tendsto f (𝓝[<] a) (𝓝 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 α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
h' : (𝓝[<] a).NeBot
pos : ∀ (H : ¬∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)), MapClusterPt (leftLim f a) (𝓝[≤] a) f
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f
have neg : ∀ (H : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)), MapClusterPt (leftLim f a) (𝓝[≤] a) f
Tactic: by_cases! H : ¬ ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
-- 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 α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
h' : (𝓝[<] a).NeBot
H : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f
have this : MapClusterPt (leftLim f a) (𝓝[<] a) f
Tactic: have : MapClusterPt (f.leftLim a) (𝓝[<] a) f := (tendsto_leftLim_of_tendsto H).mapClusterPt
-- 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))
⊢ 𝓝[≤] a = 𝓝[<] a ⊔ pure a
have rw : 𝓝[<] a ⊔ 𝓝[Icc a a] a = 𝓝[<] a ⊔ pure a
Tactic: rw [← Iio_union_Icc_eq_Iic le_rfl, nhdsWithin_union]
-- 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))
⊢ ContinuousWithinAt (leftLim f) (Iic a) a
have this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
Tactic: have : 𝓝[≤] a = 𝓝[<] a ⊔ pure a := by
    rw [← Iio_union_Icc_eq_Iic le_rfl, nhdsWithin_union]
    simp
-- 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
⊢ ContinuousWithinAt (leftLim f) (Iic a) a
have rw : Tendsto (leftLim f) (𝓝[<] a) (𝓝 (leftLim f a)) ∧ Tendsto (leftLim f) (pure a) (𝓝 (leftLim f a))
Tactic: rw [ContinuousWithinAt, this, tendsto_sup]
-- 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
⊢ Tendsto (leftLim f) (𝓝[<] a) (𝓝 (leftLim f a)) ∧ Tendsto (leftLim f) (pure a) (𝓝 (leftLim f a))
have simp : Tendsto (leftLim f) (𝓝[<] a) (𝓝 (leftLim f a))
Tactic: simp only [tendsto_pure_nhds, and_true]
-- 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
⊢ Tendsto (leftLim f) (𝓝[<] a) (𝓝 (leftLim f a))
have apply : ∀ (i : Set β), i ∈ 𝓝 (leftLim f a) ∧ IsClosed[inst_1] i → ∀ᶠ (x : α) in 𝓝[<] a, leftLim 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 (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
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
have inl : ∀ (h' : 𝓝[<] a = ⊥), ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
Tactic: rcases eq_or_neBot (𝓝[<] a) 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 β
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
inl : ∀ (h' : 𝓝[<] a = ⊥), ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
have inr : ∀ (h' : (𝓝[<] a).NeBot), ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
Tactic: rcases eq_or_neBot (𝓝[<] a) 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 β
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
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
have inr : ∀ (b : α) (hb : b ∈ Iio a), ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
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 (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))
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 < 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))
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
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
have inr : ∀ (u : α) (au : u < a) (hu : Ioo u a ⊆ {x : α | f x ∈ s}), ∀ᶠ (x : α) in 𝓝[<] a, leftLim 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))
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}
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
have h₁ : ∀ (c : α) (hc : c ∈ Ioo u a), leftLim 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))
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
⊢ leftLim f c ∈ id s
have h₁ : ∀ (h'c : 𝓝[<] c = ⊥), leftLim 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))
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₁ : ∀ (h'c : 𝓝[<] c = ⊥), leftLim f c ∈ id s
⊢ leftLim f c ∈ id s
have h₂ : ∀ (h'c : (𝓝[<] c).NeBot), leftLim 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))
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
⊢ leftLim f c ∈ id s
have pos : ∀ (h''c : ¬∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)), leftLim 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))
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
pos : ∀ (h''c : ¬∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)), leftLim f c ∈ id s
⊢ leftLim f c ∈ id s
have neg : ∀ (h''c : ∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)), leftLim f c ∈ id s
Tactic: by_cases! h''c : ¬ ∃ y, Tendsto f (𝓝[<] c) (𝓝 y)