α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
set v : ℕ → α := fun n ↦ if n < N then 0 else u n
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
have hC : 0 ≤ C :=
  (zero_le_mul_right <| pow_pos hr₀ N).mp ((norm_nonneg _).trans <| h N <| le_refl N)
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
have : ∀ n ≥ N, u n = v n := by
  intro n hn
  simp [hn, if_neg (not_lt.mpr hn)]
case refine'_1
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
⊢ ℝ

case refine'_2
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
⊢ ∀ (n : ℕ), ‖v n‖ ≤ ?refine'_1 * r ^ n
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
refine'
  cauchySeq_sum_of_eventually_eq this (NormedAddCommGroup.cauchy_series_of_le_geometric' hr₁ _)
case refine'_2
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
⊢ ‖v n‖ ≤ C * r ^ n
case refine'_2
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
⊢ ∀ (n : ℕ), ‖v n‖ ≤ C * r ^ n
intro n
case refine'_2
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
⊢ ‖if n < N then 0 else u n‖ ≤ C * r ^ n
case refine'_2
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
⊢ ‖v n‖ ≤ C * r ^ n
simp only
case refine'_2.inl
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : n < N
⊢ ‖0‖ ≤ C * r ^ n

case refine'_2.inr
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : ¬n < N
⊢ ‖u n‖ ≤ C * r ^ n
case refine'_2
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
⊢ ‖if n < N then 0 else u n‖ ≤ C * r ^ n
split_ifs with H
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
n : ℕ
hn : n ≥ N
⊢ u n = v n
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
⊢ ∀ (n : ℕ), n ≥ N → u n = v n
intro n hn
no goals
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
n : ℕ
hn : n ≥ N
⊢ u n = v n
simp [hn, if_neg (not_lt.mpr hn)]
no goals
case refine'_1
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
⊢ ℝ
exact C
case refine'_2.inl
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : n < N
⊢ 0 ≤ C * r ^ n
case refine'_2.inl
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : n < N
⊢ ‖0‖ ≤ C * r ^ n
rw [norm_zero]
no goals
case refine'_2.inl
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : n < N
⊢ 0 ≤ C * r ^ n
exact mul_nonneg hC (pow_nonneg hr₀.le _)
case refine'_2.inr
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : N ≤ n
⊢ ‖u n‖ ≤ C * r ^ n
case refine'_2.inr
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : ¬n < N
⊢ ‖u n‖ ≤ C * r ^ n
push_neg at H
no goals
case refine'_2.inr
α : Type u_1
β : Type ?u.1175572
ι : Type ?u.1175575
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : N ≤ n
⊢ ‖u n‖ ≤ C * r ^ n
exact h _ H