[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
⊢ NormedAddGroupHom.SurjectiveOnWith f (AddSubgroup.topologicalClosure K) (C + ε)
[PROOFSTEP]
rintro (h : H)
  (h_in : h ∈ K.topologicalClosure)
    -- We first get rid of the easy case where `h = 0`.
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
by_cases hyp_h : h = 0
[GOAL]
case pos
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : h = 0
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
rw [hyp_h]
[GOAL]
case pos
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : h = 0
⊢ ∃ g, ↑f g = 0 ∧ ‖g‖ ≤ (C + ε) * ‖0‖
[PROOFSTEP]
use 0
[GOAL]
case 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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : h = 0
⊢ ↑f 0 = 0 ∧ ‖0‖ ≤ (C + ε) * ‖0‖
[PROOFSTEP]
simp
  /- The desired preimage will be constructed as the sum of a series. Convergence of
      the series will be guaranteed by completeness of `G`. We first write `h` as the sum
      of a sequence `v` of elements of `K` which starts close to `h` and then quickly goes to zero.
      The sequence `b` below quantifies this. -/
[GOAL]
case neg
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : ¬h = 0
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
set b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
[GOAL]
case neg
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
have b_pos : ∀ i, 0 < b i := by
  intro i
  field_simp [hC]
  exact div_pos (mul_pos hε (norm_pos_iff.mpr hyp_h)) (mul_pos (by norm_num : (0 : ℝ) < 2 ^ i * 2) hC)
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
⊢ ∀ (i : ℕ), 0 < b i
[PROOFSTEP]
intro i
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
i : ℕ
⊢ 0 < b i
[PROOFSTEP]
field_simp [hC]
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
i : ℕ
⊢ 0 < ε * ‖h‖ / (2 ^ i * 2 * C)
[PROOFSTEP]
exact div_pos (mul_pos hε (norm_pos_iff.mpr hyp_h)) (mul_pos (by norm_num : (0 : ℝ) < 2 ^ i * 2) hC)
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
i : ℕ
⊢ 0 < 2 ^ i * 2
[PROOFSTEP]
norm_num
[GOAL]
case neg
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
obtain
  ⟨v : ℕ → H, lim_v : Tendsto (fun n : ℕ => ∑ k in 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
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), n > 0 → ‖v n‖ < b n
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
have : ∀ n, ∃ m' : G, f m' = v n ∧ ‖m'‖ ≤ C * ‖v n‖ := fun n : ℕ => hyp (v n) (v_in n)
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), n > 0 → ‖v n‖ < b n
this : ∀ (n : ℕ), ∃ m', ↑f m' = v n ∧ ‖m'‖ ≤ C * ‖v n‖
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
choose u hu hnorm_u using this
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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‖
[PROOFSTEP]
set s : ℕ → G := fun n => ∑ k in range (n + 1), u k
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
have : CauchySeq s :=
  by
  apply NormedAddCommGroup.cauchy_series_of_le_geometric'' (by norm_num) 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 [mul_div_cancel' _ hC.ne.symm]
    _ = ε * ‖h‖ / 2 * (1 / 2) ^ n :=
      mul_comm _
        _
          -- We now show that the limit `g` of `s` is the desired preimage.
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
⊢ CauchySeq s
[PROOFSTEP]
apply NormedAddCommGroup.cauchy_series_of_le_geometric'' (by norm_num) one_half_lt_one
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
⊢ 0 < 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
⊢ ∀ (n : ℕ), n ≥ ?m.14929 → ‖u n‖ ≤ ?m.14927 * (1 / 2) ^ n
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
⊢ ℝ
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
⊢ ℕ
[PROOFSTEP]
rintro n (hn : n ≥ 1)
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
n : ℕ
hn : n ≥ 1
⊢ ‖u n‖ ≤ ?m.14927 * (1 / 2) ^ n
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
⊢ ℝ
[PROOFSTEP]
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 [mul_div_cancel' _ hC.ne.symm]
  _ = ε * ‖h‖ / 2 * (1 / 2) ^ n :=
    mul_comm _
      _
        -- We now show that the limit `g` of `s` is the desired preimage.
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
n : ℕ
hn : n ≥ 1
⊢ C * ‖v n‖ ≤ C * b n
[PROOFSTEP]
gcongr
[GOAL]
case 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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
n : ℕ
hn : n ≥ 1
⊢ ‖v n‖ ≤ b n
[PROOFSTEP]
exact (hv _ <| Nat.succ_le_iff.mp hn).le
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
n : ℕ
hn : n ≥ 1
⊢ C * b n = (1 / 2) ^ n * (ε * ‖h‖ / 2)
[PROOFSTEP]
simp [mul_div_cancel' _ hC.ne.symm]
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
obtain ⟨g : G, hg⟩ := cauchySeq_tendsto_of_complete this
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
refine' ⟨g, _, _⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.refine'_1
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ↑f g = h
[PROOFSTEP]
have : f ∘ s = fun n => ∑ k in range (n + 1), v k := by
  ext n
  simp [map_sum, hu]
    /- In the above equality, the left-hand-side converges to `f g` by continuity of `f` and
          definition of `g` while the right-hand-side converges to `h` by construction of `v` so
          `g` is indeed a preimage of `h`. -/
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ↑f ∘ s = fun n => ∑ k in range (n + 1), v k
[PROOFSTEP]
ext n
[GOAL]
case 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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ (↑f ∘ s) n = ∑ k in range (n + 1), v k
[PROOFSTEP]
simp [map_sum, hu]
  /- In the above equality, the left-hand-side converges to `f g` by continuity of `f` and
        definition of `g` while the right-hand-side converges to `h` by construction of `v` so
        `g` is indeed a preimage of `h`. -/
[GOAL]
case neg.intro.intro.intro.intro.intro.refine'_1
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
this : ↑f ∘ s = fun n => ∑ k in range (n + 1), v k
⊢ ↑f g = h
[PROOFSTEP]
rw [← this] at lim_v
[GOAL]
case neg.intro.intro.intro.intro.intro.refine'_1
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 : ℕ), 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 in range (n + 1), u k
lim_v : Tendsto (↑f ∘ s) atTop (𝓝 h)
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
this : ↑f ∘ s = fun n => ∑ k in range (n + 1), v k
⊢ ↑f g = h
[PROOFSTEP]
exact tendsto_nhds_unique ((f.continuous.tendsto g).comp hg) lim_v
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ‖g‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
suffices : ∀ n, ‖s n‖ ≤ (C + ε) * ‖h‖
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
this : ∀ (n : ℕ), ‖s n‖ ≤ (C + ε) * ‖h‖
⊢ ‖g‖ ≤ (C + ε) * ‖h‖
case this
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ∀ (n : ℕ), ‖s n‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
exact le_of_tendsto' (continuous_norm.continuousAt.tendsto.comp hg) this
[GOAL]
case this
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ∀ (n : ℕ), ‖s n‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
intro n
[GOAL]
case this
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖s n‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
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 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]
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖u 0‖ ≤ C * b 0 + C * ‖h‖
[PROOFSTEP]
have :=
  calc
    ‖v 0‖ ≤ ‖h‖ + ‖v 0 - h‖ := norm_le_insert' _ _
    _ ≤ ‖h‖ + b 0 := by gcongr
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖h‖ + ‖v 0 - h‖ ≤ ‖h‖ + b 0
[PROOFSTEP]
gcongr
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
⊢ ‖u 0‖ ≤ C * b 0 + C * ‖h‖
[PROOFSTEP]
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]
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
⊢ C * ‖v 0‖ ≤ C * (‖h‖ + b 0)
[PROOFSTEP]
gcongr
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in range (n + 1), u k
this✝ : 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‖
[PROOFSTEP]
rw [add_comm, mul_add]
[GOAL]
case this
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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‖
[PROOFSTEP]
have : (∑ k in range (n + 1), C * b k) ≤ ε * ‖h‖ :=
  calc
    (∑ k in range (n + 1), C * b k) = (∑ k in range (n + 1), (1 / 2 : ℝ) ^ k) * (ε * ‖h‖ / 2) := by
      simp only [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
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), C * b k = (∑ k in range (n + 1), (1 / 2) ^ k) * (ε * ‖h‖ / 2)
[PROOFSTEP]
simp only [mul_div_cancel' _ hC.ne.symm, ← sum_mul]
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), (1 / 2) ^ k) * (ε * ‖h‖ / 2) ≤ 2 * (ε * ‖h‖ / 2)
[PROOFSTEP]
gcongr
[GOAL]
case 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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), (1 / 2) ^ k ≤ 2
[PROOFSTEP]
apply sum_geometric_two_le
[GOAL]
case this
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ‖s n‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
calc
  ‖s n‖ ≤ ∑ k in range (n + 1), ‖u k‖ := norm_sum_le _ _
  _ = (∑ k in range n, ‖u (k + 1)‖) + ‖u 0‖ := (sum_range_succ' _ _)
  _ ≤ (∑ k in range n, C * ‖v (k + 1)‖) + ‖u 0‖ := by gcongr; apply hnorm_u
  _ ≤ (∑ k in range n, C * b (k + 1)) + (C * b 0 + C * ‖h‖) := by gcongr with k; exact (hv _ k.succ_pos).le
  _ = (∑ k in 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
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k in range n, ‖u (k + 1)‖ + ‖u 0‖ ≤ ∑ k in range n, C * ‖v (k + 1)‖ + ‖u 0‖
[PROOFSTEP]
gcongr
[GOAL]
case bc.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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), C * b k ≤ ε * ‖h‖
i✝ : ℕ
a✝ : i✝ ∈ range n
⊢ ‖u (i✝ + 1)‖ ≤ C * ‖v (i✝ + 1)‖
[PROOFSTEP]
apply hnorm_u
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k in range n, C * ‖v (k + 1)‖ + ‖u 0‖ ≤ ∑ k in range n, C * b (k + 1) + (C * b 0 + C * ‖h‖)
[PROOFSTEP]
gcongr with k
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), C * b k ≤ ε * ‖h‖
k : ℕ
a✝ : k ∈ range n
⊢ ‖v (k + 1)‖ ≤ b (k + 1)
[PROOFSTEP]
exact (hv _ k.succ_pos).le
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k in range n, C * b (k + 1) + (C * b 0 + C * ‖h‖) = ∑ k in range (n + 1), C * b k + C * ‖h‖
[PROOFSTEP]
rw [← add_assoc, sum_range_succ']
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k in range (n + 1), C * b k + C * ‖h‖ ≤ (C + ε) * ‖h‖
[PROOFSTEP]
rw [add_comm, add_mul]
[GOAL]
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 : NormedAddGroupHom.SurjectiveOnWith f K C
h : H
h_in : h ∈ AddSubgroup.topologicalClosure K
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 in range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖v 0 - h‖ < b 0
hv : ∀ (n : ℕ), 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 in 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 in range (n + 1), C * b k ≤ ε * ‖h‖
⊢ C * ‖h‖ + ∑ k in range (n + 1), C * b k ≤ C * ‖h‖ + ε * ‖h‖
[PROOFSTEP]
apply add_le_add_left this
[GOAL]
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
⊢ NormedAddGroupHom.SurjectiveOnWith f (AddSubgroup.topologicalClosure (NormedAddGroupHom.range j)) (C + ε)
[PROOFSTEP]
replace hyp : ∀ h ∈ j.range, ∃ g, f g = h ∧ ‖g‖ ≤ C * ‖h‖
[GOAL]
case hyp
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
⊢ ∀ (h : H), h ∈ NormedAddGroupHom.range j → ∃ g, ↑f g = h ∧ ‖g‖ ≤ C * ‖h‖
[PROOFSTEP]
intro h h_in
[GOAL]
case hyp
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
h : H
h_in : h ∈ NormedAddGroupHom.range j
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ C * ‖h‖
[PROOFSTEP]
rcases(j.mem_range _).mp h_in with ⟨k, rfl⟩
[GOAL]
case hyp.intro
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : ↑j k ∈ NormedAddGroupHom.range j
⊢ ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖↑j k‖
[PROOFSTEP]
rw [hj]
[GOAL]
case hyp.intro
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : ↑j k ∈ NormedAddGroupHom.range j
⊢ ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
[PROOFSTEP]
exact hyp k
[GOAL]
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (h : H), h ∈ NormedAddGroupHom.range j → ∃ g, ↑f g = h ∧ ‖g‖ ≤ C * ‖h‖
⊢ NormedAddGroupHom.SurjectiveOnWith f (AddSubgroup.topologicalClosure (NormedAddGroupHom.range j)) (C + ε)
[PROOFSTEP]
exact controlled_closure_of_complete hC hε hyp


[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ ↑f (x - y) ≤ max (↑f x) (↑f y)
[PROOFSTEP]
rw [sub_eq_add_neg, ← NonarchAddGroupSeminormClass.map_neg_eq_map' f y]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ ↑f (x + -y) ≤ max (↑f x) (↑f (-y))
[PROOFSTEP]
exact map_add_le_max _ _ _
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
src✝ : NonarchAddGroupSeminormClass F E := inst✝
f : F
x y : E
⊢ ∀ (a : E), 0 ≤ ↑f a
[PROOFSTEP]
intro a
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
src✝ : NonarchAddGroupSeminormClass F E := inst✝
f : F
x y a : E
⊢ 0 ≤ ↑f a
[PROOFSTEP]
rw [← NonarchAddGroupSeminormClass.map_zero f, ← sub_self a]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
src✝ : NonarchAddGroupSeminormClass F E := inst✝
f : F
x y a : E
⊢ ↑f (a - a) ≤ ↑f a
[PROOFSTEP]
exact le_trans (map_sub_le_max _ _ _) (by rw [max_self (f a)])
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
src✝ : NonarchAddGroupSeminormClass F E := inst✝
f : F
x y a : E
⊢ max (↑f a) (↑f a) ≤ ↑f a
[PROOFSTEP]
rw [max_self (f a)]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q f g : GroupSeminorm E
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q g : GroupSeminorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
h :
  (fun f => f.toFun) { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } =
    (fun f => f.toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
toFun✝¹ : E → ℝ
map_one'✝¹ : toFun✝¹ 1 = 0
mul_le'✝¹ : ∀ (x y : E), toFun✝¹ (x * y) ≤ toFun✝¹ x + toFun✝¹ y
inv'✝¹ : ∀ (x : E), toFun✝¹ x⁻¹ = toFun✝¹ x
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
h :
  (fun f => f.toFun) { toFun := toFun✝¹, map_one' := map_one'✝¹, mul_le' := mul_le'✝¹, inv' := inv'✝¹ } =
    (fun f => f.toFun) { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹, mul_le' := mul_le'✝¹, inv' := inv'✝¹ } =
    { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ (fun x => ↑p x + ↑q x) 1 = 0
[PROOFSTEP]
simp_rw [map_one_eq_zero p, map_one_eq_zero q, zero_add]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
x : E
⊢ (fun x => ↑p x + ↑q x) x⁻¹ = (fun x => ↑p x + ↑q x) x
[PROOFSTEP]
simp_rw [map_inv_eq_map p, map_inv_eq_map q]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ (↑p ⊔ ↑q) 1 = 0
[PROOFSTEP]
rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_zero q]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
x : E
⊢ (↑p ⊔ ↑q) x⁻¹ = (↑p ⊔ ↑q) x
[PROOFSTEP]
rw [Pi.sup_apply, Pi.sup_apply, map_inv_eq_map p, map_inv_eq_map q]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q : GroupSeminorm E
f✝ : F →* E
p : GroupSeminorm E
f : F →* E
⊢ (fun x => ↑p (↑f x)) 1 = 0
[PROOFSTEP]
simp_rw [f.map_one, map_one_eq_zero p]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q : GroupSeminorm E
f✝ : F →* E
p : GroupSeminorm E
f : F →* E
x : F
⊢ (fun x => ↑p (↑f x)) x⁻¹ = (fun x => ↑p (↑f x)) x
[PROOFSTEP]
simp_rw [map_inv, map_inv_eq_map p]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ y : E
p q : GroupSeminorm E
x : E
⊢ 0 ∈ lowerBounds (range fun y => ↑p y + ↑q (x / y))
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝¹ y : E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => ↑p y + ↑q (x✝ / y)) x
[PROOFSTEP]
dsimp
[GOAL]
case intro
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝¹ y : E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ ↑p x + ↑q (x✝ / x)
[PROOFSTEP]
positivity
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x y : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
⊢ ↑p 1 + ↑q (1 / 1) < r
[PROOFSTEP]
rwa [div_one, map_one_eq_zero p, map_one_eq_zero q, add_zero]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ y✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ (fun x => ⨅ (y : E), ↑p y + ↑q (x / y)) (x * y) ≤ ↑p u + ↑q (x / u) + (↑p v + ↑q (y / v))
[PROOFSTEP]
refine' ciInf_le_of_le mul_bddBelow_range_add (u * v) _
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ y✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ ↑p (u * v) + ↑q (x * y / (u * v)) ≤ ↑p u + ↑q (x / u) + (↑p v + ↑q (y / v))
[PROOFSTEP]
rw [mul_div_mul_comm, add_add_add_comm]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ y✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ ↑p (u * v) + ↑q (x / u * (y / v)) ≤ ↑p u + ↑p v + (↑q (x / u) + ↑q (y / v))
[PROOFSTEP]
exact add_le_add (map_mul_le_add p _ _) (map_mul_le_add q _ _)
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ y : E
p q : GroupSeminorm E
x : E
⊢ ⨅ (x_1 : E), ↑p x_1⁻¹ + ↑q (x⁻¹ / x_1⁻¹) = (fun x => ⨅ (y : E), ↑p y + ↑q (x / y)) x
[PROOFSTEP]
simp_rw [map_inv_eq_map p, ← inv_div', map_inv_eq_map q]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ y : E
src✝ : SemilatticeSup (GroupSeminorm E) := semilatticeSup
p q : GroupSeminorm E
x : E
⊢ ↑p x + ↑q (x / x) ≤ (fun f => ↑f) p x
[PROOFSTEP]
rw [div_self', map_one_eq_zero q, add_zero]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ y : E
src✝ : SemilatticeSup (GroupSeminorm E) := semilatticeSup
p q : GroupSeminorm E
x : E
⊢ ↑p 1 + ↑q (x / 1) ≤ (fun f => ↑f) q x
[PROOFSTEP]
simpa only [div_one x, map_one_eq_zero p, zero_add (q x)] using le_rfl
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
⊢ (fun x => if x = 0 then 0 else 1) (x + y) ≤ (fun x => if x = 0 then 0 else 1) x + (fun x => if x = 0 then 0 else 1) y
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (fun x => if x = 0 then 0 else 1) (x + y) ≤ (fun x => if x = 0 then 0 else 1) x + (fun x => if x = 0 then 0 else 1) y
[PROOFSTEP]
simp only
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1
[PROOFSTEP]
rw [if_pos hx, hx, zero_add, zero_add]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (fun x => if x = 0 then 0 else 1) (x + y) ≤ (fun x => if x = 0 then 0 else 1) x + (fun x => if x = 0 then 0 else 1) y
[PROOFSTEP]
simp only
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1
[PROOFSTEP]
rw [if_neg hx]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1 + if y = 0 then 0 else 1
[PROOFSTEP]
refine' le_add_of_le_of_nonneg _ _
[GOAL]
case neg.refine'_1
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1
[PROOFSTEP]
split_ifs
[GOAL]
case neg.refine'_2
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ 0 ≤ if y = 0 then 0 else 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : x + y = 0
⊢ 0 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬x + y = 0
⊢ 1 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : y = 0
⊢ 0 ≤ 0
[PROOFSTEP]
norm_num
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
p : AddGroupSeminorm E
inst✝ : DecidableEq E
x : E
⊢ (fun x => if x = 0 then 0 else 1) (-x) = (fun x => if x = 0 then 0 else 1) x
[PROOFSTEP]
simp_rw [neg_eq_zero]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p✝ : AddGroupSeminorm E
r : R
p : AddGroupSeminorm E
⊢ (fun x => r • ↑p x) 0 = 0
[PROOFSTEP]
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_zero, mul_zero]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p✝ : AddGroupSeminorm E
r : R
p : AddGroupSeminorm E
x✝¹ x✝ : E
⊢ (fun x => r • ↑p x) (x✝¹ + x✝) ≤ (fun x => r • ↑p x) x✝¹ + (fun x => r • ↑p x) x✝
[PROOFSTEP]
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p✝ : AddGroupSeminorm E
r : R
p : AddGroupSeminorm E
x✝¹ x✝ : E
⊢ ↑(r • 1) * ↑p (x✝¹ + x✝) ≤ ↑(r • 1) * (↑p x✝¹ + ↑p x✝)
[PROOFSTEP]
gcongr
[GOAL]
case h
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p✝ : AddGroupSeminorm E
r : R
p : AddGroupSeminorm E
x✝¹ x✝ : E
⊢ ↑p (x✝¹ + x✝) ≤ ↑p x✝¹ + ↑p x✝
[PROOFSTEP]
apply map_add_le_add
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p✝ : AddGroupSeminorm E
r : R
p : AddGroupSeminorm E
x : E
⊢ (fun x => r • ↑p x) (-x) = (fun x => r • ↑p x) x
[PROOFSTEP]
simp_rw [map_neg_eq_map]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p✝ : AddGroupSeminorm E
r : R
p q : AddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)
[PROOFSTEP]
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
  mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p q f g : NonarchAddGroupSeminorm E
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _, _⟩ := f
[GOAL]
case mk.mk
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p q g : NonarchAddGroupSeminorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝ :
  ∀ (r s : E),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (r + s) ≤
      max (ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } r)
        (ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } s)
neg'✝ :
  ∀ (r : E),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (-r) =
      ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } r
