no goals
case zero
n : ℕ
⊢ choose n zero * (n + 1) = choose (n + 1) zero * (n + 1 - zero)
simp
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)

case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
case succ
n k : ℕ
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
obtain hk | hk := le_or_lt (k + 1) (n + 1)
no goals
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
  mul_tsub, add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
no goals
case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul,
  zero_mul]