no goals
⊢ succ 0 * choose 0 0 = choose (succ 0) (succ 0) * succ 0
decide
no goals
k : ℕ
⊢ succ 0 * choose 0 (k + 1) = choose (succ 0) (succ (k + 1)) * succ (k + 1)
simp [choose]
no goals
n : ℕ
⊢ succ (n + 1) * choose (n + 1) 0 = choose (succ (n + 1)) (succ 0) * succ 0
simp [choose, mul_succ, succ_eq_add_one, add_comm]
no goals
n k : ℕ
⊢ succ (n + 1) * choose (n + 1) (k + 1) = choose (succ (n + 1)) (succ (k + 1)) * succ (k + 1)
rw [choose_succ_succ (succ n) (succ k), add_mul, ← succ_mul_choose_eq n, mul_succ, ←
  succ_mul_choose_eq n, add_right_comm, ← mul_add, ← choose_succ_succ, ← succ_mul]