awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
b_pos : ∀ (i : ℕ), 0 < b i
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‖
have this : ∀ (n : ℕ), ∃ (m' : G), (f : (a : G) → H) m' = v n ∧ ‖m'‖ ≤ C * ‖v n‖
Tactic: have : ∀ n, ∃ m' : G, f m' = v n ∧ ‖m'‖ ≤ C * ‖v n‖ := fun n : ℕ => hyp (v n) (v_in n)
-- 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
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
this : ∀ (n : ℕ), ∃ (m' : G), (f : (a : G) → H) m' = v n ∧ ‖m'‖ ≤ C * ‖v n‖
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have neg : ∀ (u : (n : ℕ) → G) (hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n) (hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖),
  ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
Tactic: choose u hu hnorm_u using this
Cleared hypotheses: this
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
⊢ CauchySeq s
have apply : ∀ n ≥ 1, ‖u n‖ ≤ ε * ‖h‖ / 2 * (1 / 2) ^ n
Tactic: apply NormedAddCommGroup.cauchy_series_of_le_geometric'' (by simp) one_half_lt_one
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
apply : ∀ n ≥ 1, ‖u n‖ ≤ ε * ‖h‖ / 2 * (1 / 2) ^ n
apply₁ : ℝ
⊢ CauchySeq s
have apply₂ : ℕ
Tactic: apply NormedAddCommGroup.cauchy_series_of_le_geometric'' (by simp) one_half_lt_one
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
n : ℕ
hn : n ≥ 1
⊢ C * ‖v n‖ ≤ C * b n
have hbc : ‖v n‖ ≤ b n
Tactic: gcongr
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
n : ℕ
hn : n ≥ 1
⊢ ‖u n‖ ≤ ε * ‖h‖ / 2 * (1 / 2) ^ n
have C₁ : C * ‖v n‖ ≤ C * b n
Tactic: calc
        ‖u n‖ ≤ C * ‖v n‖ := hnorm_u n
        _ ≤ C * b n := by gcongr; exact (hv _ <| Nat.succ_le_iff.mp hn).le
        _ = (1 / 2) ^ n * (ε * ‖h‖ / 2) := by simp [b, mul_div_cancel₀ _ hC.ne.symm]
        _ = ε * ‖h‖ / 2 * (1 / 2) ^ n := mul_comm _ _
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
n : ℕ
hn : n ≥ 1
C₁ : C * ‖v n‖ ≤ C * b n
⊢ ‖u n‖ ≤ ε * ‖h‖ / 2 * (1 / 2) ^ n
have C₂ : C * b n = (1 / 2) ^ n * (ε * ‖h‖ / 2)
Tactic: calc
        ‖u n‖ ≤ C * ‖v n‖ := hnorm_u n
        _ ≤ C * b n := by gcongr; exact (hv _ <| Nat.succ_le_iff.mp hn).le
        _ = (1 / 2) ^ n * (ε * ‖h‖ / 2) := by simp [b, mul_div_cancel₀ _ hC.ne.symm]
        _ = ε * ‖h‖ / 2 * (1 / 2) ^ n := mul_comm _ _
-- 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
b_pos : ∀ (i : ℕ), 0 < b i
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have this : CauchySeq s
Tactic: have : CauchySeq s := by
    apply NormedAddCommGroup.cauchy_series_of_le_geometric'' (by simp) one_half_lt_one
    · rintro n (hn : n ≥ 1)
      calc
        ‖u n‖ ≤ C * ‖v n‖ := hnorm_u n
        _ ≤ C * b n := by gcongr; exact (hv _ <| Nat.succ_le_iff.mp hn).le
        _ = (1 / 2) ^ n * (ε * ‖h‖ / 2) := by simp [b, mul_div_cancel₀ _ hC.ne.symm]
        _ = ε * ‖h‖ / 2 * (1 / 2) ^ n := mul_comm _ _
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have neg : ∀ (g : G) (hg : Tendsto s atTop (𝓝 g)), ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
Tactic: obtain ⟨g : G, hg⟩ := cauchySeq_tendsto_of_complete this
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have neg : (f : (a : G) → H) g = h
Tactic: refine ⟨g, ?_, ?_⟩
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
neg : (f : (a : G) → H) g = h
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
have neg₁ : ‖g‖ ≤ (C + ε) * ‖h‖
Tactic: refine ⟨g, ?_, ?_⟩
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ Eq.{u_2 + 1} (α := ℕ → H) ((⇑f : (a : G) → H) ∘ s) fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), v k
have h₁ : ∀ (n : ℕ), Eq.{u_2 + 1} (α := H) (((⇑f : (a : G) → H) ∘ s) n) (∑ k ∈ range (n + 1), v k)
Tactic: ext n
-- 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
b_pos : ∀ (i : ℕ), 0 < b i
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ (f : (a : G) → H) g = h
have this₁ : Eq.{u_2 + 1} (α := ℕ → H) ((⇑f : (a : G) → H) ∘ s) fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), v k
Tactic: have : f ∘ s = fun n => ∑ k ∈ range (n + 1), v k := by
      ext n
      simp [s, map_sum, hu]
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this_1 : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
this : Eq.{u_2 + 1} (α := ℕ → H) ((⇑f : (a : G) → H) ∘ s) fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), v k
⊢ (f : (a : G) → H) g = h
have neg : ∀ (lim_v : Tendsto ((⇑f : (a : G) → H) ∘ s) atTop (𝓝 h)) (this : CauchySeq s) (g : G) (hg : Tendsto s atTop (𝓝 g))
  (this : Eq.{u_2 + 1} (α := ℕ → H) ((⇑f : (a : G) → H) ∘ s) fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), v k),
  (f : (a : G) → H) g = h
