α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
hd : Summable d
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
hd : Summable d
⊢ CauchySeq f
refine EMetric.cauchySeq_iff_NNReal.2 fun ε εpos => ?_
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
hd : Summable d
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (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✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
ε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
⊢ edist (f n) (f N) < ↑ε
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε
refine (Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn => ?_
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : dist (∑ x in range n, d x) (∑ x in range N, d x) < ↑ε
⊢ edist (f n) (f N) < ↑ε
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
ε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
⊢ edist (f n) (f N) < ↑ε
specialize hN n hn
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : ∑ k in Ico N n, d k < ε ∧ ∑ x in range N, d x - (∑ k in range N, d k + ∑ k in Ico N n, d k) < ε
⊢ edist (f n) (f N) < ↑ε
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : dist (∑ x in range n, d x) (∑ x in range N, d x) < ↑ε
⊢ edist (f n) (f N) < ↑ε
rw [dist_nndist, NNReal.nndist_eq, ← sum_range_add_sum_Ico _ hn, add_tsub_cancel_left,
  NNReal.coe_lt_coe, max_lt_iff] at hN
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : ∑ k in Ico N n, d k < ε ∧ ∑ x in range N, d x - (∑ k in range N, d k + ∑ k in Ico N n, d k) < ε
⊢ edist (f N) (f n) < ↑ε
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : ∑ k in Ico N n, d k < ε ∧ ∑ x in range N, d x - (∑ k in range N, d k + ∑ k in Ico N n, d k) < ε
⊢ edist (f n) (f N) < ↑ε
rw [edist_comm]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : ∑ k in Ico N n, d k < ε ∧ ∑ x in range N, d x - (∑ k in range N, d k + ∑ k in Ico N n, d k) < ε
⊢ ∑ i in Ico N n, ↑(d i) < ↑ε
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : ∑ k in Ico N n, d k < ε ∧ ∑ x in range N, d x - (∑ k in range N, d k + ∑ k in Ico N n, d k) < ε
⊢ edist (f N) (f n) < ↑ε
refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ => hf _) ?_
no goals
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : ∑ k in Ico N n, d k < ε ∧ ∑ x in range N, d x - (∑ k in range N, d k + ∑ k in Ico N n, d k) < ε
⊢ ∑ i in Ico N n, ↑(d i) < ↑ε
exact_mod_cast hN.1