no goals
α : Type u
β : Type v
X : Type ?u.11251
ι : Type ?u.11254
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ dist (f m) (f n) ≤ ∑ i in Finset.Ico m n, dist (f i) (f (i + 1))
induction n, h using Nat.le_induction with
| base => rw [Finset.Ico_self, Finset.sum_empty, dist_self]
| succ n hle ihn =>
  calc
    dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_triangle _ _ _
    _ ≤ (∑ i in Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
    _ = ∑ i in Finset.Ico m (n + 1), _ := by
    { rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp }
no goals
case base
α : Type u
β : Type v
X : Type ?u.11251
ι : Type ?u.11254
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
⊢ dist (f m) (f m) ≤ ∑ i in Finset.Ico m m, dist (f i) (f (i + 1))
rw [Finset.Ico_self, Finset.sum_empty, dist_self]
no goals
case succ
α : Type u
β : Type v
X : Type ?u.11251
ι : Type ?u.11254
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i in Finset.Ico m n, dist (f i) (f (i + 1))
⊢ dist (f m) (f (n + 1)) ≤ ∑ i in Finset.Ico m (n + 1), dist (f i) (f (i + 1))
calc
  dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_triangle _ _ _
  _ ≤ (∑ i in Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
  _ = ∑ i in Finset.Ico m (n + 1), _ := by
  { rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp }