-- 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:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
s : Finset α
hc : (↑s).Pairwise (Commute on x)
⊢ ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
induction' s using Finset.induction with a s ha ih

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

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

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

Tactic:
rw [sum_empty]

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

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) *
      ((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)

Tactic:
rw [Multiset.noncommProd_eq_pow_card _ _ _ fun _ => Multiset.eq_of_mem_replicate]

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) *
      (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)

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

Tactic:
haveI : Subsingleton (Sym α 0) := Unique.instSubsingleton

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

Proof state:
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)
this : Zero (Sym α 0)
⊢ { x // x ∈ ∅.sym 0 }

Tactic:
exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩

Result:
no goals

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

Tactic:
intro n

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

Proof state:
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:
have : Zero (Sym α 0) := Sym.instZeroSym

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)
this : Zero (Sym α 0)
⊢ { x // x ∈ ∅.sym 0 }

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 }
⊢ ↑(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)

Tactic:
congr 1

Result:
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 }
⊢ ↑(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 ⋯) =
    x a ^ ↑((symInsertEquiv ha) m).fst *
      (↑(↑↑((symInsertEquiv ha) m).snd).multinomial * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯)

Proof state:
α : 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 ∈ s, Commute (x a) (x i)

Tactic:
exact fun _ hb => hc (mem_insert_self a s) (mem_insert_of_mem hb)
  (ne_of_mem_of_not_mem hb ha).symm

Result:
no goals