no goals
α : Type u_1
β : Type ?u.569045
γ : Type ?u.569048
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ edist (f 0) a ≤ ∑' (m : ℕ), d m
simpa using edist_le_tsum_of_edist_le_of_tendsto d hf ha 0