no goals
α : Type ?u.68751
β : Type ?u.68754
ι : Type ?u.68757
r : ℝ
h₁ : 0 ≤ r
h₂ : r < 1
this✝ : r ≠ 1
this : Tendsto (fun n => (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹))
⊢ Tendsto (fun n => ∑ i in Finset.range n, r ^ i) atTop (𝓝 (1 - r)⁻¹)
simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv]