ι : Type ?u.7861
α : Type ?u.7864
E : Type u_1
F : Type ?u.7870
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (∑ i in range n, f i) (∑ i in range N, f i) < ε
ι : Type ?u.7861
α : Type ?u.7864
E : Type u_1
F : Type ?u.7870
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
⊢ CauchySeq fun n => ∑ i in range n, f i
refine' Metric.cauchySeq_iff'.2 fun ε hε => _
ι : Type ?u.7861
α : Type ?u.7864
E : Type u_1
F : Type ?u.7870
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N : ℕ
hg : ∀ (n : ℕ), n ≥ N → dist (∑ i in range n, g i) (∑ i in range N, g i) < ε
n : ℕ
hn : n ≥ N
⊢ dist (∑ i in range n, f i) (∑ i in range N, f i) < ε
ι : Type ?u.7861
α : Type ?u.7864
E : Type u_1
F : Type ?u.7870
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (∑ i in range n, f i) (∑ i in range N, f i) < ε
refine' (Metric.cauchySeq_iff'.1 hg ε hε).imp fun N hg n hn => _
ι : Type ?u.7861
α : Type ?u.7864
E : Type u_1
F : Type ?u.7870
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : dist (∑ i in range n, g i) (∑ i in range N, g i) < ε
⊢ dist (∑ i in range n, f i) (∑ i in range N, f i) < ε
ι : Type ?u.7861
α : Type ?u.7864
E : Type u_1
F : Type ?u.7870
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N : ℕ
hg : ∀ (n : ℕ), n ≥ N → dist (∑ i in range n, g i) (∑ i in range N, g i) < ε
n : ℕ
hn : n ≥ N
⊢ dist (∑ i in range n, f i) (∑ i in range N, f i) < ε
specialize hg n hn
ι : Type ?u.7861
α : Type ?u.7864
E : Type u_1
F : Type ?u.7870
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : ‖∑ k in Ico N n, g k‖ < ε
⊢ ‖∑ k in Ico N n, f k‖ < ε
ι : Type ?u.7861
α : Type ?u.7864
E : Type u_1
F : Type ?u.7870
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : dist (∑ i in range n, g i) (∑ i in range N, g i) < ε
⊢ dist (∑ i in range n, f i) (∑ i in range N, f i) < ε
rw [dist_eq_norm, ← sum_Ico_eq_sub _ hn] at hg⊢
no goals
ι : Type ?u.7861
α : Type ?u.7864
E : Type u_1
F : Type ?u.7870
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : ‖∑ k in Ico N n, g k‖ < ε
⊢ ‖∑ k in Ico N n, f k‖ < ε
calc
  ‖∑ k in Ico N n, f k‖ ≤ ∑ k in _, ‖f k‖ := norm_sum_le _ _
  _ ≤ ∑ k in _, g k := (sum_le_sum fun x _ => hf x)
  _ ≤ ‖∑ k in _, g k‖ := (le_abs_self _)
  _ < ε := hg