awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
have obtain : ∀ (u : ℕ → E) (u_in : ∀ (n : ℕ), u n ∈ s) (lim_u : Tendsto u atTop (𝓝 a)),
  ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
Tactic: obtain ⟨u : ℕ → E, u_in : ∀ n, u n ∈ s, lim_u : Tendsto u atTop (𝓝 a)⟩ :=
    mem_closure_iff_seq_limit.mp hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
⊢ {x : E | ‖x⁻¹ * a‖ < b 0} ∈ 𝓝 a
have simp_rw : {x : E | dist x a < b 0} ∈ 𝓝 a
Tactic: simp_rw [← dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
have obtain : ∀ (n₀ : ℕ) (hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0),
  ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
Tactic: obtain ⟨n₀, hn₀⟩ : ∃ n₀, ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0 :=
    haveI : { x | ‖x⁻¹ * a‖ < b 0 } ∈ 𝓝 a := by
      simp_rw [← dist_eq_norm_inv_mul]
      exact Metric.ball_mem_nhds _ (b_pos _)
    Filter.tendsto_atTop'.mp lim_u _ this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (hypothesis)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
have lim_z : Tendsto z atTop (𝓝 a)
Tactic: have lim_z : Tendsto z atTop (𝓝 a) := lim_u.comp (tendsto_add_atTop_nat n₀)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (hypothesis)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
have mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
Tactic: have mem_𝓤 : ∀ n, { p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1) } ∈ 𝓤 E := fun n => by
    simpa [← dist_eq_norm_inv_mul] using Metric.dist_mem_uniformity (b_pos <| n + 1)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
have obtain : ∀ (φ : ℕ → ℕ) (φ_extr : StrictMono φ) (hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)),
  ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
Tactic: obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)⟩ :=
    lim_z.cauchySeq.subseq_mem mem_𝓤
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (hypothesis)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
have hw : Tendsto w atTop (𝓝 a)
Tactic: have hw : Tendsto w atTop (𝓝 a) := lim_z.comp φ_extr.tendsto_atTop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
have refine_1 : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a)
Tactic: refine ⟨v, ?_, ?_, hn₀ _ (n₀.le_add_left _), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
refine_1 : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a)
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
have refine_2 : ∀ (n : ℕ), v n ∈ s
Tactic: refine ⟨v, ?_, ?_, hn₀ _ (n₀.le_add_left _), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
refine_1 : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a)
refine_2 : ∀ (n : ℕ), v n ∈ s
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
have refine_3 : ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
Tactic: refine ⟨v, ?_, ?_, hn₀ _ (n₀.le_add_left _), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a)
have apply : ∀ (n : ℕ), w n = ∏ i ∈ range (n + 1), v i
Tactic: apply hw.congr (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n : ℕ
⊢ w n = ∏ i ∈ range (n + 1), v i
have rw : w n = (∏ k ∈ range n, v (k + 1)) * v 0
Tactic: rw [Finset.prod_range_succ']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n : ℕ
⊢ ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n
have apply : ∀ (k : ℕ) (hk : k < n), (v 0)⁻¹ * w (k + 1) = (v 0)⁻¹ * w k * v (k + 1)
Tactic: apply prod_range_induction _ _ (by simp [v]) _ (fun k hk ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n k : ℕ
hk : k < n
⊢ (v 0)⁻¹ * w (k + 1) = (v 0)⁻¹ * w k * v (k + 1)
have simp : (w 0)⁻¹ * w (k + 1) = (w 0)⁻¹ * w k * ((w k)⁻¹ * w (k + 1))
Tactic: simp only [↓reduceIte, Nat.add_eq_zero_iff, one_ne_zero, and_false, add_tsub_cancel_right, v]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (hypothesis)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n : ℕ
⊢ w n = (∏ k ∈ range n, v (k + 1)) * v 0
have this : ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n
Tactic: have : ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n := by
      apply prod_range_induction _ _ (by simp [v]) _ (fun k hk ↦ ?_)
      simp only [↓reduceIte, Nat.add_eq_zero_iff, one_ne_zero, and_false, add_tsub_cancel_right, v]
      group
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ v 0 ∈ s
have refine_2 : w 0 ∈ s
Tactic: change w 0 ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
l : ℕ
hl : 0 < l
⊢ ‖v l‖ < b l
have refine_3 : ∀ (k : ℕ) (hl : 0 < k + 1), ‖v (k + 1)‖ < b (k + 1)
Tactic: obtain ⟨k, rfl⟩ : ∃ k, l = k + 1 := Nat.exists_eq_succ_of_ne_zero hl.ne'
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
k : ℕ
hl : 0 < k + 1
⊢ ‖v (k + 1)‖ < b (k + 1)
have refine_3 : ‖(v (k + 1))⁻¹‖ < b (k + 1)
Tactic: rw [← norm_inv']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
k : ℕ
hl : 0 < k + 1
⊢ ‖(v (k + 1))⁻¹‖ < b (k + 1)
have refine_3 : ‖(w (k + 1))⁻¹ * w k‖ < b (k + 1)
Tactic: simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, add_tsub_cancel_right,
      mul_inv_rev, inv_inv, v]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
F : Type u_5
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑j.range : Set F)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
⊢ ∃ (a : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (a i)) atTop (𝓝 b) ∧
      ‖HMul.hMul (α := F) (((j : (a : E) → F) (a 0))⁻¹ : F) b‖ < f 0 ∧
        ∀ (n : ℕ), 0 < n → norm.{u_5} (E := F) ((j : (a : E) → F) (a n) : F) < f n
have obtain : ∀ (v : ℕ → F) (sum_v : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)) (v_in : ∀ (n : ℕ), v n ∈ j.range)
  (hv₀ : ‖(v 0)⁻¹ * b‖ < f 0) (hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n),
  ∃ (a : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (a i)) atTop (𝓝 b) ∧
      ‖HMul.hMul (α := F) (((j : (a : E) → F) (a 0))⁻¹ : F) b‖ < f 0 ∧
        ∀ (n : ℕ), 0 < n → norm.{u_5} (E := F) ((j : (a : E) → F) (a n) : F) < f n
Tactic: obtain ⟨v, sum_v, v_in, hv₀, hv_pos⟩ := controlled_prod_of_mem_closure hb b_pos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
F : Type u_5
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑j.range : Set F)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
v_in : ∀ (n : ℕ), v n ∈ j.range
hv₀ : ‖(v 0)⁻¹ * b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
⊢ ∃ (a : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (a i)) atTop (𝓝 b) ∧
      ‖HMul.hMul (α := F) (((j : (a : E) → F) (a 0))⁻¹ : F) b‖ < f 0 ∧
        ∀ (n : ℕ), 0 < n → norm.{u_5} (E := F) ((j : (a : E) → F) (a n) : F) < f n
