calc
  dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry
  _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
  _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry
  _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry
  _ ≤ 1 / 2 ^ N * 2 := sorry
  _ < ε := sorry
case h.intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
k : ℕ
hn : N + k ≥ N
⊢ dist (u (N + k)) (u N) < ε
no goals