α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ multinomial (insert a s) f = (f a + Finset.sum s f)! / ((f a)! * (f a + Finset.sum s f - f a)!) * multinomial s f
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ multinomial (insert a s) f = choose (f a + Finset.sum s f) (f a) * multinomial s f
rw [choose_eq_factorial_div_factorial (le.intro rfl)]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ (f a + ∑ i in s, f i)! / ((f a)! * ∏ i in s, (f i)!) =
    (f a + Finset.sum s f)! / ((f a)! * (Finset.sum s f)!) * ((∑ i in s, f i)! / ∏ i in s, (f i)!)
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ multinomial (insert a s) f = (f a + Finset.sum s f)! / ((f a)! * (f a + Finset.sum s f - f a)!) * multinomial s f
simp only [multinomial, Nat.add_sub_cancel_left, Finset.sum_insert h, Finset.prod_insert h,
  Function.comp_apply]
no goals
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ (f a + ∑ i in s, f i)! / ((f a)! * ∏ i in s, (f i)!) =
    (f a + Finset.sum s f)! / ((f a)! * (Finset.sum s f)!) * ((∑ i in s, f i)! / ∏ i in s, (f i)!)
rw [div_mul_div_comm ((f a).factorial_mul_factorial_dvd_factorial_add (s.sum f))
    (prod_factorial_dvd_factorial_sum _ _),
  mul_comm (f a)! (s.sum f)!, mul_assoc, mul_comm _ (s.sum f)!,
  Nat.mul_div_mul_left _ _ (factorial_pos _)]