awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
inl :
  ∀ (xt : Ne (α := ℝ≥0∞) 0 ∞), HasBasis (α := ℝ≥0∞) (𝓝 0) (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (0 - ε) (0 + ε)
⊢ (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)
have inr : ∀ (x0 : 0 < x), (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)
Tactic: rcases eq_zero_or_pos x with rfl | x0
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
xt : Ne (α := ℝ≥0∞) 0 ∞
⊢ HasBasis (α := ℝ≥0∞) (𝓝 0) (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (0 - ε) (0 + ε)
have inl : HasBasis (α := ℝ≥0∞) (𝓝 ⊥) (fun (x : ℝ≥0∞) ↦ ⊥ < x) fun (ε : ℝ≥0∞) ↦ Iic ε
Tactic: simp_rw [zero_tsub, zero_add, ← bot_eq_zero, Icc_bot, ← bot_lt_iff_ne_bot]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
⊢ (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)
have inr : ∀ (i : ℝ≥0∞ × ℝ≥0∞), i.1 < x ∧ x < i.2 → ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo i.1 i.2
Tactic: refine (nhds_basis_Ioo' ⟨_, x0⟩ ⟨_, xt.lt_top⟩).to_hasBasis ?_ fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
inr : ∀ (i : ℝ≥0∞ × ℝ≥0∞), i.1 < x ∧ x < i.2 → ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo i.1 i.2
⊢ (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)
have inr₁ : ∀ (ε : ℝ≥0∞) (ε0 : ε ≠ 0), ∃ (i : ℝ≥0∞ × ℝ≥0∞), (i.1 < x ∧ x < i.2) ∧ Ioo i.1 i.2 ⊆ Icc (x - ε) (x + ε)
Tactic: refine (nhds_basis_Ioo' ⟨_, x0⟩ ⟨_, xt.lt_top⟩).to_hasBasis ?_ fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
⊢ ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2
have inr : ∀ (ε : ℝ≥0∞) (ε0 : 0 < ε) (hε : ε < x - (a, b).1), ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2
Tactic: rcases exists_between (tsub_pos_of_lt ha) with ⟨ε, ε0, hε⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
⊢ ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2
have inr : ∀ (δ : ℝ≥0) (δ0 : 0 < δ) (hδ : x + (↑δ : ℝ≥0∞) < (a, b).2),
  ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2
Tactic: rcases lt_iff_exists_add_pos_lt.1 hb with ⟨δ, δ0, hδ⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + (↑δ : ℝ≥0∞) < (a, b).2
⊢ ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2
have inr : (a, b).1 < x - min ε (↑δ : ℝ≥0∞)
Tactic: refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + (↑δ : ℝ≥0∞) < (a, b).2
inr : (a, b).1 < x - min ε (↑δ : ℝ≥0∞)
⊢ ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2
have inr₁ : x + min ε (↑δ : ℝ≥0∞) < (a, b).2
Tactic: refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
⊢ Tendsto u f (𝓝 a)
have refine : Tendsto u f (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 (Icc (a - ε) (a + ε)))
Tactic: refine Tendsto.mono_right ?_ (biInf_le_nhds _)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
⊢ Tendsto (β := ℝ≥0∞) (fun (n : α) ↦ a - f n) l (𝓝 0) ↔ Tendsto (fun (n : α) ↦ f n) l (𝓝 a)
have rw : (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
Tactic: rw [ENNReal.tendsto_nhds_zero, ENNReal.tendsto_nhds ha]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
have refine_1 : ∀ (h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) (ε : ℝ≥0∞) (hε : ε > 0), ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
refine_1 :
  ∀ (h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) (ε : ℝ≥0∞) (hε : ε > 0), ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
have refine_2 : ∀ (h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)) (ε : ℝ≥0∞) (hε : ε > 0), ∀ᶠ (x : α) in l, a - f x ≤ ε
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
have h₁ : ∀ (n : α) (hn : a - f n ≤ ε), f n ∈ Icc (a - ε) (a + ε)
Tactic: filter_upwards [h ε hε] with n hn
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ f n ∈ Icc (a - ε) (a + ε)
have h₁ : a - ε ≤ f n
Tactic: refine ⟨?_, (hfa n).trans (le_add_right le_rfl)⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ a - ε ≤ f n
have h₁ : ∀ (hn : a ≤ ε + f n), a ≤ f n + ε
Tactic: rw [tsub_le_iff_right] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, a - f x ≤ ε
have h₁ : ∀ (n : α) (hn : f n ∈ Icc (a - ε) (a + ε)), a - f n ≤ ε
Tactic: filter_upwards [h ε hε] with n hn
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
⊢ a - f n ≤ ε
have hN_left : a - ε ≤ f n
Tactic: have hN_left := hn.1
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a - ε ≤ f n
⊢ a - f n ≤ ε
have h₁ : ∀ (hN_left : a ≤ f n + ε), a ≤ ε + f n
Tactic: rw [tsub_le_iff_right] at hN_left ⊢
Cleared hypotheses: hN_left
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_2
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), True ∧ ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)
have simp : (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
  ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)
Tactic: simp only [true_and]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_2
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), True ∧ ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε
have simp : (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε
Tactic: simp only [true_and]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
have rw : (∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
Tactic: rw [ENNReal.tendsto_atTop_zero]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
have refine_1 : ∀ (h : ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε) (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (n : β), f n ≤ ε
Tactic: refine ⟨fun h ↦ fun ε hε ↦ ?_, fun h ↦ fun ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
refine_1 : ∀ (h : ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε) (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (n : β), f n ≤ ε
⊢ (∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
have refine_2 : ∀ (h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) (ε : ℝ≥0∞) (hε : ε > 0), ∃ (N : β), ∀ n ≥ N, f n ≤ ε
Tactic: refine ⟨fun h ↦ fun ε hε ↦ ?_, fun h ↦ fun ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (n : β), f n ≤ ε
have refine_1 : ∀ (n : β) (hn : ∀ n_1 ≥ n, f n_1 ≤ ε), ∃ (n : β), f n ≤ ε
Tactic: obtain ⟨n, hn⟩ := h ε hε
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (N : β), ∀ n ≥ N, f n ≤ ε
have refine_2 : ∀ (n : β) (hn : f n ≤ ε), ∃ (N : β), ∀ n ≥ N, f n ≤ ε
Tactic: obtain ⟨n, hn⟩ := h ε hε
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
have rw : (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
Tactic: rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
have mp : (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
mp : (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
have mpr : (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (n : β), f n < ε
have mp : ∀ (n : β) (hn : f n ≤ min 1 (ε / 2)), ∃ (n : β), f n < ε
Tactic: obtain ⟨n, hn⟩ := h (min 1 (ε / 2))
      (lt_min_iff.mpr ⟨zero_lt_one, (ENNReal.div_pos_iff.mpr ⟨hε.ne', by finiteness⟩)⟩)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
⊢ ∃ (n : β), f n < ε
have mp : min 1 (ε / 2) < ε
Tactic: refine ⟨n, hn.trans_lt ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
⊢ min 1 (ε / 2) < ε
have pos : ∀ (hε_top : ε = ∞), min 1 (ε / 2) < ε
Tactic: by_cases hε_top : ε = ∞
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
pos : ∀ (hε_top : ε = ∞), min 1 (ε / 2) < ε
⊢ min 1 (ε / 2) < ε
have neg : ∀ (hε_top : ¬ε = ∞), min 1 (ε / 2) < ε
Tactic: by_cases hε_top : ε = ∞
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ min 1 (ε / 2) < ε
have neg : ε / 2 < ε
Tactic: refine (min_le_right _ _).trans_lt ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ ε / 2 < ε
have neg : ε < ε * 2
Tactic: rw [ENNReal.div_lt_iff (Or.inr hε.ne') (Or.inr hε_top)]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
| ε
have rw : ε * 1
Tactic: rw [← mul_one ε]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ ε < ε * 2
have neg : ε * 1 < ε * 2
Tactic: conv_lhs => rw [← mul_one ε]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ ε * 1 < ε * 2
have neg : LT.lt (α := ℝ≥0∞) 1 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (n : β), f n ≤ ε
have mpr : ∀ (n : β) (hn : f n < ε), ∃ (n : β), f n ≤ ε
Tactic: obtain ⟨n, hn⟩ := h ε hε
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
b : ℝ≥0
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) (𝓝 (∞, (↑b : ℝ≥0∞))) (𝓝 (∞ - (↑b : ℝ≥0∞)))
have rw : ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, (↑b : ℝ≥0∞)), (↑x : ℝ≥0∞) < a.1 - a.2
Tactic: rw [top_sub_coe, tendsto_nhds_top_iff_nnreal]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
b : ℝ≥0
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, (↑b : ℝ≥0∞)), (↑x : ℝ≥0∞) < a.1 - a.2
have refine : ∀ (x : ℝ≥0) (y : ℝ≥0∞ × ℝ≥0∞) (hy : (↑(b + 1 + x) : ℝ≥0∞) < y.1 ∧ y.2 ≤ (↑(b + 1) : ℝ≥0∞)), (↑x : ℝ≥0∞) < y.1 - y.2
Tactic: refine fun x => ((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds
      (ge_mem_nhds <| coe_lt_coe.2 <| lt_add_one b)).mono fun y hy => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
b : ℝ≥0
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : (↑(b + 1 + x) : ℝ≥0∞) < y.1 ∧ y.2 ≤ (↑(b + 1) : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞) < y.1 - y.2
have grw : (↑(b + 1) : ℝ≥0∞) + (↑x : ℝ≥0∞) < y.1
Tactic: grw [lt_tsub_iff_left, hy.2]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0
h : (↑a : ℝ≥0∞) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) (𝓝 ((↑a : ℝ≥0∞), ∞)) (𝓝 0)
have refine : ∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 ((↑a : ℝ≥0∞), ∞), x.1 - x.2 = 0
Tactic: refine (tendsto_pure.2 ?_).mono_right (pure_le_nhds _)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ≥0
h : (↑a : ℝ≥0∞) ≠ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) (𝓝 ((↑a : ℝ≥0∞), (↑b : ℝ≥0∞))) (𝓝 ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)))
have simp : Tendsto (fun (a : ℝ≥0 × ℝ≥0) ↦ a.1 - a.2) (𝓝 (a, b)) (𝓝 (a - b))
Tactic: simp only [nhds_coe_coe, tendsto_map'_iff, ← ENNReal.coe_sub, Function.comp_def, tendsto_coe]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
⊢ Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
have refine : ∀ (n : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2
Tactic: refine tendsto_nhds_top_iff_nnreal.2 fun n => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2
have rcases : ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ≥0∞)) (hεb : (↑ε : ℝ≥0∞) < b), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2
Tactic: rcases lt_iff_exists_nnreal_btwn.1 (pos_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < (↑ε : ℝ≥0∞)
hεb : (↑ε : ℝ≥0∞) < b
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2
have this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2
Tactic: have : ∀ᶠ c : ℝ≥0∞ × ℝ≥0∞ in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2 :=
      (lt_mem_nhds <| div_lt_top coe_ne_top hε.ne').prod_nhds (lt_mem_nhds hεb)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < (↑ε : ℝ≥0∞)
hεb : (↑ε : ℝ≥0∞) < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2
have refine : ∀ (c : ℝ≥0∞ × ℝ≥0∞) (hc : (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2), (↑n : ℝ≥0∞) < c.1 * c.2
Tactic: refine this.mono fun c hc => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
have ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
Tactic: have ht : ∀ b : ℝ≥0∞, b ≠ 0 →
      Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞) := fun b hb => by
    refine tendsto_nhds_top_iff_nnreal.2 fun n => ?_
    rcases lt_iff_exists_nnreal_btwn.1 (pos_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩
    have : ∀ᶠ c : ℝ≥0∞ × ℝ≥0∞ in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2 :=
      (lt_mem_nhds <| div_lt_top coe_ne_top hε.ne').prod_nhds (lt_mem_nhds hεb)
    refine this.mono fun c hc => ?_
    exact (ENNReal.div_mul_cancel hε.ne' coe_ne_top).symm.trans_lt (mul_lt_mul hc.1 hc.2)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
a b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 (∞ * b))
have hb₁ : ¬b = 0
Tactic: simp only [ne_eq, or_false, not_true_eq_false] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
a_1 b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
ha : (↑a : ℝ≥0∞) ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞
hb : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), ∞)) (𝓝 ((↑a : ℝ≥0∞) * ∞))
have ha₁ : ¬(↑a : ℝ≥0∞) = 0
Tactic: simp only [ne_eq, or_false, not_true_eq_false] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a_1 b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
ha : (↑a : ℝ≥0∞) ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), b)) (𝓝 ((↑a : ℝ≥0∞) * b))
have coe : ∀ (ha : (↑a : ℝ≥0∞) ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞) (hb : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞),
  Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), ∞)) (𝓝 ((↑a : ℝ≥0∞) * ∞))
Tactic: induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a_1 b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
ha : (↑a : ℝ≥0∞) ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞
coe :
  ∀ (ha : (↑a : ℝ≥0∞) ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞) (hb : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞),
    Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), ∞)) (𝓝 ((↑a : ℝ≥0∞) * ∞))
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), b)) (𝓝 ((↑a : ℝ≥0∞) * b))
have coe₁ : ∀ (b : ℝ≥0) (ha : (↑a : ℝ≥0∞) ≠ 0 ∨ (↑b : ℝ≥0∞) ≠ ∞) (hb : (↑b : ℝ≥0∞) ≠ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞),
  Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), (↑b : ℝ≥0∞))) (𝓝 ((↑a : ℝ≥0∞) * (↑b : ℝ≥0∞)))
Tactic: induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
have top : ∀ (ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ b ≠ ∞) (hb : b ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞),
  Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 (∞ * b))
Tactic: induction a with
  | top => simp only [ne_eq, or_false, not_true_eq_false] at hb; simp [ht b hb, top_mul hb]
  | coe a =>
    induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]
Cleared hypotheses: ha, hb