rw [Finset.sum_range_succ,
    Nat.succ_eq_add_one,
    Nat.choose_self,
    Nat.sub_self,
    pow_zero,
    mul_one,
    one_mul,
    Finset.sum_range_succ',
    Nat.choose_zero_right,
    one_mul,
    Nat.sub_zero,
    pow_zero,
    mul_one]
case succ
x y n : ℕ
ih : (x + y) ^ n = ∑ k in Finset.range (n + 1), Nat.choose n k * x ^ (n - k) * y ^ k
⊢ (x + y) ^ Nat.succ n = ∑ k in Finset.range (Nat.succ n + 1), Nat.choose (Nat.succ n) k * x ^ (Nat.succ n - k) * y ^ k
case succ
x y n : ℕ
ih : (x + y) ^ n = ∑ k in Finset.range (n + 1), Nat.choose n k * x ^ (n - k) * y ^ k
⊢ (x + y) ^ (n + 1) =
    ∑ k in Finset.range n, Nat.choose (n + 1) (k + 1) * x ^ (n + 1 - (k + 1)) * y ^ (k + 1) + x ^ (n + 1) + y ^ (n + 1)