-- 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.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
⊢ ↑(multinomial s (f + fun i => if i = a then p.1 else 0)) = ↑(multinomial s f)

Tactic:
rw [multinomial_congr]

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

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) ⋯)
⊢ ↑s ⊆ ↑(cons a s has)

Tactic:
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 ∈ 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) ⋯)

Tactic:
refine fun p hp ↦ sum_congr rfl fun f hf ↦ ?_

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 : f ∈ s.piAntidiag p.2
⊢ ↑((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) ⋯)

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

Tactic:
rw [Pi.add_apply, if_neg, add_zero]

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

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) ⋯)
i : α
hi : i ∈ s
⊢ a ∈ ↑(cons a s has)

Tactic:
simp

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 ∈ 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:
rw [sum_congr rfl this]

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) ⋯)
⊢ (f a + ∑ x ∈ s, f x) ^ n =
    ∑ x ∈ antidiagonal n,
      ∑ g ∈ s.piAntidiag x.2, ↑(n.choose x.1) * ↑(multinomial s g) * (f a ^ x.1 * s.noncommProd (fun i => f i ^ g i) ⋯)