awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s) : Set α).Pairwise (Commute on x)
n : ℕ
ih :
  ∀ (n : ℕ),
    s.sum x ^ n =
      ∑ k : ↥(s.sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯
m : ↥((insert a s).sym n)
⊢ x a ^ Multiset.count a (↑(↑m : Sym α n) : Multiset α) *
        (↑(Multiset.filter (fun (x : α) ↦ a ≠ x) (↑(↑m : Sym α n) : Multiset α)).countPerms : R) *
      (Multiset.map x (Multiset.filter (fun (a_1 : α) ↦ ¬a = a_1) (↑(↑m : Sym α n) : Multiset α))).noncommProd ⋯ =
    x a ^
          (↑(Sigma.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                ((symInsertEquiv ha : (a : ↥((insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))) m)) :
            ℕ) *
        (↑(Multiset.countPerms (α := α)
              ((↑(↑(Sigma.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                          ((symInsertEquiv ha :
                              (a : ↥((insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                            m)) :
                      Sym α
                        (n -
                          (↑((symInsertEquiv ha :
                                    (a : ↥((insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                                  m).fst :
                            ℕ))) :
                  Multiset α) :
                Multiset α)) :
          R) *
      (Multiset.map x
            (↑(↑(Sigma.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                      ((symInsertEquiv ha : (a : ↥((insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                        m)) :
                  Sym α
                    (n -
                      (↑((symInsertEquiv ha : (a : ↥((insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                              m).fst :
                        ℕ))) :
              Multiset α)).noncommProd
        ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
f : α → R
n : ℕ
simp_rw :
  HPow.hPow (α := R) (∑ i ∈ s, f i) n =
    ∑ x ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s x) : R) (s.noncommProd (fun (i : α) ↦ f i ^ x i) ⋯)
⊢ HPow.hPow (α := R) (∑ i ∈ s, f i) n =
    ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (∏ i ∈ s, f i ^ k i)

Tactic:
simp_rw [← noncommProd_eq_prod]

Premises used: Finset.noncommProd_eq_prod
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
f : α → R
n : ℕ
rw rw₁ : HPow.hPow (α := R) (∑ i ∈ s, f i) n = HPow.hPow (α := R) (∑ i ∈ s, f i) n
⊢ HPow.hPow (α := R) (∑ i ∈ s, f i) n =
    ∑ x ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s x) : R) (s.noncommProd (fun (i : α) ↦ f i ^ x i) ⋯)

Tactic:
rw [← sum_pow_eq_sum_piAntidiag_of_commute _ _ fun _ _ _ _ _ ↦ Commute.all ..]

Premises used: Finset.sum_pow_eq_sum_piAntidiag_of_commute
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
x : α → R
n : ℕ
rw :
  ∑ i : ↥(s.sym n),
    (↑(↑(↑i : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑i : Sym α n) : Multiset α)).prod
| ∑ k ∈ s.sym n, (↑(↑k : Multiset α).countPerms : R) * (Multiset.map x (↑k : Multiset α)).prod

Tactic:
rw [← sum_coe_sort]

Premises used: Finset.sum_coe_sort
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
x : α → R
n : ℕ
conv_rhs :
  s.sum x ^ n =
    ∑ i : ↥(s.sym n),
      (↑(↑(↑i : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑i : Sym α n) : Multiset α)).prod
⊢ s.sum x ^ n = ∑ k ∈ s.sym n, (↑(↑k : Multiset α).countPerms : R) * (Multiset.map x (↑k : Multiset α)).prod

Tactic:
conv_rhs => rw [← sum_coe_sort]

Premises used: Finset.sum_coe_sort
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
x : α → R
n : ℕ
⊢ s.sum x ^ n =
    ∑ k : ↥(s.sym n),
      (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯

Tactic:
sum_pow_of_commute x s (fun _ _ _ _ _ ↦ Commute.all ..) n

Premises used: Finset.sum_pow_of_commute, Commute.all
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
x : α → R
n : ℕ
h :
  ∀ (x_1 : ↥(s.sym n)),
    Membership.mem (γ := Finset ↥(s.sym n)) univ x_1 →
      (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).prod =
        (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).noncommProd ⋯
⊢ s.sum x ^ n =
    ∑ i : ↥(s.sym n),
      (↑(↑(↑i : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑i : Sym α n) : Multiset α)).prod

Tactic:
convert! sum_pow_of_commute x s (fun _ _ _ _ _ ↦ Commute.all ..) n

Premises used: Finset.sum_pow_of_commute, Commute.all
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
x : α → R
n : ℕ
x_1 : ↥(s.sym n)
h_1 : Membership.mem (γ := Finset ↥(s.sym n)) univ x_1
h h₁ : (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).prod = (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).prod
⊢ (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).prod =
    (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).noncommProd ⋯

Tactic:
rw [Multiset.noncommProd_eq_prod]

Premises used: Multiset.noncommProd_eq_prod
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
rw :
  (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! / ∏ i ∈ s, (2 * f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!
⊢ (multinomial s fun (i : ι) ↦ 2 * f i) ≤ HPow.hPow (α := ℕ) (β := ℕ) (∑ 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 ..)]

Premises used: Finset.mul_sum, Nat.multinomial, Nat.prod_factorial_dvd_factorial_sum, Nat.mul_div_assoc
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Ne (α := ℕ) (∏ i ∈ s, (f i)!) 0

Tactic:
positivity
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
refine :
  (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! / ∏ i ∈ s, (2 * f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ 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 ..)) ?_

Premises used: Nat.prod_factorial_dvd_factorial_sum, Nat.dvd_mul_left, Nat.div_le_div_of_mul_le_mul, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
bc :
  (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! ≤
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! ≤
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!

Tactic:
Nat.factorial_two_mul_le _

Premises used: Nat.factorial_two_mul_le
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! ≤
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!

Tactic:
exact Nat.factorial_two_mul_le _

Premises used: Nat.factorial_two_mul_le
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
rw :
  (∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i)) * HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      ∏ i ∈ s, (f i)! =
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      HMul.hMul (α := ℕ) (∏ x ∈ s, HPow.hPow (α := ℕ) 2 (f x)) (∏ x ∈ s, (f x)!)
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      ∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)!

Tactic:
rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, mul_pow
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i)) * HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      ∏ i ∈ s, (f i)! =
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      HMul.hMul (α := ℕ) (∏ x ∈ s, HPow.hPow (α := ℕ) 2 (f x)) (∏ x ∈ s, (f x)!)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
bc : ∀ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)! ≤ (2 * f i)!
⊢ HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      ∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
i : ι
h : i ∈ s
bc : (2 * f i)‼ ≤ (2 * f i)!
⊢ HPow.hPow (α := ℕ) 2 (f i) * (f i)! ≤ (2 * f i)!

Tactic:
rw [← doubleFactorial_two_mul]

Premises used: Nat.doubleFactorial_two_mul
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
i : ι
h : i ∈ s
⊢ (2 * f i)‼ ≤ (2 * f i)!

Tactic:
doubleFactorial_le_factorial _

Premises used: Nat.doubleFactorial_le_factorial
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
i : ι
h : i ∈ s
⊢ (2 * f i)‼ ≤ (2 * f i)!

Tactic:
exact doubleFactorial_le_factorial _

Premises used: Nat.doubleFactorial_le_factorial
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
i :
  (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
i₁ :
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      ∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)!
i₂ :
  HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      ∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ 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 _

Premises used: HMul.hMul, HPow.hPow, Nat.factorial, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ s
rw :
  (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) *
      (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms =
    n.choose (↑m : ℕ) * (↑s : Multiset α).countPerms
⊢ (↑(fill x m s) : Multiset α).countPerms = n.choose (↑m : ℕ) * (↑s : Multiset α).countPerms

Tactic:
rw [Multiset.countPerms_filter_ne x]

Premises used: Multiset.countPerms_filter_ne
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ s
⊢ x ∉ (↑s : Multiset α)

Tactic:
rw [← mem_coe] at hx

Premises used: Sym.mem_coe
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) *
      (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms =
    n.choose (↑m : ℕ) * (↑s : Multiset α).countPerms

Tactic:
congrArg₂ _ ?_ ?_

Premises used: congrArg₂
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_1 : (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) = n.choose (↑m : ℕ)
refine_2 :
  (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms = (↑s : Multiset α).countPerms
⊢ (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) *
      (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms =
    n.choose (↑m : ℕ) * (↑s : Multiset α).countPerms

Tactic:
refine congrArg₂ _ ?_ ?_

Premises used: congrArg₂
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_1 : n.choose (Multiset.count x (↑(fill x m s) : Multiset α)) = n.choose (↑m : ℕ)
refine_1₁ refine_1₂ : n.choose (↑m : ℕ) = n.choose (↑m : ℕ)
⊢ (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) = n.choose (↑m : ℕ)

Tactic:
rw [card_coe, count_coe_fill_self_of_notMem hx]

Premises used: Sym.count_coe_fill_self_of_notMem, Sym.card_coe
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms = (↑s : Multiset α).countPerms

Tactic:
congrArg _ ?_

Premises used: congrArg
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_2 : Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α) = (↑s : Multiset α)
⊢ (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms = (↑s : Multiset α).countPerms

Tactic:
refine congrArg _ ?_

Premises used: congrArg
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_2 :
  Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑s : Multiset α) +
      Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) =
    (↑s : Multiset α)
⊢ Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α) = (↑s : Multiset α)

Tactic:
rw [coe_fill, coe_replicate, Multiset.filter_add]

Premises used: Sym.coe_fill, Multiset.filter_add, Sym.coe_replicate
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_2 :
  (↑s : Multiset α) + Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) = (↑s : Multiset α)
refine_2₁ : ∀ a ∈ (↑s : Multiset α), x ≠ a
⊢ Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑s : Multiset α) +
      Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) =
    (↑s : Multiset α)

Tactic:
rw [Multiset.filter_eq_self.mpr]

Premises used: Iff.mpr, Multiset.filter_eq_self
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_2 : Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) = 0
⊢ (↑s : Multiset α) + Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) = (↑s : Multiset α)

Tactic:
rw [add_eq_left]

Premises used: add_eq_left
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_2 : ∀ a ∈ Multiset.replicate (↑m : ℕ) x, ¬x ≠ a
⊢ Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) = 0

Tactic:
rw [Multiset.filter_eq_nil]

Premises used: Multiset.filter_eq_nil
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
j : α
hj : j ∈ Multiset.replicate (↑m : ℕ) x
⊢ ¬x ≠ j

Tactic:
simp [Multiset.mem_replicate.mp hj]

Premises used: Multiset.mem_replicate, Iff.mp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ ∀ a ∈ Multiset.replicate (↑m : ℕ) x, ¬x ≠ a

Tactic:
exact fun j hj ↦ by simp [Multiset.mem_replicate.mp hj]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
j : α
hj : j ∈ (↑s : Multiset α)
h : x = j
⊢ x ∈ (↑s : Multiset α)

Tactic:
simpa [h] using hj
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ ∀ a ∈ (↑s : Multiset α), x ≠ a

Tactic:
exact fun j hj h ↦ hx <| by simpa [h] using hj
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ ∀ i ∈ s, Eq (α := ℕ) (id 0) 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ ∀ i ∈ s, 0! = 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
rw :
  (∑ i ∈ s, (d : (a : σ) → ℕ) i)! / ∏ i ∈ s, ((d : (a : σ) → ℕ) i)! =
    (∑ x ∈ s, id ((d : (a : σ) → ℕ) x))! / ∏ x ∈ s, ((d : (a : σ) → ℕ) x)!
⊢ Nat.multinomial s (⇑d : (a : σ) → ℕ) = d.multinomial

Tactic:
rw [Nat.multinomial, Finsupp.multinomial,
    sum_of_support_subset _ h _ (by simp), prod_of_support_subset _ h _ (by simp)]

Premises used: Nat.multinomial, Finsupp.multinomial, Finsupp.prod_of_support_subset, Finsupp.sum_of_support_subset
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ (∑ i ∈ s, (d : (a : σ) → ℕ) i)! / ∏ i ∈ s, ((d : (a : σ) → ℕ) i)! =
    (∑ x ∈ s, id ((d : (a : σ) → ℕ) x))! / ∏ x ∈ s, ((d : (a : σ) → ℕ) x)!

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : DecidableEq α
l : List α
⊢ Eq.{u_1 + 1} (α := α) (Finsupp.sum (toFinsupp []) fun (x : ℕ) (a : α) ↦ a) (sum [])

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : DecidableEq α
l_1 : List α
x : α
l : List α
simp :
  ((HAdd.hAdd (α := ℕ →₀ α) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp)).sum
      fun (x : ℕ) (a : α) ↦ a) =
    x + l.sum
⊢ (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) (a : α) ↦ a) = (x :: l).sum

Tactic:
simp only [toFinsupp_cons_eq_single_add_embDomain, sum_cons]

Premises used: List.toFinsupp_cons_eq_single_add_embDomain, List.sum_cons
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : DecidableEq α
l_1 : List α
x : α
l : List α
⊢ ∀ a ∈ Finsupp.support (Finsupp.single 0 x) ∪ Finsupp.support (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp),
    Eq.{u_1 + 1} (α := α) 0 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : DecidableEq α
l_1 : List α
x : α
l : List α
⊢ ∀ a ∈ Finsupp.support (Finsupp.single 0 x) ∪ Finsupp.support (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp),
    ∀ (b₁ b₂ : α), b₁ + b₂ = b₁ + b₂

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : DecidableEq α
l_1 : List α
x : α
l : List α
rw :
  HAdd.hAdd (α := α) (Finsupp.sum (Finsupp.single 0 x) fun (x : ℕ) (a : α) ↦ a)
      (Finsupp.sum (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp) fun (x : ℕ) (a : α) ↦ a) =
    x + l.sum
⊢ ((HAdd.hAdd (α := ℕ →₀ α) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp)).sum
      fun (x : ℕ) (a : α) ↦ a) =
    x + l.sum

Tactic:
rw [Finsupp.sum_add_index (by simp) (by simp)]

Premises used: Finsupp.sum_add_index
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : DecidableEq α
l_1 : List α
x : α
l : List α
⊢ HAdd.hAdd (α := α) (Finsupp.sum (Finsupp.single 0 x) fun (x : ℕ) (a : α) ↦ a)
      (Finsupp.sum (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp) fun (x : ℕ) (a : α) ↦ a) =
    x + l.sum

Tactic:
simp [Finsupp.sum_embDomain, l.toFinsupp_sum]

Premises used: Finsupp.sum_embDomain
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : DecidableEq α
l : List α
⊢ (Finsupp.sum l.toFinsupp fun (x : ℕ) (a : α) ↦ a) = l.sum

Tactic:
match l with
  | nil => simp
  | x :: l =>
    simp only [toFinsupp_cons_eq_single_add_embDomain, sum_cons]
    rw [Finsupp.sum_add_index (by simp) (by simp)]
    simp [Finsupp.sum_embDomain, l.toFinsupp_sum]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
rw :
  Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) *
      Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) =
    (x + l.sum).choose x * Finsupp.multinomial l.toFinsupp
⊢ Finsupp.multinomial (x :: l).toFinsupp = (x + l.sum).choose x * Finsupp.multinomial l.toFinsupp

Tactic:
rw [Finsupp.multinomial_update 0 (x :: l).toFinsupp]

Premises used: List.toFinsupp, Finsupp.multinomial_update, List.cons, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
e_a :
  Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) =
    (x + l.sum).choose x
e_a₁ : Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) = Finsupp.multinomial l.toFinsupp
⊢ Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) *
      Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) =
    (x + l.sum).choose x * Finsupp.multinomial l.toFinsupp

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
e_a : (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) = x + l.sum
⊢ Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) =
    (x + l.sum).choose x

Tactic:
congr
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
⊢ (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) = x + l.sum

Tactic:
List.toFinsupp_sum (x :: l)

Premises used: List.sum, List.cons, List.toFinsupp_sum, List.foldr
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
⊢ (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) = x + l.sum

Tactic:
exact List.toFinsupp_sum (x :: l)

Premises used: List.cons, List.toFinsupp_sum