have choose : ∀ (g : (n : ℕ) → E) (hg : ∀ (n : ℕ), (j : (a : E) → F) (g n) = v n),
  ∃ (a : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (a i)) atTop (𝓝 b) ∧
      ‖HMul.hMul (α := F) (((j : (a : E) → F) (a 0))⁻¹ : F) b‖ < f 0 ∧
        ∀ (n : ℕ), 0 < n → norm.{u_5} (E := F) ((j : (a : E) → F) (a n) : F) < f n
Tactic: choose g hg using v_in
Cleared hypotheses: v_in
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : NormedGroup E
a : E
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)
have apply : Tendsto (β := ℝ) (fun (a_1 : E) ↦ ‖a_1⁻¹ * a‖) (𝓟 {a}ᶜ) (𝓟 (Set.Ioi 0))
Tactic: apply (tendsto_norm_inv_mul_self a).inf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : NormedGroup E
a : E
⊢ Tendsto (β := ℝ) (fun (a_1 : E) ↦ ‖a_1⁻¹ * a‖) (𝓟 {a}ᶜ) (𝓟 (Set.Ioi 0))
have apply : ∀ (_x : E) (hx : Membership.mem (γ := Set E) {a}ᶜ _x), _x⁻¹ * a ≠ 1
Tactic: apply tendsto_principal_principal.2 (fun _x hx => norm_pos_iff'.2 ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_7
inst : NormedCommGroup E
a : E
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0)
have simp_rw : Tendsto (β := ℝ) (fun (x : E) ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)
Tactic: simp_rw [← norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ControlledClosure (goal)
Goal:
G : Type u_1
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
H : Type u_2
inst_2 : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have pos : ∀ (hyp_h : h = 0), ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
Tactic: by_cases hyp_h : h = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ControlledClosure (goal)
Goal:
G : Type u_1
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
H : Type u_2
inst_2 : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
pos : ∀ (hyp_h : h = 0), ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have neg : ∀ (hyp_h : ¬h = 0), ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
Tactic: by_cases hyp_h : h = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ControlledClosure (goal)
Goal:
G : Type u_1
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
H : Type u_2
inst_2 : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : h = 0
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have pos : ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) (0 : H) ∧ ‖g‖ ≤ (C + ε) * norm.{u_2} (E := H) 0
Tactic: rw [hyp_h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ControlledClosure (goal)
Goal:
G : Type u_1
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
H : Type u_2
inst_2 : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : h = 0
⊢ ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) (0 : H) ∧ ‖g‖ ≤ (C + ε) * norm.{u_2} (E := H) 0
have h₁ : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) 0 : H) (0 : H) ∧ norm.{u_1} (E := G) 0 ≤ (C + ε) * norm.{u_2} (E := H) 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ControlledClosure (hypothesis)
Goal:
G : Type u_1
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
H : Type u_2
inst_2 : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun (i : ℕ) ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have b_pos : ∀ (i : ℕ), 0 < b i
Tactic: have b_pos (i) : 0 < b i := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ControlledClosure (goal)
Goal:
G : Type u_1
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
H : Type u_2
inst_2 : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun (i : ℕ) ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have neg : ∀ (v : ℕ → H) (lim_v : Tendsto (fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)) (v_in : ∀ (n : ℕ), v n ∈ K)
  (hv₀ : ‖-v 0 + h‖ < b 0) (hv : ∀ n > 0, ‖v n‖ < b n), ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
Tactic: obtain
    ⟨v : ℕ → H, lim_v : Tendsto (fun n : ℕ => ∑ k ∈ range (n + 1), v k) atTop (𝓝 h), v_in :
      ∀ n, v n ∈ K, hv₀ : ‖-v 0 + h‖ < b 0, hv : ∀ n > 0, ‖v n‖ < b n⟩ :=
    controlled_sum_of_mem_closure h_in b_pos