[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
⊢ multinomial ∅ f = 1
[PROOFSTEP]
dsimp [multinomial]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
⊢ 1 / 1 = 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
⊢ multinomial {a} f = 1
[PROOFSTEP]
simp [multinomial, Nat.div_self (factorial_pos (f a))]
[GOAL]
α : 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
[PROOFSTEP]
simp only [multinomial, one_mul, factorial]
[GOAL]
α : 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)!)
[PROOFSTEP]
rw [Finset.sum_insert h, Finset.prod_insert h, h₁, add_comm, ← succ_eq_add_one, factorial_succ]
[GOAL]
α : 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)!)
[PROOFSTEP]
simp only [factorial_one, one_mul, Function.comp_apply, factorial, mul_one, ← one_eq_succ_zero]
[GOAL]
α : 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)!)
[PROOFSTEP]
rw [Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ multinomial (insert a s) f = choose (f a + Finset.sum s f) (f a) * multinomial s f
[PROOFSTEP]
rw [choose_eq_factorial_div_factorial (le.intro rfl)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ multinomial (insert a s) f = (f a + Finset.sum s f)! / ((f a)! * (f a + Finset.sum s f - f a)!) * multinomial s f
[PROOFSTEP]
simp only [multinomial, Nat.add_sub_cancel_left, Finset.sum_insert h, Finset.prod_insert h, Function.comp_apply]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ (f a + ∑ i in s, f i)! / ((f a)! * ∏ i in s, (f i)!) =
    (f a + Finset.sum s f)! / ((f a)! * (Finset.sum s f)!) * ((∑ i in s, f i)! / ∏ i in s, (f i)!)
[PROOFSTEP]
rw [div_mul_div_comm ((f a).factorial_mul_factorial_dvd_factorial_add (s.sum f)) (prod_factorial_dvd_factorial_sum _ _),
  mul_comm (f a)! (s.sum f)!, mul_assoc, mul_comm _ (s.sum f)!, Nat.mul_div_mul_left _ _ (factorial_pos _)]
[GOAL]
α : Type u_1
s : Finset α
f✝ : α → ℕ
a b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
⊢ multinomial s f = multinomial s g
[PROOFSTEP]
simp only [multinomial]
[GOAL]
α : Type u_1
s : Finset α
f✝ : α → ℕ
a b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
⊢ (∑ i in s, f i)! / ∏ i in s, (f i)! = (∑ i in s, g i)! / ∏ i in s, (g i)!
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u_1
s : Finset α
f✝ : α → ℕ
a b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
⊢ (∑ i in s, f i)! = (∑ i in s, g i)!
[PROOFSTEP]
rw [Finset.sum_congr rfl h]
[GOAL]
case e_a
α : Type u_1
s : Finset α
f✝ : α → ℕ
a b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
⊢ ∏ i in s, (f i)! = ∏ i in s, (g i)!
[PROOFSTEP]
exact Finset.prod_congr rfl fun a ha => by rw [h a ha]
[GOAL]
α : Type u_1
s : Finset α
f✝ : α → ℕ
a✝ b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
a : α
ha : a ∈ s
⊢ (f a)! = (g a)!
[PROOFSTEP]
rw [h a ha]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} f = (f a + f b)! / ((f a)! * (f b)!)
[PROOFSTEP]
simp [multinomial, Finset.sum_pair h, Finset.prod_pair h]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} f = choose (f a + f b) (f a)
[PROOFSTEP]
simp [binomial_eq _ h, choose_eq_factorial_div_factorial (Nat.le_add_right _ _)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
hab : a ≠ b
⊢ (f a)! * (f b)! * multinomial {a, b} f = (f a + f b)!
[PROOFSTEP]
simpa [Finset.sum_pair hab, Finset.prod_pair hab] using multinomial_spec { a, b } f
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
h₁ : f a = 1
⊢ multinomial {a, b} f = succ (f b)
[PROOFSTEP]
simp [multinomial_insert_one { b } f (Finset.not_mem_singleton.mpr h) h₁]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} (Function.update (Function.update f a (succ (f a))) b (succ (f b))) =
    multinomial {a, b} (Function.update f a (succ (f a))) + multinomial {a, b} (Function.update f b (succ (f b)))