h :
  (fun f => f.toFun)
      { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝, neg' := neg'✝ } =
    (fun f => f.toFun) g
⊢ { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝, neg' := neg'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk.mk
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p q : NonarchAddGroupSeminorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝¹ :
  ∀ (r s : E),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (r + s) ≤
      max (ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } r)
        (ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } s)
neg'✝¹ :
  ∀ (r : E),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (-r) =
      ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } r
toZeroHom✝ : ZeroHom E ℝ
add_le_max'✝ :
  ∀ (r s : E), ZeroHom.toFun toZeroHom✝ (r + s) ≤ max (ZeroHom.toFun toZeroHom✝ r) (ZeroHom.toFun toZeroHom✝ s)
neg'✝ : ∀ (r : E), ZeroHom.toFun toZeroHom✝ (-r) = ZeroHom.toFun toZeroHom✝ r
h :
  (fun f => f.toFun)
      { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝¹, neg' := neg'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }
⊢ { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝¹, neg' := neg'✝¹ } =
    { toZeroHom := toZeroHom✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p q : NonarchAddGroupSeminorm E
⊢ ↑p.toZeroHom = ↑p
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p q : NonarchAddGroupSeminorm E
f : F →+ E
r s : E
⊢ ZeroHom.toFun { toFun := 0, map_zero' := (_ : OfNat.ofNat 0 0 = 0) } (r + s) ≤
    max (ZeroHom.toFun { toFun := 0, map_zero' := (_ : OfNat.ofNat 0 0 = 0) } r)
      (ZeroHom.toFun { toFun := 0, map_zero' := (_ : OfNat.ofNat 0 0 = 0) } s)
[PROOFSTEP]
simp only [Pi.zero_apply]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p q : NonarchAddGroupSeminorm E
f : F →+ E
r s : E
⊢ 0 ≤ max 0 0
[PROOFSTEP]
rw [max_eq_right]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p q : NonarchAddGroupSeminorm E
f : F →+ E
r s : E
⊢ 0 ≤ 0
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p✝ q✝ : NonarchAddGroupSeminorm E
f : F →+ E
p q : NonarchAddGroupSeminorm E
⊢ (↑p ⊔ ↑q) 0 = 0
[PROOFSTEP]
rw [Pi.sup_apply, ← map_zero p, sup_eq_left, map_zero p, map_zero q]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p✝ q✝ : NonarchAddGroupSeminorm E
f : F →+ E
p q : NonarchAddGroupSeminorm E
x : E
⊢ ZeroHom.toFun { toFun := ↑p ⊔ ↑q, map_zero' := (_ : (↑p ⊔ ↑q) 0 = 0) } (-x) =
    ZeroHom.toFun { toFun := ↑p ⊔ ↑q, map_zero' := (_ : (↑p ⊔ ↑q) 0 = 0) } x
[PROOFSTEP]
simp_rw [Pi.sup_apply, map_neg_eq_map p, map_neg_eq_map q]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddCommGroup E
inst✝ : AddCommGroup F
p✝ q✝ : NonarchAddGroupSeminorm E
x✝ y : E
p q : NonarchAddGroupSeminorm E
x : E
⊢ 0 ∈ lowerBounds (range fun y => ↑p y + ↑q (x - y))
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddCommGroup E
inst✝ : AddCommGroup F
p✝ q✝ : NonarchAddGroupSeminorm E
x✝¹ y : E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => ↑p y + ↑q (x✝ - y)) x
[PROOFSTEP]
dsimp
[GOAL]
case intro
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddCommGroup E
inst✝ : AddCommGroup F
p✝ q✝ : NonarchAddGroupSeminorm E
x✝¹ y : E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ ↑p x + ↑q (x✝ - x)
[PROOFSTEP]
positivity
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
⊢ (fun x => if x = 1 then 0 else 1) (x * y) ≤ (fun x => if x = 1 then 0 else 1) x + (fun x => if x = 1 then 0 else 1) y
[PROOFSTEP]
by_cases hx : x = 1
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 1
⊢ (fun x => if x = 1 then 0 else 1) (x * y) ≤ (fun x => if x = 1 then 0 else 1) x + (fun x => if x = 1 then 0 else 1) y
[PROOFSTEP]
simp only
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1
[PROOFSTEP]
rw [if_pos hx, hx, one_mul, zero_add]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (fun x => if x = 1 then 0 else 1) (x * y) ≤ (fun x => if x = 1 then 0 else 1) x + (fun x => if x = 1 then 0 else 1) y
[PROOFSTEP]
simp only
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1
[PROOFSTEP]
rw [if_neg hx]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ 1 + if y = 1 then 0 else 1
[PROOFSTEP]
refine' le_add_of_le_of_nonneg _ _
[GOAL]
case neg.refine'_1
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ 1
[PROOFSTEP]
split_ifs
[GOAL]
case neg.refine'_2
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ 0 ≤ if y = 1 then 0 else 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : x * y = 1
⊢ 0 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬x * y = 1
⊢ 1 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : y = 1
⊢ 0 ≤ 0
[PROOFSTEP]
norm_num
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬y = 1
⊢ 0 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x : E
⊢ (fun x => if x = 1 then 0 else 1) x⁻¹ = (fun x => if x = 1 then 0 else 1) x
[PROOFSTEP]
simp_rw [inv_eq_one]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
⊢ (fun x => r • ↑p x) 1 = 0
[PROOFSTEP]
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_one_eq_zero p, mul_zero]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x✝¹ x✝ : E
⊢ (fun x => r • ↑p x) (x✝¹ * x✝) ≤ (fun x => r • ↑p x) x✝¹ + (fun x => r • ↑p x) x✝
[PROOFSTEP]
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x✝¹ x✝ : E
⊢ ↑(r • 1) * ↑p (x✝¹ * x✝) ≤ ↑(r • 1) * (↑p x✝¹ + ↑p x✝)
[PROOFSTEP]
gcongr
[GOAL]
case h
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x✝¹ x✝ : E
⊢ ↑p (x✝¹ * x✝) ≤ ↑p x✝¹ + ↑p x✝
[PROOFSTEP]
apply map_mul_le_add
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x : E
⊢ (fun x => r • ↑p x) x⁻¹ = (fun x => r • ↑p x) x
[PROOFSTEP]
simp_rw [map_inv_eq_map p]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : GroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)
[PROOFSTEP]
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
  mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
⊢ ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } (x + y) ≤
    max (ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } x)
      (ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } (x + y) ≤
    max (ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } x)
      (ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } y)
[PROOFSTEP]
simp_rw [if_pos hx, hx, zero_add]
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if y = 0 then 0 else 1) ≤ max 0 (if y = 0 then 0 else 1)
[PROOFSTEP]
exact le_max_of_le_right (le_refl _)
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } (x + y) ≤
    max (ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } x)
      (ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } y)
