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
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 : ℕ
rw : ‖h‖ + ‖-v 0 + h‖ ≤ ‖h‖ + b 0
⊢ ‖h‖ + ‖v 0 - h‖ ≤ ‖h‖ + b 0

Tactic:
rw [← norm_neg_add]

Premises used: norm_neg_add
-- 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 : ℕ
⊢ ‖h‖ + ‖-v 0 + h‖ ≤ ‖h‖ + b 0

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
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖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
-- 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)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
⊢ ‖u 0‖ ≤ C * ‖v 0‖

Tactic:
hnorm_u 0

Premises used: 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
this_1 : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
ha : 0 ≤ C
⊢ C * ‖v 0‖ ≤ C * (‖h‖ + b 0)

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
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‖
rw₁ rw₂ : C * b 0 + C * ‖h‖ = C * b 0 + C * ‖h‖
⊢ C * (‖h‖ + b 0) = C * b 0 + C * ‖h‖

Tactic:
rw [add_comm, mul_add]

Premises used: add_comm, mul_add
-- 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)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
C₁ : C * ‖v 0‖ ≤ C * (‖h‖ + b 0)
C₂ : C * (‖h‖ + b 0) = C * b 0 + C * ‖h‖
⊢ ‖u 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]

Premises used: Norm.norm, HAdd.hAdd, 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
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖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]
-- 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 : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
⊢ ∑ k ∈ range (n + 1), C * b k = (∑ k ∈ range (n + 1), (1 / 2) ^ k) * (ε * ‖h‖ / 2)

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

Premises used: Ne.symm, mul_div_cancel₀, Finset.sum_mul, 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
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
hbc : LE.le (α := ℝ) (∑ k ∈ range (n + 1), (1 / 2) ^ k) 2
⊢ (∑ k ∈ range (n + 1), (1 / 2) ^ k) * (ε * ‖h‖ / 2) ≤ 2 * (ε * ‖h‖ / 2)

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
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
⊢ LE.le (α := ℝ) (∑ k ∈ range (n + 1), (1 / 2) ^ k) 2

Tactic:
apply sum_geometric_two_le

Premises used: sum_geometric_two_le
-- 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 : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
⊢ ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖

Tactic:
have : (∑ k ∈ range (n + 1), C * b k) ≤ ε * ‖h‖ :=
      calc (∑ k ∈ range (n + 1), C * b k)
        _ = (∑ k ∈ range (n + 1), (1 / 2 : ℝ) ^ k) * (ε * ‖h‖ / 2) := by
          simp only [b, mul_div_cancel₀ _ hC.ne.symm, ← sum_mul]
        _ ≤ 2 * (ε * ‖h‖ / 2) := by gcongr; apply sum_geometric_two_le
        _ = ε * ‖h‖ := mul_div_cancel₀ _ two_ne_zero
-- 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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ‖s n‖ ≤ ∑ k ∈ range (n + 1), ‖u k‖

Tactic:
norm_sum_le _ _

Premises used: norm_sum_le
-- 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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k ∈ range (n + 1), ‖u k‖ = ∑ k ∈ range n, ‖u (k + 1)‖ + ‖u 0‖

Tactic:
sum_range_succ' _ _

Premises used: Finset.sum_range_succ'
-- 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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
bc : ∀ i ∈ range n, ‖u (i + 1)‖ ≤ C * ‖v (i + 1)‖
⊢ ∑ k ∈ range n, ‖u (k + 1)‖ + ‖u 0‖ ≤ ∑ k ∈ range n, C * ‖v (k + 1)‖ + ‖u 0‖

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
this_1 : 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‖
i : ℕ
h_1 : i ∈ range n
⊢ ‖u (i + 1)‖ ≤ C * ‖v (i + 1)‖

Tactic:
apply hnorm_u
-- 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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
h₁ : ∀ k ∈ range n, ‖v (k + 1)‖ ≤ b (k + 1)
⊢ ∑ 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
-- 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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
k : ℕ
h_1 : k ∈ range n
⊢ ‖v (k + 1)‖ ≤ b (k + 1)

Tactic:
(hv _ k.succ_pos).le

Premises used: LT.lt.le, Nat.succ_pos
-- 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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
k : ℕ
h_1 : k ∈ range n
⊢ ‖v (k + 1)‖ ≤ b (k + 1)

Tactic:
exact (hv _ k.succ_pos).le

Premises used: LT.lt.le, Nat.succ_pos
-- 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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
rw : ∑ k ∈ range n, C * b (k + 1) + C * b 0 + C * ‖h‖ = ∑ k ∈ range (n + 1), C * b k + C * ‖h‖
rw₁ rw₂ : ∑ k ∈ range n, C * b (k + 1) + C * b 0 + C * ‖h‖ = ∑ k ∈ range n, C * b (k + 1) + C * b 0 + C * ‖h‖
⊢ ∑ k ∈ range n, C * b (k + 1) + (C * b 0 + C * ‖h‖) = ∑ k ∈ range (n + 1), C * b k + C * ‖h‖

Tactic:
rw [← add_assoc, sum_range_succ']

Premises used: add_assoc, Finset.sum_range_succ'
-- 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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
rw : C * ‖h‖ + ∑ k ∈ range (n + 1), C * b k ≤ C * ‖h‖ + ε * ‖h‖
⊢ ∑ k ∈ range (n + 1), C * b k + C * ‖h‖ ≤ (C + ε) * ‖h‖

Tactic:
rw [add_comm, add_mul]

Premises used: add_mul, add_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_1 : 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‖
⊢ C * ‖h‖ + ∑ k ∈ range (n + 1), C * b k ≤ C * ‖h‖ + ε * ‖h‖

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
this_1 : 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 : ∑ k ∈ range n, ‖u (k + 1)‖ + ‖u 0‖ ≤ ∑ k ∈ range n, C * ‖v (k + 1)‖ + ‖u 0‖
k₁ : ∑ k ∈ range n, C * ‖v (k + 1)‖ + ‖u 0‖ ≤ ∑ k ∈ range n, C * b (k + 1) + (C * b 0 + C * ‖h‖)
k₂ : ∑ k ∈ range n, C * b (k + 1) + (C * b 0 + C * ‖h‖) = ∑ k ∈ range (n + 1), C * b k + C * ‖h‖
k₃ : ∑ k ∈ range (n + 1), C * b k + C * ‖h‖ ≤ (C + ε) * ‖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]
        gcongr

Premises used: Norm.norm, HMul.hMul, Finset.range, HAdd.hAdd, OfNat.ofNat, Finset.sum_range_succ', norm_sum_le, Finset.sum