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

Tactic:
rw [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:
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
⊢ s.noncommProd (fun i => f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯ = s.noncommProd (fun i => f✝ i ^ f i) ⋯

Tactic:
refine noncommProd_congr rfl (fun 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✝ t ^ (f t + if t = a then p.1 else 0) = f✝ t ^ f t

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 ≠ i

Tactic:
simpa [eq_comm] using ne_of_mem_of_not_mem hi has

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

Tactic:
rw [mem_piAntidiag] at 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 : 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) ⋯)

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

Tactic:
simp only [Nat.antidiagonal_eq_map, sum_map, Function.Embedding.coeFn_mk]

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 ∈ 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 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
⊢ ↑((p.1 + p.2).choose p.1) = ↑(n.choose p.1)

Tactic:
rw [mem_antidiagonal.1 hp]

Result:
no goals