[PROOFSTEP]
simp_rw [if_neg hx]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max 1 (if y = 0 then 0 else 1)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : x + y = 0
h✝ : y = 0
⊢ 0 ≤ max 1 0
[PROOFSTEP]
norm_num
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : x + y = 0
h✝ : ¬y = 0
⊢ 0 ≤ max 1 1
[PROOFSTEP]
norm_num
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : ¬x + y = 0
h✝ : y = 0
⊢ 1 ≤ max 1 0
[PROOFSTEP]
norm_num
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : ¬x + y = 0
h✝ : ¬y = 0
⊢ 1 ≤ max 1 1
[PROOFSTEP]
norm_num
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x : E
⊢ ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } (-x) =
    ZeroHom.toFun { toFun := fun x => if x = 0 then 0 else 1, map_zero' := (_ : (if 0 = 0 then 0 else 1) = 0) } x
[PROOFSTEP]
simp_rw [neg_eq_zero]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
⊢ (fun x => r • ↑p x) 0 = 0
[PROOFSTEP]
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_zero p, mul_zero]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x y : E
⊢ ZeroHom.toFun { toFun := fun x => r • ↑p x, map_zero' := (_ : r • ↑p 0 = 0) } (x + y) ≤
    max (ZeroHom.toFun { toFun := fun x => r • ↑p x, map_zero' := (_ : r • ↑p 0 = 0) } x)
      (ZeroHom.toFun { toFun := fun x => r • ↑p x, map_zero' := (_ : r • ↑p 0 = 0) } y)
[PROOFSTEP]
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_max_of_nonneg _ _ NNReal.zero_le_coe]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x y : E
⊢ ↑(r • 1) * ↑p (x + y) ≤ ↑(r • 1) * max (↑p x) (↑p y)
[PROOFSTEP]
gcongr
[GOAL]
case h
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x y : E
⊢ ↑p (x + y) ≤ max (↑p x) (↑p y)
[PROOFSTEP]
apply map_add_le_max
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x : E
⊢ ZeroHom.toFun { toFun := fun x => r • ↑p x, map_zero' := (_ : r • ↑p 0 = 0) } (-x) =
    ZeroHom.toFun { toFun := fun x => r • ↑p x, map_zero' := (_ : r • ↑p 0 = 0) } x
[PROOFSTEP]
simp_rw [map_neg_eq_map p]
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : NonarchAddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)
[PROOFSTEP]
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
  mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q f g : GroupNorm E
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _, _, _⟩, _⟩ := f
[GOAL]
case mk.mk
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q g : GroupNorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
eq_one_of_map_eq_zero'✝ :
  ∀ (x : E),
    GroupSeminorm.toFun { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } x = 0 → x = 1
h :
  (fun f => f.toFun)
      { toGroupSeminorm := { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ },
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ } =
    (fun f => f.toFun) g
⊢ { toGroupSeminorm := { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ },
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ } =
    g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk.mk
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupNorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
eq_one_of_map_eq_zero'✝¹ :
  ∀ (x : E),
    GroupSeminorm.toFun { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } x = 0 → x = 1
toGroupSeminorm✝ : GroupSeminorm E
eq_one_of_map_eq_zero'✝ : ∀ (x : E), GroupSeminorm.toFun toGroupSeminorm✝ x = 0 → x = 1
h :
  (fun f => f.toFun)
      { toGroupSeminorm := { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ },
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝¹ } =
    (fun f => f.toFun) { toGroupSeminorm := toGroupSeminorm✝, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ }
⊢ { toGroupSeminorm := { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ },
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝¹ } =
    { toGroupSeminorm := toGroupSeminorm✝, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ }
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddGroup E
inst✝ : AddGroup F
p q f g : NonarchAddGroupNorm E
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _, _⟩, _⟩ := f
[GOAL]
case mk.mk.mk
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddGroup E
inst✝ : AddGroup F
p q g : NonarchAddGroupNorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝ :
  ∀ (r s : E),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (r + s) ≤
      max (ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } r)
        (ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } s)
neg'✝ :
  ∀ (r : E),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (-r) =
      ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } r
eq_zero_of_map_eq_zero'✝ :
  ∀ (x : E),
    ZeroHom.toFun
          { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝,
              neg' := neg'✝ }.toZeroHom
          x =
        0 →
      x = 0
h :
  (fun f => f.toFun)
      {
        toNonarchAddGroupSeminorm :=
          { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝, neg' := neg'✝ },
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    (fun f => f.toFun) g
⊢ {
      toNonarchAddGroupSeminorm :=
        { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝, neg' := neg'✝ },
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk.mk.mk
ι : Type u_1
R : Type u_2
R' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹ : AddGroup E
inst✝ : AddGroup F
p q : NonarchAddGroupNorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝ :
  ∀ (r s : E),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (r + s) ≤
      max (ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } r)
        (ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } s)
neg'✝ :
  ∀ (r : E),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (-r) =
      ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } r
eq_zero_of_map_eq_zero'✝¹ :
  ∀ (x : E),
    ZeroHom.toFun
          { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝,
              neg' := neg'✝ }.toZeroHom
          x =
        0 →
      x = 0
toNonarchAddGroupSeminorm✝ : NonarchAddGroupSeminorm E
eq_zero_of_map_eq_zero'✝ : ∀ (x : E), ZeroHom.toFun toNonarchAddGroupSeminorm✝.toZeroHom x = 0 → x = 0
h :
  (fun f => f.toFun)
      {
        toNonarchAddGroupSeminorm :=
          { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝, neg' := neg'✝ },
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f => f.toFun)
      { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ {
      toNonarchAddGroupSeminorm :=
        { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, add_le_max' := add_le_max'✝, neg' := neg'✝ },
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
[PROOFSTEP]
congr


[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → ℝ
g : ι' → ℝ
hf : Summable f
hg : Summable g
hf' : 0 ≤ f
hg' : 0 ≤ g
⊢ Summable fun x => ∑' (y : ι'), f (x, y).fst * g (x, y).snd
[PROOFSTEP]
simpa only [hg.tsum_mul_left _] using hf.mul_right (∑' x, g x)
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ kl in antidiagonal n, f kl.fst * g kl.snd‖
[PROOFSTEP]
have :=
  summable_sum_mul_antidiagonal_of_summable_mul
    (Summable.mul_of_nonneg hf hg (fun _ => norm_nonneg _) fun _ => norm_nonneg _)
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
⊢ Summable fun n => ‖∑ kl in antidiagonal n, f kl.fst * g kl.snd‖
[PROOFSTEP]
refine' summable_of_nonneg_of_le (fun _ => norm_nonneg _) _ this
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
⊢ ∀ (b : ℕ), ‖∑ kl in antidiagonal b, f kl.fst * g kl.snd‖ ≤ ∑ kl in antidiagonal b, ‖f kl.fst‖ * ‖g kl.snd‖
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
n : ℕ
⊢ ‖∑ kl in antidiagonal n, f kl.fst * g kl.snd‖ ≤ ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
[PROOFSTEP]
calc
  ‖∑ kl in antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl in antidiagonal n, ‖f kl.1 * g kl.2‖ := norm_sum_le _ _
  _ ≤ ∑ kl in antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ := by gcongr; apply norm_mul_le
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
n : ℕ
⊢ ∑ kl in antidiagonal n, ‖f kl.fst * g kl.snd‖ ≤ ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
[PROOFSTEP]
gcongr
[GOAL]
case h
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
n : ℕ
i✝ : ℕ × ℕ
a✝ : i✝ ∈ antidiagonal n
⊢ ‖f i✝.fst * g i✝.snd‖ ≤ ‖f i✝.fst‖ * ‖g i✝.snd‖
[PROOFSTEP]
apply norm_mul_le
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ k in range (n + 1), f k * g (n - k)‖
[PROOFSTEP]
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ ij in antidiagonal n, f ij.fst * g ij.snd‖
[PROOFSTEP]
exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k in range (n + 1), f k * g (n - k)
[PROOFSTEP]
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij in antidiagonal n, f ij.fst * g ij.snd
[PROOFSTEP]
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg


[GOAL]
V : SemiNormedGroupCat
v : ↑V
⊢ ‖(fun v => ↑↑V v) v‖ ≤ 1 * ‖v‖
[PROOFSTEP]
simp
[GOAL]
V : SemiNormedGroupCat
W : SemiNormedGroupCat
⊢ ∀ (P Q R : SemiNormedGroupCat) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
intros _ Q _ f f' g
[GOAL]
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q R✝ : SemiNormedGroupCat
f f' : P✝ ⟶ Q
g : Q ⟶ R✝
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
ext x
[GOAL]
case h
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q R✝ : SemiNormedGroupCat
f f' : P✝ ⟶ Q
g : Q ⟶ R✝
x : ↑P✝
⊢ ↑((f + f') ≫ g) x = ↑(f ≫ g + f' ≫ g) x
[PROOFSTEP]
rw [NormedAddGroupHom.add_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply,
  @NormedAddGroupHom.add_apply _ _ (_) (_)]
[GOAL]
case h
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q R✝ : SemiNormedGroupCat
f f' : P✝ ⟶ Q
g : Q ⟶ R✝
x : ↑P✝
⊢ ↑g (↑f x + ↑f' x) = ↑g (↑f x) + ↑g (↑f' x)
[PROOFSTEP]
convert map_add g (f x) (f' x)
[GOAL]
V : SemiNormedGroupCat
W : SemiNormedGroupCat
⊢ ∀ (P Q R : SemiNormedGroupCat) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
intros
[GOAL]
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q✝ R✝ : SemiNormedGroupCat
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
[PROOFSTEP]
ext
  -- Porting note: failing simps probably due to instance synthesis issues with concrete
      -- cats; see the gymnastics below for what used to be
      -- simp only [add_apply, comp_apply. map_add]
[GOAL]
case h
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q✝ R✝ : SemiNormedGroupCat
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
x✝ : ↑P✝
⊢ ↑(f✝ ≫ (g✝ + g'✝)) x✝ = ↑(f✝ ≫ g✝ + f✝ ≫ g'✝) x✝
[PROOFSTEP]
rw [NormedAddGroupHom.add_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply,
  @NormedAddGroupHom.add_apply _ _ (_) (_)]