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

State before:
n : ℕ
⊢ mchoose 1 n = 1
Tactic:
simp only [mchoose, Finset.range_one, Finset.prod_singleton, zero_mul,
  zero_add, Nat.choose_self]
State after:
no goals