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
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‖
⊢ ‖s n‖ ≤ (C + ε) * ‖h‖
have this₁ : ∑ 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
-- 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 : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k ∈ range n, ‖u (k + 1)‖ + ‖u 0‖ ≤ ∑ k ∈ range n, C * ‖v (k + 1)‖ + ‖u 0‖
have bc : ∀ i ∈ range n, ‖u (i + 1)‖ ≤ C * ‖v (i + 1)‖
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 : ℕ
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‖)
have h₁ : ∀ k ∈ range n, ‖v (k + 1)‖ ≤ b (k + 1)
Tactic: gcongr with k
-- 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 : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k ∈ range n, C * b (k + 1) + (C * b 0 + C * ‖h‖) = ∑ k ∈ range (n + 1), C * b k + C * ‖h‖
have rw : ∑ 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']
-- 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 : ℕ
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‖
⊢ ∑ k ∈ range n, C * b (k + 1) + (C * b 0 + C * ‖h‖) = ∑ k ∈ range (n + 1), C * b k + C * ‖h‖
have 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‖
Tactic: rw [← add_assoc, sum_range_succ']
-- 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 : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k ∈ range (n + 1), C * b k + C * ‖h‖ ≤ (C + ε) * ‖h‖
have rw : C * ‖h‖ + ∑ k ∈ range (n + 1), C * b k ≤ C * ‖h‖ + ε * ‖h‖
Tactic: rw [add_comm, add_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
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‖ ≤ (C + ε) * ‖h‖
have k : ∑ k ∈ range n, ‖u (k + 1)‖ + ‖u 0‖ ≤ ∑ k ∈ range n, C * ‖v (k + 1)‖ + ‖u 0‖
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
-- 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 : ℕ
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‖
⊢ ‖s n‖ ≤ (C + ε) * ‖h‖
have k₁ : ∑ k ∈ range n, C * ‖v (k + 1)‖ + ‖u 0‖ ≤ ∑ k ∈ range n, C * b (k + 1) + (C * b 0 + 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
-- 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 : ℕ
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‖)
⊢ ‖s n‖ ≤ (C + ε) * ‖h‖
have k₂ : ∑ k ∈ range n, C * b (k + 1) + (C * b 0 + C * ‖h‖) = ∑ k ∈ range (n + 1), C * b k + 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
-- 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 : ℕ
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‖
⊢ ‖s n‖ ≤ (C + ε) * ‖h‖
have k₃ : ∑ k ∈ range (n + 1), C * b k + C * ‖h‖ ≤ (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
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
h : H
h_in : h ∈ j.range
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ C * ‖h‖
have rcases : ∀ (k : K) (h_in : Membership.mem (α := H) j.range ((j : (a : K) → H) k : H)),
  ∃ (g : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧
      ‖g‖ ≤ C * norm.{u_2} (E := H) ((j : (a : K) → H) k : H)
Tactic: rcases (j.mem_range _).mp h_in with ⟨k, rfl⟩
Cleared hypotheses: h, h_in
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : Membership.mem (α := H) j.range ((j : (a : K) → H) k : H)
⊢ ∃ (g : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧
      ‖g‖ ≤ C * norm.{u_2} (E := H) ((j : (a : K) → H) k : H)
have rw : ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
Tactic: rw [hj]
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
⊢ f.SurjectiveOnWith j.range.topologicalClosure (C + ε)
have hyp₁ : ∀ h ∈ j.range, ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ C * ‖h‖
Tactic: replace hyp : ∀ h ∈ j.range, ∃ g, f g = h ∧ ‖g‖ ≤ C * ‖h‖ := by
    intro h h_in
    rcases (j.mem_range _).mp h_in with ⟨k, rfl⟩
    rw [hj]
    exact hyp k
Cleared hypotheses: hyp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Defs (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist x y = ‖x⁻¹ * y‖
have rw : dist x y = dist 1 (x⁻¹ * y)
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Defs (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist x y = dist 1 (x⁻¹ * y)
have a : dist x y ≤ dist 1 (x⁻¹ * y)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Defs (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
a : dist x y ≤ dist 1 (x⁻¹ * y)
⊢ dist x y = dist 1 (x⁻¹ * y)
have a₁ : dist 1 (x⁻¹ * y) ≤ dist x y
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Defs (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
⊢ dist x y = ‖x⁻¹ * y‖
have rw : dist x y = dist 1 (x⁻¹ * y)
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Defs (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
⊢ dist x y = dist 1 (x⁻¹ * y)
have a : dist x y ≤ dist 1 (x⁻¹ * y)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Defs (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
a : dist x y ≤ dist 1 (x⁻¹ * y)
⊢ dist x y = dist 1 (x⁻¹ * y)
have a₁ : dist 1 (x⁻¹ * y) ≤ dist x y
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Defs (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Group E
f : GroupSeminorm E
x y : E
⊢ Eq (α := ℝ) ((f : (a : E) → ℝ) (x⁻¹ * y) : ℝ) ((f : (a : E) → ℝ) (y⁻¹ * x) : ℝ)
have h : x⁻¹ * y = (y⁻¹ * x)⁻¹
Tactic: convert! map_inv_eq_map f (y⁻¹ * x) using 2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Defs (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Group E
f : GroupSeminorm E
x y z : E
⊢ (f : (a : E) → ℝ) (x⁻¹ * z) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) (x⁻¹ * y) : ℝ) ((f : (a : E) → ℝ) (y⁻¹ * z) : ℝ)
have h : x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)
Tactic: convert! map_mul_le_add f (x⁻¹ * y) (y⁻¹ * z) using 2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (t : Finset α) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop s
have refine : ∀ (ε : ℝ) (εpos : ε > 0),
  ∀ᶠ (n : Finset α) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : α), f n x) (∑ n ∈ n, f n x) < ε
Tactic: refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : Finset α) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : α), f n x) (∑ n ∈ n, f n x) < ε
have h : ∀ (t : Finset α) (ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε) (x : β) (hx : x ∈ s),
  dist.{u_3} (α := F) (∑' (n : α), f n x) (∑ n ∈ t, f n x) < ε
Tactic: filter_upwards [(tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos] with t ht x hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (hypothesis)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
⊢ dist.{u_3} (α := F) (∑' (n : α), f n x) (∑ n ∈ t, f n x) < ε
have A : Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖
Tactic: have A : Summable fun n => ‖f n x‖ :=
    .of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n => hfu n x hx) hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
A : Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖
⊢ dist.{u_3} (α := F) (∑' (n : α), f n x) (∑ n ∈ t, f n x) < ε
have h : norm.{u_3} (E := F) (∑' (x_1 : { x : α // x ∉ t }), f (↑x_1 : α) x) < ε
Tactic: rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl t, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
A : Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖
⊢ norm.{u_3} (E := F) (∑' (x_1 : { x : α // x ∉ t }), f (↑x_1 : α) x) < ε
have apply : norm.{u_3} (E := F) (∑' (x_1 : { x : α // x ∉ t }), f (↑x_1 : α) x) ≤ ∑' (a : { x : α // x ∉ t }), u (↑a : α)
Tactic: apply lt_of_le_of_lt _ ht
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
A : Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖
⊢ norm.{u_3} (E := F) (∑' (x_1 : { x : α // x ∉ t }), f (↑x_1 : α) x) ≤ ∑' (a : { x : α // x ∉ t }), u (↑a : α)
have apply : LE.le (α := ℝ) (∑' (i : { x : α // x ∉ t }), ‖f (↑i : α) x‖) (∑' (a : { x : α // x ∉ t }), u (↑a : α))
Tactic: apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : ι), f n x) atTop s
have refine : ∀ (ε : ℝ) (εpos : ε > 0),
  ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
Tactic: refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (hypothesis)
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
have this : ∀ᶠ (b : Finset ι) in atTop, ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε
Tactic: have := (tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos