case empty
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i in ∅, (f i)! ∣ (∑ i in ∅, f i)!

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)!
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i in s, (f i)! ∣ (∑ i in s, f i)!
induction' s using Finset.induction with a' s' has ih
no goals
case empty
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i in ∅, (f i)! ∣ (∑ i in ∅, f i)!
simp only [Finset.sum_empty, Finset.prod_empty, factorial]
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)!
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)!
simp only [Finset.prod_insert has, Finset.sum_insert has]
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)!
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)!
refine' dvd_trans (mul_dvd_mul_left (f a')! ih) _
no goals
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)!
apply Nat.factorial_mul_factorial_dvd_factorial_add