α : Type u_2
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_1
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)
α : Type u_2
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_1
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)
conv_rhs => rw [← sum_coe_sort]
case h.e'_3.a.h.e'_6
α : Type u_2
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_1
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)
α : Type u_2
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_1
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)
convert sum_pow_of_commute s x (fun _ _ _ _ _ => mul_comm _ _) n
no goals
case h.e'_3.a.h.e'_6
α : Type u_2
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_1
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)
rw [Multiset.noncommProd_eq_prod]