awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
Ax : hs.extend (s := s) f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
Ay : hs.extend (s := s) f y = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
⊢ Membership.mem (γ := Set (α × α))
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2} (x, y)
have simp : edist (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)) ≤
  (↑K : ℝ≥0∞) * edist x y
Tactic: simp only [Set.mem_setOf_eq, Ax, Ay]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
⊢ LipschitzWith K (hs.extend (s := s) f)
have this₁ : Dense.{u_4} (X := α × α)
  {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
Tactic: have : Dense {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
    apply (hs.prod hs).mono
    rintro ⟨x, y⟩ ⟨hx, hy⟩
    have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩
    have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩
    simp only [Set.mem_setOf_eq, Ax, Ay]
    exact hf ⟨x, hx⟩ ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
n : ℕ∞
h : n ≠ ⊤
⊢ 𝓝 n = pure n
have lift : ∀ (n : ℕ), Eq (α := Filter ℕ∞) (𝓝 (↑n : ℕ∞)) (pure (↑n : ℕ∞))
Tactic: lift n to ℕ using h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
x : ℕ∞
hx : x ≠ ⊤
⊢ IsOpen (X := ℕ∞) {x}
have rw : 𝓝 x = pure x
Tactic: rw [isOpen_singleton_iff_nhds_eq_pure, ENat.nhds_eq_pure hx]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
x : ℕ∞
hx : x ≠ ⊤
rw : 𝓝 x = pure x
⊢ IsOpen (X := ℕ∞) {x}
have rw₁ : Eq (α := Filter ℕ∞) (pure x) (pure x)
Tactic: rw [isOpen_singleton_iff_nhds_eq_pure, ENat.nhds_eq_pure hx]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
have simp_rw : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l < ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
Tactic: simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top,
    mem_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℕ∞
simp_rw : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l < ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
have simp_rw₁ : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l ≠ ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
Tactic: simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top,
    mem_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℕ∞
simp_rw : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l < ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₁ : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l ≠ ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
have simp_rw₂ : (∀ (i : ℕ∞) (i_1 : i ≠ ⊤), Tendsto f l (𝓟 (Ioi i))) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
Tactic: simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top,
    mem_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℕ∞
simp_rw : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l < ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₁ : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l ≠ ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₂ : (∀ (i : ℕ∞) (i_1 : i ≠ ⊤), Tendsto f l (𝓟 (Ioi i))) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
have simp_rw₃ : (∀ (i : ℕ∞) (i_1 : i ≠ ⊤), ∀ᶠ (a : α) in l, f a ∈ Ioi i) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
Tactic: simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top,
    mem_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℕ∞
simp_rw : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l < ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₁ : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l ≠ ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₂ : (∀ (i : ℕ∞) (i_1 : i ≠ ⊤), Tendsto f l (𝓟 (Ioi i))) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₃ : (∀ (i : ℕ∞) (i_1 : i ≠ ⊤), ∀ᶠ (a : α) in l, f a ∈ Ioi i) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
have simp_rw₄ : (∀ (x : ℕ), ∀ᶠ (a : α) in l, Membership.mem (γ := Set ℕ∞) (Ioi (↑x : ℕ∞)) (f a)) ↔
  ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
Tactic: simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top,
    mem_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
⊢ ContinuousAdd ℕ∞
have refine : ∀ (x : ℕ∞ × ℕ∞) (a b : ℕ∞), ContinuousAt (Y := ℕ∞) (fun (p : ℕ∞ × ℕ∞) ↦ p.1 + p.2) (a, b)
Tactic: refine ⟨continuous_iff_continuousAt.2 fun (a, b) ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a : ℕ∞
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (a, ⊤)
have inl : ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (0, ⊤)
Tactic: rcases eq_zero_or_pos a with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a : ℕ∞
inl : ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (0, ⊤)
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (a, ⊤)
have inr : ∀ (ha : 0 < a), ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (a, ⊤)
Tactic: rcases eq_zero_or_pos a with rfl | ha
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a : ℕ∞
ha : 0 < a
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (a, ⊤)
have inr : Tendsto (α := ℕ∞ × ℕ∞) (β := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (𝓝 (a, ⊤)) (𝓝 ⊤)
Tactic: simp only [ContinuousAt, Function.uncurry, mul_top ha.ne']
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a : ℕ∞
ha : 0 < a
⊢ Tendsto (α := ℕ∞ × ℕ∞) (β := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (𝓝 (a, ⊤)) (𝓝 ⊤)
have inr : EventuallyLE (α := ℕ∞ × ℕ∞) (𝓝 (a, ⊤)) Prod.snd (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2)
Tactic: refine tendsto_nhds_top_mono continuousAt_snd ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a : ℕ∞
ha : 0 < a
x y : ℕ∞
⊢ Membership.mem (γ := Set (ℕ∞ × ℕ∞)) (Prod.fst ⁻¹' {x : ℕ∞ | 0 < x}) (x, y) →
    (x, y).2 ≤ Function.uncurry (fun (x1 x2 : ℕ∞) ↦ x1 * x2) (x, y)
have h : ∀ (hx : 0 < x), (x, y).2 ≤ Function.uncurry (fun (x1 x2 : ℕ∞) ↦ x1 * x2) (x, y)
Tactic: (hx : 0 < x)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a : ℕ∞
ha : 0 < a
⊢ EventuallyLE (α := ℕ∞ × ℕ∞) (𝓝 (a, ⊤)) Prod.snd (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2)
have h : ∀ (x y : ℕ∞) (hx : 0 < x), (x, y).2 ≤ Function.uncurry (fun (x1 x2 : ℕ∞) ↦ x1 * x2) (x, y)
Tactic: filter_upwards [continuousAt_fst (lt_mem_nhds ha)] with (x, y) (hx : 0 < x)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a_1 b : ℕ∞
h : a_1 ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
h_1 : Ne (α := ℕ∞) (↑a : ℕ∞) ⊤ ∨ Ne (α := ℕ∞) ⊤ ⊤
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 - x2) ((↑a : ℕ∞), ⊤)
have suffices : ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, (↑a : ℕ∞) - b = 0
Tactic: suffices ∀ᶠ b in 𝓝 ⊤, (a - b : ℕ∞) = 0 by
      simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a_1 b : ℕ∞
h : a_1 ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
h_1 : Ne (α := ℕ∞) (↑a : ℕ∞) ⊤ ∨ Ne (α := ℕ∞) ⊤ ⊤
⊢ ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, (↑a : ℕ∞) - b = 0
have h₁ : ∀ (a_2 : ℕ∞),
  Membership.mem (γ := Set ℕ∞)
    {x : ℕ∞ |
      Membership.mem (γ := Set ℕ∞) {x : ℕ∞ | (fun (x : ℕ∞) ↦ (↑a : WithTop ℕ) ≤ x) x} x →
        Membership.mem (γ := Set ℕ∞) {x : ℕ∞ | (fun (b : ℕ∞) ↦ (↑a : ℕ∞) - b = 0) x} x}
    a_2
Tactic: filter_upwards [le_mem_nhds (WithTop.coe_lt_top a)] with b using tsub_eq_zero_of_le
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a_1 b : ℕ∞
h : a_1 ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
h_1 : Ne (α := ℕ∞) (↑a : ℕ∞) ⊤ ∨ Ne (α := ℕ∞) ⊤ ⊤
h₁ :
  ∀ (a_2 : ℕ∞),
    Membership.mem (γ := Set ℕ∞)
      {x : ℕ∞ |
        Membership.mem (γ := Set ℕ∞) {x : ℕ∞ | (fun (x : ℕ∞) ↦ (↑a : WithTop ℕ) ≤ x) x} x →
          Membership.mem (γ := Set ℕ∞) {x : ℕ∞ | (fun (b : ℕ∞) ↦ (↑a : ℕ∞) - b = 0) x} x}
      a_2
⊢ ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, (↑a : ℕ∞) - b = 0
have h₂ : ∀ (a_2 : ℕ∞), (↑a : WithTop ℕ) ≤ a_2 → (↑a : ℕ∞) - a_2 = 0
Tactic: filter_upwards [le_mem_nhds (WithTop.coe_lt_top a)] with b using tsub_eq_zero_of_le
-- Lean 4 proof step from Mathlib.Topology.Instances.ENat (goal)
Goal:
a b_1 : ℕ∞
h : a ≠ ⊤ ∨ b_1 ≠ ⊤
b : ℕ
h_1 : Ne (α := ℕ∞) ⊤ ⊤ ∨ Ne (α := ℕ∞) (↑b : ℕ∞) ⊤
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 - x2) (⊤, (↑b : ℕ∞))
have suffices : ∀ (n : ℕ), ∀ᶠ (a : ℕ∞) in 𝓝 ⊤, HAdd.hAdd (α := ℕ∞) (↑b : ℕ∞) (↑n : ℕ∞) < a
Tactic: suffices ∀ n : ℕ, ∀ᶠ a : ℕ∞ in 𝓝 ⊤, b + n < a by
      simpa [ContinuousAt, nhds_prod_eq, (· ∘ ·), lt_tsub_iff_left, tendsto_nhds_top_iff_natCast_lt]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ (range Real.toEReal).OrdConnected
have rw : OrdConnected (α := EReal) (Ioo ⊥ ⊤)
Tactic: rw [range_coe_eq_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : EReal
ha : a ≠ ⊤
h'a : a ≠ ⊥
⊢ Tendsto toReal (𝓝 a) (𝓝 a.toReal)
have lift : ∀ (a : ℝ) (ha : (↑a : EReal) ≠ ⊤) (h'a : (↑a : EReal) ≠ ⊥), Tendsto toReal (𝓝 (↑a : EReal)) (𝓝 (↑a : EReal).toReal)
Tactic: lift a to ℝ using ⟨ha, h'a⟩
Cleared hypotheses: a, ha, h'a
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
ha : (↑a : EReal) ≠ ⊤
h'a : (↑a : EReal) ≠ ⊥
⊢ Tendsto toReal (𝓝 (↑a : EReal)) (𝓝 (↑a : EReal).toReal)
have rw : Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a : EReal).toReal)
Tactic: rw [nhds_coe, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ (range ENNReal.toEReal).OrdConnected
have rw : OrdConnected (α := EReal) (Ici 0)
Tactic: rw [range_coe_ennreal]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ IsClosed (range ENNReal.toEReal)
have rw : IsClosed (X := EReal) (Ici 0)
Tactic: rw [range_coe_ennreal]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ HasBasis (α := EReal) (𝓝 ⊤) (fun (x : ℝ) ↦ True) fun (x : ℝ) ↦ Ioi (↑x : EReal)
have refine : ∀ (x : EReal) (hx : x < ⊤), ∃ (i' : ℝ), True ∧ Ioi (↑i' : EReal) ⊆ Ioi x
Tactic: refine (nhds_top_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
hx : x < ⊤
⊢ ∃ (i' : ℝ), True ∧ Ioi (↑i' : EReal) ⊆ Ioi x
have rcases : ∀ (y : ℚ) (hxy : x < (↑(↑y : ℝ) : EReal)), ∃ (i' : ℝ), True ∧ Ioi (↑i' : EReal) ⊆ Ioi x
Tactic: rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ HasBasis (α := EReal) (𝓝 ⊥) (fun (x : ℝ) ↦ True) fun (x : ℝ) ↦ Iio (↑x : EReal)
have refine : ∀ (x : EReal) (hx : ⊥ < x), ∃ (i' : ℝ), True ∧ Iio (↑i' : EReal) ⊆ Iio x
Tactic: refine (_root_.nhds_bot_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
hx : ⊥ < x
⊢ ∃ (i' : ℝ), True ∧ Iio (↑i' : EReal) ⊆ Iio x
have rcases : ∀ (y : ℚ) (hxy : (↑(↑y : ℝ) : EReal) < x), ∃ (i' : ℝ), True ∧ Iio (↑i' : EReal) ⊆ Iio x
Tactic: rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ 𝓝[≠] ⊤ = map Real.toEReal atTop
have h : ∀ i < ⊤, ∃ (i' : ℝ), True ∧ Real.toEReal '' Ici i' ⊆ Ici i ∩ {⊤}ᶜ
Tactic: apply (nhdsWithin_hasBasis nhds_top_basis_Ici _).ext (atTop_basis.map Real.toEReal)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
h : ∀ i < ⊤, ∃ (i' : ℝ), True ∧ Real.toEReal '' Ici i' ⊆ Ici i ∩ {⊤}ᶜ
⊢ 𝓝[≠] ⊤ = map Real.toEReal atTop
have h' : ∀ (i' : ℝ), True → ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Real.toEReal '' Ici i'
Tactic: apply (nhdsWithin_hasBasis nhds_top_basis_Ici _).ext (atTop_basis.map Real.toEReal)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ∀ i < ⊤, ∃ (i' : ℝ), True ∧ Real.toEReal '' Ici i' ⊆ Ici i ∩ {⊤}ᶜ
have h : ∀ i < ⊤, ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici i ∩ {⊤}ᶜ
Tactic: simp only [EReal.image_coe_Ici, true_and]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
hx : x < ⊤
⊢ ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ
have pos : ∀ (hx_bot : x = ⊥), ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ
Tactic: by_cases hx_bot : x = ⊥
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
hx : x < ⊤
pos : ∀ (hx_bot : x = ⊥), ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ
⊢ ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ
have neg : ∀ (hx_bot : ¬x = ⊥), ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ
Tactic: by_cases hx_bot : x = ⊥
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
hx : x < ⊤
hx_bot : ¬x = ⊥
⊢ ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici x ∩ {⊤}ᶜ
have neg : ∀ (x : ℝ) (hx : (↑x : EReal) < ⊤) (hx_bot : ¬(↑x : EReal) = ⊥),
  ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici (↑x : EReal) ∩ {⊤}ᶜ
Tactic: lift x to ℝ using ⟨hx.ne_top, hx_bot⟩
Cleared hypotheses: x, hx, hx_bot
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : ℝ
hx : (↑x : EReal) < ⊤
hx_bot : ¬(↑x : EReal) = ⊥
⊢ ∃ (i' : ℝ), Ico (↑i' : EReal) ⊤ ⊆ Ici (↑x : EReal) ∩ {⊤}ᶜ
have neg : ∀ x_1 ∈ Ico (↑x : EReal) ⊤, ∀ (h1 : (↑x : EReal) ≤ x_1) (h2 : x_1 < ⊤), x_1 ∈ Ici (↑x : EReal) ∩ {⊤}ᶜ
Tactic: refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ∀ (i' : ℝ), True → ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Real.toEReal '' Ici i'
have h' : ∀ (i' : ℝ), ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Ico (↑i' : EReal) ⊤
Tactic: simp only [EReal.image_coe_Ici, true_implies]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ∀ (i' : ℝ), ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Ico (↑i' : EReal) ⊤
have h' : ∀ (x : ℝ),
  ∀ x_1 ∈ Ici (↑x : EReal) ∩ {⊤}ᶜ,
    ∀ (h1 : (↑x : EReal) ≤ x_1) (h2 : Membership.mem (γ := Set EReal) {⊤}ᶜ x_1), x_1 ∈ Ico (↑x : EReal) ⊤
Tactic: refine fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ 𝓝[≠] ⊥ = map Real.toEReal atBot
have h : ∀ (i : EReal), ⊥ < i → ∃ (i' : ℝ), True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ
Tactic: apply (nhdsWithin_hasBasis nhds_bot_basis_Iic _).ext (atBot_basis.map Real.toEReal)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
h : ∀ (i : EReal), ⊥ < i → ∃ (i' : ℝ), True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ
⊢ 𝓝[≠] ⊥ = map Real.toEReal atBot
have h' : ∀ (i' : ℝ), True → ∃ (i : EReal), ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Real.toEReal '' Iic i'
Tactic: apply (nhdsWithin_hasBasis nhds_bot_basis_Iic _).ext (atBot_basis.map Real.toEReal)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ∀ (i : EReal), ⊥ < i → ∃ (i' : ℝ), True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ
have h : ∀ (i : EReal), ⊥ < i → ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic i ∩ {⊥}ᶜ
Tactic: simp only [EReal.image_coe_Iic,
      true_and]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
hx : ⊥ < x
⊢ ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ
have pos : ∀ (hx_top : x = ⊤), ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ
Tactic: by_cases hx_top : x = ⊤
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
hx : ⊥ < x
pos : ∀ (hx_top : x = ⊤), ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ
⊢ ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ
have neg : ∀ (hx_top : ¬x = ⊤), ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ
Tactic: by_cases hx_top : x = ⊤
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
hx : ⊥ < x
hx_top : ¬x = ⊤
⊢ ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic x ∩ {⊥}ᶜ
have neg : ∀ (x : ℝ) (hx : ⊥ < (↑x : EReal)) (hx_top : ¬(↑x : EReal) = ⊤),
  ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic (↑x : EReal) ∩ {⊥}ᶜ
Tactic: lift x to ℝ using ⟨hx_top, hx.ne_bot⟩
Cleared hypotheses: x, hx, hx_top
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : ℝ
hx : ⊥ < (↑x : EReal)
hx_top : ¬(↑x : EReal) = ⊤
⊢ ∃ (i' : ℝ), Ioc ⊥ (↑i' : EReal) ⊆ Iic (↑x : EReal) ∩ {⊥}ᶜ
have neg : ∀ x_1 ∈ Ioc ⊥ (↑x : EReal), ∀ (h1 : ⊥ < x_1) (h2 : x_1 ≤ (↑x : EReal)), x_1 ∈ Iic (↑x : EReal) ∩ {⊥}ᶜ
Tactic: refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ∀ (i' : ℝ), True → ∃ (i : EReal), ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Real.toEReal '' Iic i'
have h' : ∀ (i' : ℝ), ∃ (i : EReal), ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Ioc ⊥ (↑i' : EReal)
Tactic: simp only [EReal.image_coe_Iic, true_implies]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ∀ (i' : ℝ), ∃ (i : EReal), ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Ioc ⊥ (↑i' : EReal)
have h' : ∀ (x : ℝ),
  ∀ x_1 ∈ Iic (↑x : EReal) ∩ {⊥}ᶜ,
    ∀ (h1 : x_1 ≤ (↑x : EReal)) (h2 : Membership.mem (γ := Set EReal) {⊥}ᶜ x_1), x_1 ∈ Ioc ⊥ (↑x : EReal)
Tactic: refine fun x ↦ ⟨x, ⟨EReal.bot_lt_coe x, fun x ⟨(h1 : x ≤ _), h2⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ Tendsto (β := EReal) (fun (x : α) ↦ (↑(f x) : EReal)) l (𝓝 ⊤) ↔ Tendsto f l atTop
have rw : (∀ (x : ℝ), ∀ᶠ (a : α) in l, (↑x : EReal) < (↑(f a) : EReal)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
Tactic: rw [tendsto_nhds_top_iff_real, atTop_basis_Ioi.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ Tendsto (β := EReal) (fun (x : α) ↦ (↑(f x) : EReal)) l (𝓝 ⊥) ↔ Tendsto f l atBot
have rw : (∀ (x : ℝ), ∀ᶠ (a : α) in l, (↑(f a) : EReal) < (↑x : EReal)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Iio i
Tactic: rw [tendsto_nhds_bot_iff_real, atBot_basis_Iio.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ Tendsto toReal (𝓝[≠] ⊤) atTop
have rw : Tendsto (toReal ∘ Real.toEReal) atTop atTop
Tactic: rw [nhdsWithin_top, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ Tendsto toReal (𝓝[≠] ⊥) atBot
have rw : Tendsto (toReal ∘ Real.toEReal) atBot atBot
Tactic: rw [nhdsWithin_bot, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ Continuous toENNReal
have refine : ∀ (x : EReal), ContinuousAt toENNReal x
Tactic: refine continuous_iff_continuousAt.mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
⊢ ContinuousAt toENNReal x
have pos : ∀ (h_top : x = ⊤), ContinuousAt toENNReal x
Tactic: by_cases h_top : x = ⊤
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
pos : ∀ (h_top : x = ⊤), ContinuousAt toENNReal x
⊢ ContinuousAt toENNReal x
have neg : ∀ (h_top : ¬x = ⊤), ContinuousAt toENNReal x
Tactic: by_cases h_top : x = ⊤
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
h_top : x = ⊤
⊢ ContinuousAt toENNReal x
have pos : Tendsto toENNReal (𝓝 ⊤) (𝓝 ∞)
Tactic: simp only [ContinuousAt, h_top, toENNReal_top]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
h_top : x = ⊤
⊢ Tendsto toENNReal (𝓝 ⊤) (𝓝 ∞)
have pos : ∀ (n : ℕ), ∀ᶠ (a : EReal) in 𝓝 ⊤, (↑n : ℝ≥0∞) < a.toENNReal
Tactic: refine ENNReal.tendsto_nhds_top fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
h_top : x = ⊤
n : ℕ
⊢ ∀ᶠ (a : EReal) in 𝓝 ⊤, (↑n : ℝ≥0∞) < a.toENNReal
have h : ∀ (y : EReal) (hy : (↑(↑n : ℝ) : EReal) < y), (↑n : ℝ≥0∞) < y.toENNReal
Tactic: filter_upwards [eventually_gt_nhds (coe_lt_top n)] with y hy
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousAt toENNReal x
have neg : ContinuousOn toENNReal {⊤}ᶜ
Tactic: refine ContinuousOn.continuousAt ?_ (compl_singleton_mem_nhds_iff.mpr h_top)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousOn toENNReal {⊤}ᶜ
have neg : ∀ (x : EReal) (hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x),
  ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
Tactic: refine (continuousOn_of_forall_continuousAt fun x hx ↦ ?_).congr (fun _ h ↦ toENNReal_of_ne_top h)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
have pos : ∀ (h_bot : x = ⊥), ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
Tactic: by_cases h_bot : x = ⊥
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
pos : ∀ (h_bot : x = ⊥), ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
have neg : ∀ (h_bot : ¬x = ⊥), ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
Tactic: by_cases h_bot : x = ⊥
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : x = ⊥
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
have pos : ∀ᶠ (x' : EReal) in 𝓝 x, ENNReal.ofReal x'.toReal = (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
Tactic: refine tendsto_nhds_of_eventually_eq ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : x = ⊥
⊢ ∀ᶠ (x' : EReal) in 𝓝 x, ENNReal.ofReal x'.toReal = (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
have pos : ∃ (i : ℝ),
  True ∧ ∀ ⦃x : EReal⦄, x ∈ Iio (↑i : EReal) → ENNReal.ofReal x.toReal = (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) ⊥
Tactic: rw [h_bot, nhds_bot_basis.eventually_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : ¬x = ⊥
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
have neg : x ∉ {⊥, ⊤}
Tactic: refine ENNReal.continuous_ofReal.continuousAt.comp' <| continuousOn_toReal.continuousAt
    <| (toFinite _).isClosed.compl_mem_nhds ?_