no goals
α : 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
simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0