case base
α : Type u
β : Type v
X : Type ?u.8135
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i in Finset.Ico m m, edist (f i) (f (i + 1))

case succ
α : Type u
β : Type v
X : Type ?u.8135
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n n✝ : ℕ
hn✝ : m ≤ n✝
a✝ : edist (f m) (f n✝) ≤ ∑ i in Finset.Ico m n✝, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n✝ + 1)) ≤ ∑ i in Finset.Ico m (n✝ + 1), edist (f i) (f (i + 1))
α : Type u
β : Type v
X : Type ?u.8135
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ edist (f m) (f n) ≤ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1))
induction n, h using Nat.le_induction
case succ
α : Type u
β : Type v
X : Type ?u.8135
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n n✝ : ℕ
hn✝ : m ≤ n✝
a✝ : edist (f m) (f n✝) ≤ ∑ i in Finset.Ico m n✝, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n✝ + 1)) ≤ ∑ i in Finset.Ico m (n✝ + 1), edist (f i) (f (i + 1))
case base
α : Type u
β : Type v
X : Type ?u.8135
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i in Finset.Ico m m, edist (f i) (f (i + 1))

case succ
α : Type u
β : Type v
X : Type ?u.8135
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n n✝ : ℕ
hn✝ : m ≤ n✝
a✝ : edist (f m) (f n✝) ≤ ∑ i in Finset.Ico m n✝, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n✝ + 1)) ≤ ∑ i in Finset.Ico m (n✝ + 1), edist (f i) (f (i + 1))
case base => rw [Finset.Ico_self, Finset.sum_empty, edist_self]
no goals
case succ
α : Type u
β : Type v
X : Type ?u.8135
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n n✝ : ℕ
hn✝ : m ≤ n✝
a✝ : edist (f m) (f n✝) ≤ ∑ i in Finset.Ico m n✝, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n✝ + 1)) ≤ ∑ i in Finset.Ico m (n✝ + 1), edist (f i) (f (i + 1))
case succ n hle ihn =>
  calc
    edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_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
α : Type u
β : Type v
X : Type ?u.8135
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i in Finset.Ico m m, edist (f i) (f (i + 1))
rw [Finset.Ico_self, Finset.sum_empty, edist_self]
no goals
α : Type u
β : Type v
X : Type ?u.8135
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n + 1)) ≤ ∑ i in Finset.Ico m (n + 1), edist (f i) (f (i + 1))
calc
  edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_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 }