-- Mathlib/Data/Nat/Choose/Multinomial.lean
lemma multinomial_two_mul_le_mul_multinomial :
    multinomial s (fun i ↦ 2 * f i) ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * multinomial s f

Proof state:
case bc.h
ι : Type u_1
s : Finset ι
f : ι → ℕ
i✝ : ι
a✝ : i✝ ∈ s
⊢ (2 * f i✝)‼ ≤ (2 * f i✝)!

Tactic:
exact doubleFactorial_le_factorial _

Result:
no goals

Proof state:
case bc
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! ≤ ((2 * ∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)!

Tactic:
exact Nat.factorial_two_mul_le _

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (multinomial s fun i => 2 * f i) ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * multinomial s f

Tactic:
rw [multinomial, multinomial, ← mul_sum,
  ← Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum ..)]

Result:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! / ∏ i ∈ s, (2 * f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)! ≤
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!

Tactic:
gcongr

Result:
case bc.h
ι : Type u_1
s : Finset ι
f : ι → ℕ
i✝ : ι
a✝ : i✝ ∈ s
⊢ 2 ^ f i✝ * (f i✝)! ≤ (2 * f i✝)!

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ∏ i ∈ s, (f i)! ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case bc.h
ι : Type u_1
s : Finset ι
f : ι → ℕ
i✝ : ι
a✝ : i✝ ∈ s
⊢ 2 ^ f i✝ * (f i✝)! ≤ (2 * f i✝)!

Tactic:
rw [← doubleFactorial_two_mul]

Result:
case bc.h
ι : Type u_1
s : Finset ι
f : ι → ℕ
i✝ : ι
a✝ : i✝ ∈ s
⊢ (2 * f i✝)‼ ≤ (2 * f i✝)!

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((∏ i ∈ s, 2 ^ f i) * (∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ((∏ x ∈ s, 2 ^ f x) * ∏ x ∈ s, (f x)!)

Tactic:
ring

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!

Tactic:
calc
  (2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
    ≤ ((2 * ∑ i ∈ s, f i) ^ (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!) * ∏ i ∈ s, (f i)! := by
    gcongr; exact Nat.factorial_two_mul_le _
  _ = ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)! := by
    rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]; ring
  _ ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)! := by
    gcongr
    rw [← doubleFactorial_two_mul]
    exact doubleFactorial_le_factorial _

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! ≤ ((2 * ∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!

Tactic:
gcongr

Result:
case bc
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! ≤ ((2 * ∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)!

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((2 * ∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)!

Tactic:
rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]

Result:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((∏ i ∈ s, 2 ^ f i) * (∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ((∏ x ∈ s, 2 ^ f x) * ∏ x ∈ s, (f x)!)

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! / ∏ i ∈ s, (2 * f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!

Tactic:
refine Nat.div_le_div_of_mul_le_mul (by positivity)
  ((prod_factorial_dvd_factorial_sum ..).trans (Nat.dvd_mul_left ..)) ?_

Result:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!