[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
hd : Summable d
⊢ CauchySeq f
[PROOFSTEP]
refine
  EMetric.cauchySeq_iff_NNReal.2 fun ε εpos =>
    ?_
      -- Actually we need partial sums of `d` to be a Cauchy sequence
[GOAL]
α : 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) < ↑ε
[PROOFSTEP]
replace hd : CauchySeq fun n : ℕ => ∑ x in range n, d x :=
  let ⟨_, H⟩ := hd
  H.tendsto_sum_nat.cauchySeq
[GOAL]
α : 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) < ↑ε
[PROOFSTEP]
refine (Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn => ?_
[GOAL]
α : 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) < ↑ε
[PROOFSTEP]
specialize hN n hn
[GOAL]
α : 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) < ↑ε
[PROOFSTEP]
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 
[GOAL]
α : 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) < ↑ε
[PROOFSTEP]
rw [edist_comm]
  -- Then use `hf` to simplify the goal to the same form
[GOAL]
α : 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) < ↑ε
[PROOFSTEP]
refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ => hf _) ?_
[GOAL]
α : 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) < ↑ε
[PROOFSTEP]
exact_mod_cast hN.1
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
⊢ CauchySeq f
[PROOFSTEP]
refine' Metric.cauchySeq_iff'.2 fun ε εpos => _
[GOAL]
α : 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) < ε
[PROOFSTEP]
replace hd : CauchySeq fun n : ℕ => ∑ x in range n, d x :=
  let ⟨_, H⟩ := hd
  H.tendsto_sum_nat.cauchySeq
[GOAL]
α : 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) < ε
[PROOFSTEP]
refine' (Metric.cauchySeq_iff'.1 hd ε εpos).imp fun N hN n hn => _
[GOAL]
α : 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) < ε
[PROOFSTEP]
have hsum := hN n hn
[GOAL]
α : 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) < ε
[PROOFSTEP]
rw [Real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum 
[GOAL]
α : 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 : |∑ k in Ico N n, d k| < ε
⊢ dist (f n) (f N) < ε
[PROOFSTEP]
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
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), d (n + m)
[PROOFSTEP]
refine' le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm => _⟩)
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)
[PROOFSTEP]
refine' le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ => hf _) _
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ i in Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)
[PROOFSTEP]
rw [sum_Ico_eq_sum_range]
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ k in range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
[PROOFSTEP]
refine' sum_le_tsum (range _) (fun _ _ => le_trans dist_nonneg (hf _)) _
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ Summable fun k => d (n + k)
[PROOFSTEP]
exact hd.comp_injective (add_right_injective n)
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ tsum d
[PROOFSTEP]
simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable fun n => dist (f n) (f (Nat.succ n))
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f (Nat.succ n))
[PROOFSTEP]
simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0
