Theorem: mchoose_succ (DividedPowers/ForMathlib/CombinatoricsLemmas.lean)

State before:
m n : ℕ
⊢ mchoose (m + 1) n = (m * n + n - 1).choose (n - 1) * mchoose m n
Tactic:
simp only [mchoose, Finset.prod_range_succ, mul_comm]
State after:
no goals