-- Mathlib/Analysis/Normed/Group/ControlledClosure.lean
theorem controlled_closure_of_complete {f : NormedAddGroupHom G H} {K : AddSubgroup H} {C ε : ℝ}
    (hC : 0 < C) (hε : 0 < ε) (hyp : f.SurjectiveOnWith K C) :
    f.SurjectiveOnWith K.topologicalClosure (C + ε)

Proof state:
case neg.intro.intro.intro.intro
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : 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 : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
set s : ℕ → G := fun n => ∑ k ∈ range (n + 1), u k

Result:
case neg.intro.intro.intro.intro
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : 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 : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n => ∑ k ∈ range (n + 1), u k
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Proof state:
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : 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 : ℕ → G
hu : ∀ (n : ℕ), f (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‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k ∈ range n, C * ‖v (k + 1)‖ + ‖u 0‖ ≤ ∑ k ∈ range n, C * b (k + 1) + (C * b 0 + C * ‖h‖)

Tactic:
gcongr with k

Result:
case h₁.h.h
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : 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 : ℕ → G
hu : ∀ (n : ℕ), f (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‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
k : ℕ
a✝ : k ∈ range n
⊢ ‖v (k + 1)‖ ≤ b (k + 1)

Proof state:
case neg.intro.intro.intro.intro.intro.refine_2
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : 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 : ℕ → G
hu : ∀ (n : ℕ), f (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‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ‖s n‖ ≤ (C + ε) * ‖h‖

Tactic:
calc
  ‖s n‖ ≤ ∑ k ∈ range (n + 1), ‖u k‖ := norm_sum_le _ _
  _ = (∑ k ∈ range n, ‖u (k + 1)‖) + ‖u 0‖ := sum_range_succ' _ _
  _ ≤ (∑ k ∈ range n, C * ‖v (k + 1)‖) + ‖u 0‖ := by gcongr; apply hnorm_u
  _ ≤ (∑ k ∈ range n, C * b (k + 1)) + (C * b 0 + C * ‖h‖) := by
    gcongr with k; exact (hv _ k.succ_pos).le
  _ = (∑ k ∈ range (n + 1), C * b k) + C * ‖h‖ := by rw [← add_assoc, sum_range_succ']
  _ ≤ (C + ε) * ‖h‖ := by
    rw [add_comm, add_mul]
    apply add_le_add_left this

Result:
no goals

Proof state:
case neg.intro.intro.intro.intro
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : 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 : ℕ → G
hu : ∀ (n : ℕ), f (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, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

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

Result:
case neg.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : 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 : ℕ → G
hu : ∀ (n : ℕ), f (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, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