Theorem: binomial_theorem (meetings/ex3.lean)

State before:
x y n : ℕ
⊢ (x + y) ^ n = ∑ k in Finset.range (n + 1), Nat.choose n k * x ^ (n - k) * y ^ k
Tactic:
induction' n with n ih
State after:
case zero
x y : ℕ
⊢ (x + y) ^ Nat.zero = ∑ k in Finset.range (Nat.zero + 1), Nat.choose Nat.zero k * x ^ (Nat.zero - 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) ^ Nat.succ n = ∑ k in Finset.range (Nat.succ n + 1), Nat.choose (Nat.succ n) k * x ^ (Nat.succ n - k) * y ^ k

State before:
case zero
x y : ℕ
⊢ (x + y) ^ Nat.zero = ∑ k in Finset.range (Nat.zero + 1), Nat.choose Nat.zero k * x ^ (Nat.zero - k) * y ^ k
Tactic:
simp
State after:
no goals

State before:
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
Tactic:
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]
State after:
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)

State before:
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)
Tactic:
simp_rw [Nat.choose_succ_succ']
State after:
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)