[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i in s, (f i)! ∣ (∑ i in s, f i)!
[PROOFSTEP]
classical
induction' s using Finset.induction with a' s' has ih
· simp only [Finset.sum_empty, Finset.prod_empty, factorial]
· simp only [Finset.prod_insert has, Finset.sum_insert has]
  refine' dvd_trans (mul_dvd_mul_left (f a')! ih) _
  apply Nat.factorial_mul_factorial_dvd_factorial_add
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i in s, (f i)! ∣ (∑ i in s, f i)!
[PROOFSTEP]
induction' s using Finset.induction with a' s' has ih
[GOAL]
case empty
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i in ∅, (f i)! ∣ (∑ i in ∅, f i)!
[PROOFSTEP]
simp only [Finset.sum_empty, Finset.prod_empty, factorial]
[GOAL]
case insert
α : Type u_1
s : Finset α
f : α → ℕ
a' : α
s' : Finset α
has : ¬a' ∈ s'
ih : ∏ i in s', (f i)! ∣ (∑ i in s', f i)!
⊢ ∏ i in insert a' s', (f i)! ∣ (∑ i in insert a' s', f i)!
[PROOFSTEP]
simp only [Finset.prod_insert has, Finset.sum_insert has]
[GOAL]
case insert
α : Type u_1
s : Finset α
f : α → ℕ
a' : α
s' : Finset α
has : ¬a' ∈ s'
ih : ∏ i in s', (f i)! ∣ (∑ i in s', f i)!
⊢ (f a')! * ∏ i in s', (f i)! ∣ (f a' + ∑ i in s', f i)!
[PROOFSTEP]
refine' dvd_trans (mul_dvd_mul_left (f a')! ih) _
[GOAL]
case insert
α : Type u_1
s : Finset α
f : α → ℕ
a' : α
s' : Finset α
has : ¬a' ∈ s'
ih : ∏ i in s', (f i)! ∣ (∑ i in s', f i)!
⊢ (f a')! * (∑ i in s', f i)! ∣ (f a' + ∑ i in s', f i)!
[PROOFSTEP]
apply Nat.factorial_mul_factorial_dvd_factorial_add
