awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
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
⊢ ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) (0 : H) ∧ ‖g‖ ≤ (C + ε) * norm.{u_2} (E := H) 0

Tactic:
use 0
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
⊢ 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:
simp
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
i : ℕ
⊢ 0 < b i

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
⊢ ∀ (i : ℕ), 0 < b i

Tactic:
have b_pos (i) : 0 < b i := by positivity
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
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‖
⊢ ∃ (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

Premises used: controlled_sum_of_mem_closure, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
⊢ ∀ (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)
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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‖
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‖
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
choose u hu hnorm_u using this
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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₁ : ℝ
apply₂ : ℕ
⊢ CauchySeq s

Tactic:
apply NormedAddCommGroup.cauchy_series_of_le_geometric'' (by simp) one_half_lt_one

Premises used: NormedAddCommGroup.cauchy_series_of_le_geometric'', one_half_lt_one
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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‖ ≤ C * ‖v n‖

Tactic:
hnorm_u n
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
hbc : ‖v n‖ ≤ b n
⊢ C * ‖v n‖ ≤ C * b n

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
⊢ ‖v n‖ ≤ b n

Tactic:
(hv _ <| Nat.succ_le_iff.mp hn).le

Premises used: LT.lt.le, Iff.mp, Nat.succ_le_iff
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
⊢ ‖v n‖ ≤ b n

Tactic:
exact (hv _ <| Nat.succ_le_iff.mp hn).le

Premises used: LT.lt.le, Iff.mp, Nat.succ_le_iff
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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 * b n = (1 / 2) ^ n * (ε * ‖h‖ / 2)

Tactic:
simp [b, mul_div_cancel₀ _ hC.ne.symm]

Premises used: Ne.symm, mul_div_cancel₀, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
⊢ (1 / 2) ^ n * (ε * ‖h‖ / 2) = ε * ‖h‖ / 2 * (1 / 2) ^ n

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
C₂ : C * b n = (1 / 2) ^ n * (ε * ‖h‖ / 2)
⊢ ‖u n‖ ≤ ε * ‖h‖ / 2 * (1 / 2) ^ 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 _ _

Premises used: Norm.norm, HMul.hMul, HDiv.hDiv, mul_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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

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 _ _
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
neg : ∀ (g : G) (hg : Tendsto s atTop (𝓝 g)), ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
obtain ⟨g : G, hg⟩ := cauchySeq_tendsto_of_complete this

Premises used: cauchySeq_tendsto_of_complete
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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‖

Tactic:
⟨g, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
neg₁ : ‖g‖ ≤ (C + ε) * ‖h‖
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
refine ⟨g, ?_, ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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)
h₁ : ∀ (n : ℕ), Eq.{u_2 + 1} (α := H) (((⇑f : (a : G) → H) ∘ s) n) (∑ k ∈ range (n + 1), v k)
⊢ Eq.{u_2 + 1} (α := ℕ → H) ((⇑f : (a : G) → H) ∘ s) fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), v k

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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 : ℕ
⊢ Eq.{u_2 + 1} (α := H) (((⇑f : (a : G) → H) ∘ s) n) (∑ k ∈ range (n + 1), v k)

Tactic:
simp [s, map_sum, hu]

Premises used: map_sum
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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

Tactic:
have : f ∘ s = fun n => ∑ k ∈ range (n + 1), v k := by
      ext n
      simp [s, map_sum, hu]
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
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
⊢ (f : (a : G) → H) g = h

Tactic:
rw [← this] at lim_v
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
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
lim_v : Tendsto ((⇑f : (a : G) → H) ∘ s) atTop (𝓝 h)
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

Tactic:
tendsto_nhds_unique ((f.continuous.tendsto g).comp hg) lim_v

Premises used: Continuous.tendsto, Filter.Tendsto.comp, tendsto_nhds_unique, NormedAddGroupHom.continuous
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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
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
lim_v : Tendsto ((⇑f : (a : G) → H) ∘ s) atTop (𝓝 h)
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

Tactic:
exact tendsto_nhds_unique ((f.continuous.tendsto g).comp hg) lim_v

Premises used: Continuous.tendsto, Filter.Tendsto.comp, tendsto_nhds_unique, NormedAddGroupHom.continuous
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
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 : ∀ (n : ℕ), ‖s n‖ ≤ (C + ε) * ‖h‖
⊢ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
suffices ∀ n, ‖s n‖ ≤ (C + ε) * ‖h‖ from
      le_of_tendsto' (continuous_norm.continuousAt.tendsto.comp hg) this