-- 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:
α : 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) ⋯)

Tactic:
refine sum_congr rfl fun i _ ↦ sum_congr rfl fun g _ ↦ ?_

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) ⋯)
i : ℕ
x✝¹ : i ∈ range (n + 1)
g : α → ℕ
x✝ : g ∈ s.piAntidiag (n - i)
⊢ f a ^ i * (↑(multinomial s g) * s.noncommProd (fun i => f i ^ g i) ⋯) * ↑(n.choose i) =
    ↑(n.choose i) * ↑(multinomial s g) * (f a ^ i * s.noncommProd (fun i => f i ^ g i) ⋯)

Proof state:
case cons.e_a.e_a
α : 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
⊢ ∀ a_1 ∈ s, (f + fun i => if i = a then p.1 else 0) a_1 = f a_1

Tactic:
intro t ht

Result:
case cons.e_a.e_a
α : 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
t : α
ht : t ∈ s
⊢ (f + fun i => if i = a then p.1 else 0) t = f t

Proof state:
case cons.e_a.e_a.hnc
α : 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
t : α
ht : t ∈ s
⊢ ¬t = a

Tactic:
exact ne_of_mem_of_not_mem ht has

Result:
no goals

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) ⋯)
⊢ (f a + ∑ x ∈ s, f x) ^ n =
    ∑ 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:
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]

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) ⋯)
⊢ ∑ 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) ⋯)

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 : ℕ
p : ℕ × ℕ
g : α → ℕ
⊢ ↑s ⊆ ↑(cons a s has)

Tactic:
simp

Result:
no goals