α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i in range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 ^ n = (x + 1) ^ n
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
have := (Commute.one_right x).geom_sum₂_mul_add n
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i in range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 ^ n = (x + 1) ^ n
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
rw [one_pow, geom_sum₂_with_one] at this
no goals
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
exact this