[GOAL]
m n k : ℕ
⊢ choose (m + n) k = ∑ ij in antidiagonal k, choose m ij.fst * choose n ij.snd
[PROOFSTEP]
calc
  (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, Nat.cast_id]
  _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
  _ = ∑ ij : ℕ × ℕ in antidiagonal k, m.choose ij.1 * n.choose ij.2 :=
    by
    rw [coeff_mul, Finset.sum_congr rfl]
    simp only [coeff_X_add_one_pow, Nat.cast_id, eq_self_iff_true, imp_true_iff]
[GOAL]
m n k : ℕ
⊢ choose (m + n) k = coeff ((X + 1) ^ (m + n)) k
[PROOFSTEP]
rw [coeff_X_add_one_pow, Nat.cast_id]
[GOAL]
m n k : ℕ
⊢ coeff ((X + 1) ^ (m + n)) k = coeff ((X + 1) ^ m * (X + 1) ^ n) k
[PROOFSTEP]
rw [pow_add]
[GOAL]
m n k : ℕ
⊢ coeff ((X + 1) ^ m * (X + 1) ^ n) k = ∑ ij in antidiagonal k, choose m ij.fst * choose n ij.snd
[PROOFSTEP]
rw [coeff_mul, Finset.sum_congr rfl]
[GOAL]
m n k : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k → coeff ((X + 1) ^ m) x.fst * coeff ((X + 1) ^ n) x.snd = choose m x.fst * choose n x.snd
[PROOFSTEP]
simp only [coeff_X_add_one_pow, Nat.cast_id, eq_self_iff_true, imp_true_iff]
