R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ (∑ i in range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i) = ∑ i in range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ (∑ i in range n, t ^ i + ∑' (i : ℕ), t ^ (i + n)) = ∑ i in range n, t ^ i + t ^ n * inverse (1 - t)
simp only [inverse_one_sub t ht, add_comm _ n, pow_add, this.tsum_mul_left]
no goals
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ (∑ i in range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i) = ∑ i in range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹
rfl