simp_rw [Nat.choose_succ_succ']
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)
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) =
    ∑ x_1 in Finset.range n, (Nat.choose n x_1 + Nat.choose n (x_1 + 1)) * x ^ (n + 1 - (x_1 + 1)) * y ^ (x_1 + 1) +
        x ^ (n + 1) +
      y ^ (n + 1)