[PROOFSTEP]
simp only [binomial_eq_choose, Function.update_apply, h, Ne.def, ite_true, ite_false]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (succ (f a) + succ (f b)) (succ (f a)) =
    choose (succ (f a) + if b = a then succ (f a) else f b) (succ (f a)) + choose (f a + succ (f b)) (f a)
[PROOFSTEP]
rw [if_neg h.symm]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (succ (f a) + succ (f b)) (succ (f a)) =
    choose (succ (f a) + f b) (succ (f a)) + choose (f a + succ (f b)) (f a)
[PROOFSTEP]
rw [add_succ, choose_succ_succ, succ_add_eq_succ_add]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (f a + succ (f b)) (f a) + choose (f a + succ (f b)) (succ (f a)) =
    choose (f a + succ (f b)) (succ (f a)) + choose (f a + succ (f b)) (f a)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ succ (f a + f b) * multinomial {a, b} f = succ (f a) * multinomial {a, b} (Function.update f a (succ (f a)))
[PROOFSTEP]
rw [binomial_eq_choose _ h, binomial_eq_choose _ h, mul_comm (f a).succ, Function.update_same,
  Function.update_noteq (ne_comm.mp h)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ succ (f a + f b) * choose (f a + f b) (f a) = choose (succ (f a) + f b) (succ (f a)) * succ (f a)
[PROOFSTEP]
rw [succ_mul_choose_eq (f a + f b) (f a), succ_add (f a) (f b)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a✝ b✝ : α
n a b : ℕ
⊢ multinomial Finset.univ ![a, b] = (a + b)! / (a ! * b !)
[PROOFSTEP]
rw [multinomial, Fin.sum_univ_two, Fin.prod_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a✝ b✝ : α
n a b c : ℕ
⊢ multinomial Finset.univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)
[PROOFSTEP]
rw [multinomial, Fin.sum_univ_three, Fin.prod_univ_three]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a✝ b✝ : α
n a b c : ℕ
⊢ (Matrix.vecCons a ![b, c] 0 + Matrix.vecCons a ![b, c] 1 + Matrix.vecCons a ![b, c] 2)! /
      ((Matrix.vecCons a ![b, c] 0)! * (Matrix.vecCons a ![b, c] 1)! * (Matrix.vecCons a ![b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
a : α
f : α →₀ ℕ
⊢ multinomial f = choose (sum f fun x => id) (↑f a) * multinomial (update f a 0)
[PROOFSTEP]
simp only [multinomial_eq]
[GOAL]
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
classical
by_cases a ∈ f.support
· rw [← Finset.insert_erase h, Nat.multinomial_insert _ f (Finset.not_mem_erase a _), Finset.add_sum_erase _ f h,
    support_update_zero]
  congr 1
  exact Nat.multinomial_congr _ fun _ h => (Function.update_noteq (Finset.mem_erase.1 h).1 0 f).symm
rw [not_mem_support_iff] at h 
rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
[GOAL]
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
by_cases a ∈ f.support
[GOAL]
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
by_cases a ∈ f.support
[GOAL]
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
rw [← Finset.insert_erase h, Nat.multinomial_insert _ f (Finset.not_mem_erase a _), Finset.add_sum_erase _ f h,
  support_update_zero]
[GOAL]
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ choose (∑ x in f.support, ↑f x) (↑f a) * Nat.multinomial (Finset.erase f.support a) ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (Finset.erase f.support a) ↑(update f a 0)
[PROOFSTEP]
congr 1
[GOAL]
case pos.e_a
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial (Finset.erase f.support a) ↑f = Nat.multinomial (Finset.erase f.support a) ↑(update f a 0)
[PROOFSTEP]
exact Nat.multinomial_congr _ fun _ h => (Function.update_noteq (Finset.mem_erase.1 h).1 0 f).symm
[GOAL]
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : ¬a ∈ f.support
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
rw [not_mem_support_iff] at h 
[GOAL]
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : ↑f a = 0
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ multinomial m = Nat.choose (↑card m) (count a m) * multinomial (filter ((fun x x_1 => x ≠ x_1) a) m)
[PROOFSTEP]
dsimp only [multinomial]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ Finsupp.multinomial (↑toFinsupp m) =
    Nat.choose (↑card m) (count a m) * Finsupp.multinomial (↑toFinsupp (filter (fun x => a ≠ x) m))
[PROOFSTEP]
convert Finsupp.multinomial_update a _
[GOAL]
case h.e'_3.h.e'_5.h.e'_1
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ ↑card m = Finsupp.sum (↑toFinsupp m) fun x => id
[PROOFSTEP]
rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]
[GOAL]
case h.e'_3.h.e'_6.h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ ↑toFinsupp (filter (fun x => a ≠ x) m) = Finsupp.update (↑toFinsupp m) a 0
[PROOFSTEP]
ext1 a
[GOAL]
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ ↑(↑toFinsupp (filter (fun x => a✝ ≠ x) m)) a = ↑(Finsupp.update (↑toFinsupp m) a✝ 0) a
[PROOFSTEP]
rw [toFinsupp_apply, count_filter, Finsupp.coe_update]
[GOAL]
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (if a✝ ≠ a then count a m else 0) = Function.update (↑(↑toFinsupp m)) a✝ 0 a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : a✝ ≠ a
⊢ count a m = Function.update (↑(↑toFinsupp m)) a✝ 0 a
[PROOFSTEP]
rw [Function.update_noteq h.symm, toFinsupp_apply]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = Function.update (↑(↑toFinsupp m)) a✝ 0 a
[PROOFSTEP]
rw [not_ne_iff.1 h, Function.update_same]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
⊢ ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
induction' s using Finset.induction with a s ha ih
[GOAL]
case empty
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
⊢ ∀ (n : ℕ),
    Finset.sum ∅ x ^ n =
      ∑ k : { x // x ∈ Finset.sym ∅ n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rw [sum_empty]
[GOAL]
case empty
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
⊢ ∀ (n : ℕ),
    0 ^ n =
      ∑ k : { x // x ∈ Finset.sym ∅ n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rintro
  (_ | n)
      -- Porting note : Lean cannot infer this instance by itself
[GOAL]
case empty.zero
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
⊢ 0 ^ zero =
    ∑ k : { x // x ∈ Finset.sym ∅ zero },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
haveI : Subsingleton (Sym α 0) := Unique.instSubsingleton
[GOAL]
case empty.zero
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ 0 ^ zero =
    ∑ k : { x // x ∈ Finset.sym ∅ zero },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rw [_root_.pow_zero, Fintype.sum_subsingleton]
[GOAL]
case empty.zero
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ 1 =
    ↑(Multiset.multinomial ↑↑?empty.zero.a) *
      Multiset.noncommProd (Multiset.map x ↑↑?empty.zero.a)
        (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑?empty.zero.a} Commute)
case empty.zero.a
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ { x // x ∈ Finset.sym ∅ zero }
[PROOFSTEP]
swap
  -- Porting note : Lean cannot infer this instance by itself
[GOAL]
case empty.zero.a
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ { x // x ∈ Finset.sym ∅ zero }
[PROOFSTEP]
have : Zero (Sym α 0) := Sym.instZeroSym
[GOAL]
case empty.zero.a
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this✝ : Subsingleton (Sym α 0)
this : Zero (Sym α 0)
⊢ { x // x ∈ Finset.sym ∅ zero }
[PROOFSTEP]
exact ⟨0, by simp⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this✝ : Subsingleton (Sym α 0)
this : Zero (Sym α 0)
⊢ 0 ∈ Finset.sym ∅ zero
[PROOFSTEP]
simp
[GOAL]
case empty.zero
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ 1 =
    ↑(Multiset.multinomial
          ↑↑(let_fun this_1 := Sym.instZeroSym;
              { val := 0, property := (_ : 0 ∈ {∅}) })) *
      Multiset.noncommProd
        (Multiset.map x
          ↑↑(let_fun this_1 := Sym.instZeroSym;
              { val := 0, property := (_ : 0 ∈ {∅}) }))
        (_ :
          Set.Pairwise
            {b |
              b ∈
                Multiset.map x
                  ↑↑(let_fun this_1 := Sym.instZeroSym;
                      { val := 0, property := (_ : 0 ∈ {∅}) })}
            Commute)
[PROOFSTEP]
convert (@one_mul R _ _).symm
[GOAL]
case h.e'_3.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ ↑(Multiset.multinomial
        ↑↑(let_fun this_1 := Sym.instZeroSym;
            { val := 0, property := (_ : 0 ∈ {∅}) })) =
    1
[PROOFSTEP]
dsimp only
[GOAL]
case h.e'_3.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ ↑(Multiset.multinomial ↑0) = 1
[PROOFSTEP]
convert @Nat.cast_one R _
[GOAL]
case empty.succ
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
n : ℕ
⊢ 0 ^ succ n =
    ∑ k : { x // x ∈ Finset.sym ∅ (succ n) },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rw [_root_.pow_succ, zero_mul]
  -- Porting note : Lean cannot infer this instance by itself
[GOAL]
case empty.succ
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
n : ℕ
⊢ 0 =
    ∑ k : { x // x ∈ Finset.sym ∅ (succ n) },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
haveI : IsEmpty (Finset.sym (∅ : Finset α) (succ n)) := Finset.instIsEmpty
[GOAL]
case empty.succ
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
n : ℕ
this : IsEmpty { x // x ∈ Finset.sym ∅ (succ n) }
⊢ 0 =
    ∑ k : { x // x ∈ Finset.sym ∅ (succ n) },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
apply (Fintype.sum_empty _).symm
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
ih :
  ∀ (hc : Set.Pairwise ↑s fun i j => Commute (x i) (x j)) (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
⊢ ∀ (n : ℕ),
    Finset.sum (insert a s) x ^ n =
      ∑ k : { x // x ∈ Finset.sym (insert a s) n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
intro n
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
ih :
  ∀ (hc : Set.Pairwise ↑s fun i j => Commute (x i) (x j)) (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
⊢ Finset.sum (insert a s) x ^ n =
    ∑ k : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
specialize ih (hc.mono <| s.subset_insert a)
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ Finset.sum (insert a s) x ^ n =
    ∑ k : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rw [sum_insert ha, (Commute.sum_right s _ _ _).add_pow, sum_range]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∑ i : Fin (n + 1), x a ^ ↑i * (∑ i in s, x i) ^ (n - ↑i) * ↑(Nat.choose n ↑i) =
    ∑ k : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∀ (i : α), i ∈ s → Commute (x a) (x i)
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∀ (i : α), i ∈ s → Commute (x a) (x i)
[PROOFSTEP]
exact fun _ hb => hc (mem_insert_self a s) (mem_insert_of_mem hb) (ne_of_mem_of_not_mem hb ha).symm
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∑ i : Fin (n + 1), x a ^ ↑i * (∑ i in s, x i) ^ (n - ↑i) * ↑(Nat.choose n ↑i) =
    ∑ k : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
simp_rw [ih, mul_sum, sum_mul, sum_sigma', univ_sigma_univ]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∑ x_1 : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) },
      x a ^ ↑x_1.fst *
          (↑(Multiset.multinomial ↑↑x_1.snd) *
            Multiset.noncommProd (Multiset.map x ↑↑x_1.snd)
              (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑x_1.snd} Commute)) *
        ↑(Nat.choose n ↑x_1.fst) =
    ∑ x_1 : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑x_1) *
        Multiset.noncommProd (Multiset.map x ↑↑x_1) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑x_1} Commute)
[PROOFSTEP]
refine' (Fintype.sum_equiv (symInsertEquiv ha) _ _ fun m => _).symm
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Multiset.multinomial ↑↑m) *
      Multiset.noncommProd (Multiset.map x ↑↑m) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑m} Commute) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
rw [m.1.1.multinomial_filter_ne a]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Nat.choose (↑Multiset.card ↑↑m) (Multiset.count a ↑↑m) *
          Multiset.multinomial (Multiset.filter ((fun x x_1 => x ≠ x_1) a) ↑↑m)) *
      Multiset.noncommProd (Multiset.map x ↑↑m) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑m} Commute) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
conv in m.1.1.map _ => rw [← m.1.1.filter_add_not ((· = ·) a), Multiset.map_add]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
| Multiset.map x ↑↑m
[PROOFSTEP]
rw [← m.1.1.filter_add_not ((· = ·) a), Multiset.map_add]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
| Multiset.map x ↑↑m
[PROOFSTEP]
rw [← m.1.1.filter_add_not ((· = ·) a), Multiset.map_add]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
| Multiset.map x ↑↑m
[PROOFSTEP]
rw [← m.1.1.filter_add_not ((· = ·) a), Multiset.map_add]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Nat.choose (↑Multiset.card ↑↑m) (Multiset.count a ↑↑m) *
          Multiset.multinomial (Multiset.filter ((fun x x_1 => x ≠ x_1) a) ↑↑m)) *
      Multiset.noncommProd
        (Multiset.map x (Multiset.filter ((fun x x_1 => x = x_1) a) ↑↑m) +
          Multiset.map x (Multiset.filter (fun a_1 => ¬(fun x x_1 => x = x_1) a a_1) ↑↑m))
        (_ :
          Set.Pairwise
            {x_1 |
              x_1 ∈
                Multiset.map x (Multiset.filter ((fun x x_2 => x = x_2) a) ↑↑m) +
                  Multiset.map x (Multiset.filter (fun a_1 => ¬(fun x x_2 => x = x_2) a a_1) ↑↑m)}
            Commute) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
simp_rw [Multiset.noncommProd_add, m.1.1.filter_eq, Multiset.map_replicate, m.1.2]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Nat.choose n (Multiset.count a ↑↑m) * Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
      (Multiset.noncommProd (Multiset.replicate (Multiset.count a ↑↑m) (x a))
          (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.replicate (Multiset.count a ↑↑m) (x a)} Commute) *
        Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
          (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute)) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
rw [Multiset.noncommProd_eq_pow_card _ _ _ fun _ => Multiset.eq_of_mem_replicate]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Nat.choose n (Multiset.count a ↑↑m) * Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
      (x a ^ ↑Multiset.card (Multiset.replicate (Multiset.count a ↑↑m) (x a)) *
        Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
          (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute)) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
rw [Multiset.card_replicate, Nat.cast_mul, mul_assoc, Nat.cast_comm]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
        (x a ^ Multiset.count a ↑↑m *
          Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
            (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute)) *
      ↑(Nat.choose n (Multiset.count a ↑↑m)) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
congr 1
[GOAL]
case insert.e_a
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
      (x a ^ Multiset.count a ↑↑m *
        Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
          (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute)) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
      (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
        Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
          (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute))
[PROOFSTEP]
simp_rw [← mul_assoc, Nat.cast_comm]
[GOAL]
case insert.e_a
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ x a ^ Multiset.count a ↑↑m * ↑(Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
      Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
        (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst * ↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
      Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
        (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
⊢ Finset.sum s x ^ n = ∑ k in Finset.sym s n, ↑(Multiset.multinomial ↑k) * Multiset.prod (Multiset.map x ↑k)
[PROOFSTEP]
conv_rhs => rw [← sum_coe_sort]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
| ∑ k in Finset.sym s n, ↑(Multiset.multinomial ↑k) * Multiset.prod (Multiset.map x ↑k)
[PROOFSTEP]
rw [← sum_coe_sort]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
| ∑ k in Finset.sym s n, ↑(Multiset.multinomial ↑k) * Multiset.prod (Multiset.map x ↑k)
[PROOFSTEP]
rw [← sum_coe_sort]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
| ∑ k in Finset.sym s n, ↑(Multiset.multinomial ↑k) * Multiset.prod (Multiset.map x ↑k)
[PROOFSTEP]
rw [← sum_coe_sort]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
⊢ Finset.sum s x ^ n =
    ∑ i : { x // x ∈ Finset.sym s n }, ↑(Multiset.multinomial ↑↑i) * Multiset.prod (Multiset.map x ↑↑i)
[PROOFSTEP]
convert sum_pow_of_commute s x (fun _ _ _ _ _ => mul_comm _ _) n
[GOAL]
case h.e'_3.a.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
x✝ : { x // x ∈ Finset.sym s n }
a✝ : x✝ ∈ univ
⊢ Multiset.prod (Multiset.map x ↑↑x✝) =
    Multiset.noncommProd (Multiset.map x ↑↑x✝) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑x✝} Commute)
[PROOFSTEP]
rw [Multiset.noncommProd_eq_prod]
