-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem sum_pow_of_commute (x : α → R) (s : Finset α)
    (hc : (s : Set α).Pairwise (Commute on x)) :
    ∀ n,
      s.sum x ^ n =
        ∑ k : s.sym n,
          k.1.1.multinomial *
            (k.1.1.map <| x).noncommProd
              (Multiset.map_set_pairwise <| hc.mono <| mem_sym_iff.1 k.2)

Proof state:
case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
this : Subsingleton (Sym α 0)
⊢ 1 =
    ↑(↑↑(let_fun this_1 := Sym.instZeroSym;
              ⟨0, ⋯⟩)).multinomial *
      (Multiset.map x
            ↑↑(let_fun this_1 := Sym.instZeroSym;
                ⟨0, ⋯⟩)).noncommProd
        ⋯

Tactic:
convert (@one_mul R _ _).symm

Result:
case h.e'_3.h.e'_5
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
this : Subsingleton (Sym α 0)
⊢ ↑(↑↑(let_fun this_1 := Sym.instZeroSym;
            ⟨0, ⋯⟩)).multinomial =
    1

Proof state:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
n : ℕ
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
m : { x // x ∈ (insert a s).sym n }
⊢ ↑(n.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x => a ≠ x) ↑↑m).multinomial) *
      (x a ^ (Multiset.replicate (Multiset.count a ↑↑m) (x a)).card *
        (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)).noncommProd ⋯) =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).multinomial * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)

Tactic:
rw [Multiset.card_replicate, Nat.cast_mul, mul_assoc, Nat.cast_comm]

Result:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
n : ℕ
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
m : { x // x ∈ (insert a s).sym n }
⊢ ↑(Multiset.filter (fun x => a ≠ x) ↑↑m).multinomial *
        (x a ^ Multiset.count a ↑↑m * (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)).noncommProd ⋯) *
      ↑(n.choose (Multiset.count a ↑↑m)) =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).multinomial * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)

Proof state:
case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
⊢ 0 = ∑ k : { x // x ∈ ∅.sym (n + 1) }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
haveI : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty

Result:
case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
this : IsEmpty { x // x ∈ ∅.sym n.succ }
⊢ 0 = ∑ k : { x // x ∈ ∅.sym (n + 1) }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯

Proof state:
case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
this : Subsingleton (Sym α 0)
⊢ 1 = ↑(↑↑?empty.zero.a).multinomial * (Multiset.map x ↑↑?empty.zero.a).noncommProd ⋯

case empty.zero.a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
this : Subsingleton (Sym α 0)
⊢ { x // x ∈ ∅.sym 0 }

Tactic:
swap

Result:
case empty.zero.a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
this : Subsingleton (Sym α 0)
⊢ { x // x ∈ ∅.sym 0 }

case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
this : Subsingleton (Sym α 0)
⊢ 1 = ↑(↑↑?empty.zero.a).multinomial * (Multiset.map x ↑↑?empty.zero.a).noncommProd ⋯

Proof state:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
n : ℕ
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
⊢ ∑ i : Fin (n + 1), x a ^ ↑i * (∑ i ∈ s, x i) ^ (n - ↑i) * ↑(n.choose ↑i) =
    ∑ k : { x // x ∈ (insert a s).sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
simp_rw [ih, mul_sum, sum_mul, sum_sigma', univ_sigma_univ]

Result:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
n : ℕ
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
⊢ ∑ x_1 : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) },
      x a ^ ↑x_1.fst * (↑(↑↑x_1.snd).multinomial * (Multiset.map x ↑↑x_1.snd).noncommProd ⋯) * ↑(n.choose ↑x_1.fst) =
    ∑ k : { x // x ∈ (insert a s).sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯

Proof state:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
n : ℕ
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
m : { x // x ∈ (insert a s).sym n }
⊢ ↑((↑↑m).card.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x => a ≠ x) ↑↑m).multinomial) *
      (Multiset.map x (Multiset.filter (fun x => a = x) ↑↑m) +
            Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)).noncommProd
        ⋯ =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).multinomial * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)

Tactic:
simp_rw [Multiset.noncommProd_add, m.1.1.filter_eq, Multiset.map_replicate, m.1.2]

Result:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
n : ℕ
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
m : { x // x ∈ (insert a s).sym n }
⊢ ↑(n.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x => a ≠ x) ↑↑m).multinomial) *
      ((Multiset.replicate (Multiset.count a ↑↑m) (x a)).noncommProd ⋯ *
        (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)).noncommProd ⋯) =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).multinomial * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)