α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f n) (f N) < ε
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
⊢ CauchySeq f
refine' Metric.cauchySeq_iff'.2 fun ε εpos => _
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f n) (f N) < ε
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f n) (f N) < ε
replace hd : CauchySeq fun n : ℕ => ∑ x in range n, d x :=
  let ⟨_, H⟩ := hd
  H.tendsto_sum_nat.cauchySeq
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
n : ℕ
hn : n ≥ N
⊢ dist (f n) (f N) < ε
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f n) (f N) < ε
refine' (Metric.cauchySeq_iff'.1 hd ε εpos).imp fun N hN n hn => _
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
n : ℕ
hn : n ≥ N
hsum : dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
⊢ dist (f n) (f N) < ε
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
n : ℕ
hn : n ≥ N
⊢ dist (f n) (f N) < ε
have hsum := hN n hn
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
n : ℕ
hn : n ≥ N
hsum : abs (∑ k in Ico N n, d k) < ε
⊢ dist (f n) (f N) < ε
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
n : ℕ
hn : n ≥ N
hsum : dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
⊢ dist (f n) (f N) < ε
rw [Real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum
no goals
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
n : ℕ
hn : n ≥ N
hsum : abs (∑ k in Ico N n, d k) < ε
⊢ dist (f n) (f N) < ε
calc
  dist (f n) (f N) = dist (f N) (f n) := dist_comm _ _
  _ ≤ ∑ x in Ico N n, d x := dist_le_Ico_sum_of_dist_le hn fun _ _ => hf _
  _ ≤ |∑ x in Ico N n, d x| := le_abs_self _
  _ < ε := hsum