Theorem: mchoose_one' (DividedPowers/ForMathlib/CombinatoricsLemmas.lean)

State before:
m : ℕ
⊢ mchoose m 1 = 1
Tactic:
simp only [mchoose, mul_one, add_tsub_cancel_right, ge_iff_le, le_refl,
  tsub_eq_zero_of_le, Nat.choose_zero_right, Finset.prod_const_one]
State after:
no goals