no goals
α : Type u_1
β : Type ?u.444903
ι : Type ?u.444906
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ edist (f 0) a ≤ 2 * C
simpa only [_root_.pow_zero, div_eq_mul_inv, inv_one, mul_one] using
  edist_le_of_edist_le_geometric_two_of_tendsto C hu ha 0