-- Mathlib/Data/Nat/Choose/Multinomial.lean
/-- The **multinomial theorem**. -/
lemma sum_pow_eq_sum_piAntidiag_of_commute (s : Finset α) (f : α → R)
    (hc : (s : Set α).Pairwise (Commute on f)) (n : ℕ) :
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ piAntidiag s n, multinomial s k *
      s.noncommProd (fun i ↦ f i ^ k i) (hc.mono' fun _ _ h ↦ h.pow_pow ..)

Proof state:
case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i => f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
⊢ (∑ i ∈ cons a s has, f i) ^ n =
    ∑ k ∈ (cons a s has).piAntidiag n,
      ↑(multinomial (cons a s has) k) * (cons a s has).noncommProd (fun i => f i ^ k i) ⋯

Tactic:
rw [Finset.sum_cons, piAntidiag_cons, sum_disjiUnion]

Result:
case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i => f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
⊢ (f a + ∑ x ∈ s, f x) ^ n =
    ∑ i ∈ antidiagonal n,
      ∑ x ∈ map (addRightEmbedding fun t => if t = a then i.1 else 0) (s.piAntidiag i.2),
        ↑(multinomial (cons a s has) x) * (cons a s has).noncommProd (fun i => f i ^ x i) ⋯

Proof state:
case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i => f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
⊢ (f a + ∑ x ∈ s, f x) ^ n =
    ∑ x ∈ antidiagonal n,
      ∑ x_1 ∈ s.piAntidiag x.2,
        ↑((x_1 a + x.1 + ∑ x ∈ s, x_1 x).choose (x_1 a + x.1)) *
            ↑(multinomial s (x_1 + fun t => if t = a then x.1 else 0)) *
          (f a ^ (x_1 a + x.1) * s.noncommProd (fun x_2 => f x_2 ^ (x_1 x_2 + if x_2 = a then x.1 else 0)) ⋯)

Tactic:
suffices ∀ p : ℕ × ℕ, p ∈ antidiagonal n →
  ∑ g ∈ piAntidiag s p.2, ((g a + p.1 + s.sum g).choose (g a + p.1) : R) *
    multinomial s (g + fun i ↦ ite (i = a) p.1 0) *
      (f a ^ (g a + p.1) * s.noncommProd (fun i ↦ f i ^ (g i + ite (i = a) p.1 0))
        ((hc.mono (by simp)).mono' fun i j h ↦ h.pow_pow ..)) =
    ∑ g ∈ piAntidiag s p.2, n.choose p.1 * multinomial s g * (f a ^ p.1 *
      s.noncommProd (fun i ↦ f i ^ g i) ((hc.mono (by simp)).mono' fun i j h ↦ h.pow_pow ..)) by
  rw [sum_congr rfl this]
  simp only [Nat.antidiagonal_eq_map, sum_map, Function.Embedding.coeFn_mk]
  rw [(Commute.sum_right _ _ _ fun i hi ↦ hc (by simp) (by simp [hi])
    (by simpa [eq_comm] using ne_of_mem_of_not_mem hi has)).add_pow]
  simp only [ih (hc.mono (by simp)), sum_mul, mul_sum]
  refine sum_congr rfl fun i _ ↦ sum_congr rfl fun g _ ↦ ?_
  rw [← Nat.cast_comm, (Nat.commute_cast (f a ^ i) _).left_comm, mul_assoc]

Result:
case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i => f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
⊢ ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i => if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i => f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i => f i ^ g i) ⋯)

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i => f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i => if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i => f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i => f i ^ g i) ⋯)
⊢ ∑ m ∈ range (n + 1), f a ^ m * (∑ i ∈ s, f i) ^ (n - m) * ↑(n.choose m) =
    ∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        ↑(n.choose x) * ↑(multinomial s x_1) * (f a ^ x * s.noncommProd (fun i => f i ^ x_1 i) ⋯)

Tactic:
simp only [ih (hc.mono (by simp)), sum_mul, mul_sum]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i => f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i => if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i => f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i => f i ^ g i) ⋯)
⊢ ∑ x ∈ range (n + 1),
      ∑ i ∈ s.piAntidiag (n - x),
        f a ^ x * (↑(multinomial s i) * s.noncommProd (fun i_1 => f i_1 ^ i i_1) ⋯) * ↑(n.choose x) =
    ∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        ↑(n.choose x) * ↑(multinomial s x_1) * (f a ^ x * s.noncommProd (fun i => f i ^ x_1 i) ⋯)

Proof state:
case empty
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
hc : (↑∅).Pairwise (Commute on f)
n : ℕ
⊢ (∑ i ∈ ∅, f i) ^ n = ∑ k ∈ ∅.piAntidiag n, ↑(multinomial ∅ k) * ∅.noncommProd (fun i => f i ^ k i) ⋯

Tactic:
cases n <;> simp

Result:
no goals

Proof state:
case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i => f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑((f a + p.1 + s.sum f).choose (f a + p.1)) * ↑(multinomial s (f + fun i => if i = a then p.1 else 0)) *
      (f✝ a ^ (f a + p.1) * s.noncommProd (fun i => f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    ↑(n.choose p.1) * ↑(multinomial s f) * (f✝ a ^ p.1 * s.noncommProd (fun i => f✝ i ^ f i) ⋯)

Tactic:
rw [not_imp_comm.1 (hf.2 _) has, zero_add, hf.1]

Result:
case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i => f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑((p.1 + p.2).choose p.1) * ↑(multinomial s (f + fun i => if i = a then p.1 else 0)) *
      (f✝ a ^ p.1 * s.noncommProd (fun i => f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    ↑(n.choose p.1) * ↑(multinomial s f) * (f✝ a ^ p.1 * s.noncommProd (fun i => f✝ i ^ f i) ⋯)