-- 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 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).multinomial * (Multiset.map x ↑↑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 [m.1.1.multinomial_filter_ne a]

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 }
⊢ ↑((↑↑m).card.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x => a ≠ x) ↑↑m).multinomial) *
      (Multiset.map x ↑↑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)

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

Tactic:
rintro (_ | n)

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

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

Proof state:
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

Tactic:
convert @Nat.cast_one R _

Result:
case h.e'_2.h.e'_3
α : 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 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 ⋯

Tactic:
apply (Fintype.sum_empty _).symm

Result:
no goals

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)
⊢ 0 ^ 0 = ∑ k : { x // x ∈ ∅.sym 0 }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
rw [_root_.pow_zero, Fintype.sum_subsingleton]

Result:
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 }

Proof state:
case insert.e_a
α : 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 }
⊢ x a ^ Multiset.count a ↑↑m * ↑(Multiset.filter (fun x => a ≠ x) ↑↑m).multinomial *
      (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 ⋯

Tactic:
rfl

Result:
no goals