no goals
α✝ : Type u
α : Type u_1
inst✝ : CommRing α
x : α
n : ℕ
⊢ ∑ i in range n, x ^ i * x ^ (n - 1 - i) = ∑ i in range n, x ^ (i + (n - 1 - i))
simp_rw [← pow_add]
no goals
α✝ : Type u
α : Type u_1
inst✝ : CommRing α
x : α
n : ℕ
⊢ card (range n) • x ^ (n - 1) = ↑n * x ^ (n - 1)
rw [Finset.card_range, nsmul_eq_mul]