-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem cauchySeq_of_edist_le_of_summable {f : ℕ → α} (d : ℕ → ℝ≥0)
    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : Summable d) : CauchySeq f

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
⊢ ∑ i ∈ Finset.Ico N n, ↑(d i) < ↑ε

Tactic:
exact mod_cast hN.1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN : dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε
⊢ edist (f n) (f N) < ↑ε

Tactic:
rw [dist_nndist, NNReal.nndist_eq, ← Finset.sum_range_add_sum_Ico _ hn, add_tsub_cancel_left,
  NNReal.coe_lt_coe, max_lt_iff] at hN

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
⊢ edist (f n) (f N) < ↑ε

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
⊢ edist (f n) (f N) < ↑ε

Tactic:
rw [edist_comm]

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
⊢ edist (f N) (f n) < ↑ε

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε

Tactic:
refine (Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn ↦ ?_

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N : ℕ
hN : ∀ n ≥ N, dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε
n : ℕ
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N : ℕ
hN : ∀ n ≥ N, dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε
n : ℕ
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε

Tactic:
specialize hN n hn

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN : dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε
⊢ edist (f n) (f N) < ↑ε

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
hd : Summable d
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε

Tactic:
replace hd : CauchySeq fun n : ℕ ↦ ∑ x ∈ Finset.range n, d x :=
  let ⟨_, H⟩ := hd
  H.tendsto_sum_nat.cauchySeq

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
⊢ edist (f N) (f n) < ↑ε

Tactic:
refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ ↦ hf _) ?_

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
⊢ ∑ i ∈ Finset.Ico N n, ↑(d i) < ↑ε

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
hd : Summable d
⊢ CauchySeq f

Tactic:
refine EMetric.cauchySeq_iff_NNReal.2 fun ε εpos ↦ ?_

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
hd : Summable d
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε