α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
h₁ : f a = 1
⊢ (∑ i in insert a s, f i)! / ∏ i in insert a s, (f i)! = succ (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
h₁ : f a = 1
⊢ multinomial (insert a s) f = succ (Finset.sum s f) * multinomial s f
simp only [multinomial, one_mul, factorial]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
h₁ : f a = 1
⊢ (∑ x in s, f x + 1) * (∑ x in s, f x)! / (1! * ∏ x in s, (f x)!) =
    succ (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
h₁ : f a = 1
⊢ (∑ i in insert a s, f i)! / ∏ i in insert a s, (f i)! = succ (Finset.sum s f) * ((∑ i in s, f i)! / ∏ i in s, (f i)!)
rw [Finset.sum_insert h, Finset.prod_insert h, h₁, add_comm, ← succ_eq_add_one, factorial_succ]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
h₁ : f a = 1
⊢ (∑ x in s, f x + 1) * (∑ x in s, f x)! / ∏ x in s, (f x)! =
    succ (Finset.sum s f) * ((∑ x in s, f x)! / ∏ x in s, (f x)!)
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
h₁ : f a = 1
⊢ (∑ x in s, f x + 1) * (∑ x in s, f x)! / (1! * ∏ x in s, (f x)!) =
    succ (Finset.sum s f) * ((∑ i in s, f i)! / ∏ i in s, (f i)!)
simp only [factorial_one, one_mul, Function.comp_apply, factorial, mul_one, ← one_eq_succ_zero]
no goals
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
h₁ : f a = 1
⊢ (∑ x in s, f x + 1) * (∑ x in s, f x)! / ∏ x in s, (f x)! =
    succ (Finset.sum s f) * ((∑ x in s, f x)! / ∏ x in s, (f x)!)
rw [Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)]