case e
n k : ℕ
⊢ (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)

n k : ℕ
e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
n k : ℕ
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
have e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
n k : ℕ
e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
case e
n k : ℕ
⊢ (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)

n k : ℕ
e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
rw [← right_distrib, ← choose_succ_succ, succ_mul_choose_eq]
no goals
n k : ℕ
e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
rw [← tsub_eq_of_eq_add_rev e, mul_comm, ← mul_tsub, add_tsub_add_eq_tsub_right]