Tactic: rw [← this] at lim_v
Cleared hypotheses: lim_v, this_1, g, hg, this
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ‖g‖ ≤ (C + ε) * ‖h‖
have neg : ∀ (n : ℕ), ‖s n‖ ≤ (C + ε) * ‖h‖
Tactic: suffices ∀ n, ‖s n‖ ≤ (C + ε) * ‖h‖ from
      le_of_tendsto' (continuous_norm.continuousAt.tendsto.comp hg) this
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖h‖ + ‖v 0 - h‖ ≤ ‖h‖ + b 0
have rw : ‖h‖ + ‖-v 0 + h‖ ≤ ‖h‖ + b 0
Tactic: rw [← norm_neg_add]
-- 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
b_pos : ∀ (i : ℕ), 0 < b i
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖u 0‖ ≤ C * b 0 + C * ‖h‖
have this₁ : ‖v 0‖ ≤ ‖h‖ + b 0
Tactic: have :=
        calc
          ‖v 0‖ ≤ ‖h‖ + ‖v 0 - h‖ := norm_le_insert' _ _
          _ ≤ ‖h‖ + b 0 := by rw [← norm_neg_add]; gcongr
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this_1 : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
⊢ C * ‖v 0‖ ≤ C * (‖h‖ + b 0)
have ha : 0 ≤ C
Tactic: gcongr
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this_1 : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
⊢ C * (‖h‖ + b 0) = C * b 0 + C * ‖h‖
have rw : C * (b 0 + ‖h‖) = C * b 0 + C * ‖h‖
Tactic: rw [add_comm, mul_add]
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this_1 : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
rw : C * (b 0 + ‖h‖) = C * b 0 + C * ‖h‖
⊢ C * (‖h‖ + b 0) = C * b 0 + C * ‖h‖
have rw₁ : C * b 0 + C * ‖h‖ = C * b 0 + C * ‖h‖
Tactic: rw [add_comm, mul_add]
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this_1 : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
⊢ ‖u 0‖ ≤ C * b 0 + C * ‖h‖
have C₁ : C * ‖v 0‖ ≤ C * (‖h‖ + b 0)
Tactic: calc
        ‖u 0‖ ≤ C * ‖v 0‖ := hnorm_u 0
        _ ≤ C * (‖h‖ + b 0) := by gcongr
        _ = C * b 0 + C * ‖h‖ := by rw [add_comm, mul_add]
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this_1 : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
C₁ : C * ‖v 0‖ ≤ C * (‖h‖ + b 0)
⊢ ‖u 0‖ ≤ C * b 0 + C * ‖h‖
have C₂ : C * (‖h‖ + b 0) = C * b 0 + C * ‖h‖
Tactic: calc
        ‖u 0‖ ≤ C * ‖v 0‖ := hnorm_u 0
        _ ≤ C * (‖h‖ + b 0) := by gcongr
        _ = C * b 0 + C * ‖h‖ := by rw [add_comm, mul_add]
-- 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
b_pos : ∀ (i : ℕ), 0 < b i
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖s n‖ ≤ (C + ε) * ‖h‖
have hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
Tactic: have hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖ := by
      have :=
        calc
          ‖v 0‖ ≤ ‖h‖ + ‖v 0 - h‖ := norm_le_insert' _ _
          _ ≤ ‖h‖ + b 0 := by rw [← norm_neg_add]; gcongr
      calc
        ‖u 0‖ ≤ C * ‖v 0‖ := hnorm_u 0
        _ ≤ C * (‖h‖ + b 0) := by gcongr
        _ = C * b 0 + C * ‖h‖ := by rw [add_comm, mul_add]
-- 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
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
u : (n : ℕ) → G
hu : ∀ (n : ℕ), (f : (a : G) → H) (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
⊢ (∑ k ∈ range (n + 1), (1 / 2) ^ k) * (ε * ‖h‖ / 2) ≤ 2 * (ε * ‖h‖ / 2)
have hbc : LE.le (α := ℝ) (∑ k ∈ range (n + 1), (1 / 2) ^ k) 2
Tactic: gcongr