awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
rw :
  (f a + ∑ x ∈ s, f x) ^ n =
    ∑ x ∈ @antidiagonal _ instAddMonoid _ n,
      ∑ g ∈ s.piAntidiag x.2,
        HMul.hMul (α := R) (↑(n.choose x.1) : R) (↑(multinomial s g) : R) *
          (f a ^ x.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯)
⊢ (f a + ∑ x ∈ s, f x) ^ n =
    ∑ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∑ x_1 ∈ s.piAntidiag x.2,
        HMul.hMul (α := R) (↑((x_1 a + x.1 + ∑ x ∈ s, x_1 x).choose (x_1 a + x.1)) : R)
            (↑(multinomial s (x_1 + fun (t : α) ↦ if t = a then x.1 else 0)) : R) *
          (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]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
simp :
  (f a + ∑ x ∈ s, f x) ^ n =
    ∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        HMul.hMul (α := R) (↑(n.choose x) : R) (↑(multinomial s x_1) : R) *
          (f a ^ x * s.noncommProd (fun (i : α) ↦ f i ^ x_1 i) ⋯)
⊢ (f a + ∑ x ∈ s, f x) ^ n =
    ∑ x ∈ @antidiagonal _ instAddMonoid _ n,
      ∑ g ∈ s.piAntidiag x.2,
        HMul.hMul (α := R) (↑(n.choose x.1) : R) (↑(multinomial s g) : R) *
          (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]

Premises used: Finset.Nat.antidiagonal_eq_map, Finset.sum_map, Function.Embedding.coeFn_mk
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
i : α
hi : i ∈ s
⊢ a ∈ (↑(cons a s has) : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
i : α
hi : i ∈ s
⊢ i ∈ (↑(cons a s has) : Set α)

Tactic:
simp [hi]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (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

Premises used: eq_comm, ne_of_mem_of_not_mem
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
rw :
  Eq.{u_2 + 1} (α := R) (∑ m ∈ range (n + 1), f a ^ m * HPow.hPow (α := R) (∑ i ∈ s, f i) (n - m) * (↑(n.choose m) : R))
    (∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        HMul.hMul (α := R) (↑(n.choose x) : R) (↑(multinomial s x_1) : R) *
          (f a ^ x * s.noncommProd (fun (i : α) ↦ f i ^ x_1 i) ⋯))
⊢ (f a + ∑ x ∈ s, f x) ^ n =
    ∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        HMul.hMul (α := R) (↑(n.choose x) : R) (↑(multinomial s x_1) : R) *
          (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]

Premises used: Commute.add_pow, Commute.sum_right
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
⊢ (↑s : Set α) ⊆ (↑(cons a s has) : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
simp :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ range (n + 1),
      ∑ i ∈ s.piAntidiag (n - x),
        f a ^ x * HMul.hMul (α := R) (↑(multinomial s i) : R) (s.noncommProd (fun (i_1 : α) ↦ f i_1 ^ i i_1) ⋯) *
          (↑(n.choose x) : R))
    (∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        HMul.hMul (α := R) (↑(n.choose x) : R) (↑(multinomial s x_1) : R) *
          (f a ^ x * s.noncommProd (fun (i : α) ↦ f i ^ x_1 i) ⋯))
⊢ Eq.{u_2 + 1} (α := R) (∑ m ∈ range (n + 1), f a ^ m * HPow.hPow (α := R) (∑ i ∈ s, f i) (n - m) * (↑(n.choose m) : R))
    (∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        HMul.hMul (α := R) (↑(n.choose x) : R) (↑(multinomial s x_1) : R) *
          (f a ^ x * s.noncommProd (fun (i : α) ↦ f i ^ x_1 i) ⋯))

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

Premises used: Finset.mul_sum, Set.Pairwise.mono, Finset.sum_mul
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ range (n + 1),
      ∑ i ∈ s.piAntidiag (n - x),
        f a ^ x * HMul.hMul (α := R) (↑(multinomial s i) : R) (s.noncommProd (fun (i_1 : α) ↦ f i_1 ^ i i_1) ⋯) *
          (↑(n.choose x) : R))
    (∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        HMul.hMul (α := R) (↑(n.choose x) : R) (↑(multinomial s x_1) : R) *
          (f a ^ x * s.noncommProd (fun (i : α) ↦ f i ^ x_1 i) ⋯))

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
refine :
  ∀ i ∈ range (n + 1),
    ∀ g ∈ s.piAntidiag (n - i),
      f a ^ i * HMul.hMul (α := R) (↑(multinomial s g) : R) (s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯) *
          (↑(n.choose i) : R) =
        HMul.hMul (α := R) (↑(n.choose i) : R) (↑(multinomial s g) : R) *
          (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ range (n + 1),
      ∑ i ∈ s.piAntidiag (n - x),
        f a ^ x * HMul.hMul (α := R) (↑(multinomial s i) : R) (s.noncommProd (fun (i_1 : α) ↦ f i_1 ^ i i_1) ⋯) *
          (↑(n.choose x) : R))
    (∑ x ∈ range (n + 1),
      ∑ x_1 ∈ s.piAntidiag (n - x),
        HMul.hMul (α := R) (↑(n.choose x) : R) (↑(multinomial s x_1) : R) *
          (f a ^ x * s.noncommProd (fun (i : α) ↦ f i ^ x_1 i) ⋯))

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
i : ℕ
h : i ∈ range (n + 1)
g : α → ℕ
h_1 : g ∈ s.piAntidiag (n - i)
rw :
  (↑(n.choose i) : R) *
      (f a ^ i * HMul.hMul (α := R) (↑(multinomial s g) : R) (s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯)) =
    HMul.hMul (α := R) (↑(n.choose i) : R) (↑(multinomial s g) : R) *
      (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯)
rw₁ :
  (↑(n.choose i) : R) * ((↑(multinomial s g) : R) * (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯)) =
    HMul.hMul (α := R) (↑(n.choose i) : R) (↑(multinomial s g) : R) *
      (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯)
rw₂ rw₃ :
  (↑(n.choose i) : R) * ((↑(multinomial s g) : R) * (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯)) =
    (↑(n.choose i) : R) * ((↑(multinomial s g) : R) * (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
⊢ f a ^ i * HMul.hMul (α := R) (↑(multinomial s g) : R) (s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯) *
      (↑(n.choose i) : R) =
    HMul.hMul (α := R) (↑(n.choose i) : R) (↑(multinomial s g) : R) *
      (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯)

Tactic:
rw [← Nat.cast_comm, (Nat.commute_cast (f a ^ i) _).left_comm, mul_assoc]

Premises used: Nat.cast_comm, Nat.commute_cast, Commute.left_comm, mul_assoc, HPow.hPow
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
cons :
  ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
⊢ (f a + ∑ x ∈ s, f x) ^ n =
    ∑ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∑ x_1 ∈ s.piAntidiag x.2,
        HMul.hMul (α := R) (↑((x_1 a + x.1 + ∑ x ∈ s, x_1 x).choose (x_1 a + x.1)) : R)
            (↑(multinomial s (x_1 + fun (t : α) ↦ if t = a then x.1 else 0)) : R) *
          (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]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
⊢ ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f)
n : ℕ
cons :
  ∀ (p : ℕ × ℕ) (hp : p ∈ @antidiagonal _ instAddMonoid _ n) (f_1 : α → ℕ) (hf : f_1 ∈ s.piAntidiag p.2),
    HMul.hMul (α := R) (↑((f_1 a + p.1 + s.sum f_1).choose (f_1 a + p.1)) : R)
          (↑(multinomial s (f_1 + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
        (f a ^ (f_1 a + p.1) * s.noncommProd (fun (i : α) ↦ f i ^ (f_1 i + if i = a then p.1 else 0)) ⋯) =
      HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s f_1) : R) *
        (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ f_1 i) ⋯)
⊢ ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
    Eq.{u_2 + 1} (α := R)
      (∑ g ∈ s.piAntidiag p.2,
        HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
            (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
          (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,
        HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
          (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : f ∈ s.piAntidiag p.2
⊢ s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s

Tactic:
rw [mem_piAntidiag] at hf

Premises used: Finset.mem_piAntidiag
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
cons :
  HMul.hMul (α := R) (↑((p.1 + p.2).choose p.1) : R)
        (↑(multinomial s (f + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
      (f_1 a ^ p.1 * s.noncommProd (fun (i : α) ↦ f_1 i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s f) : R) *
      (f_1 a ^ p.1 * s.noncommProd (fun (i : α) ↦ f_1 i ^ f i) ⋯)
⊢ HMul.hMul (α := R) (↑((f a + p.1 + s.sum f).choose (f a + p.1)) : R)
        (↑(multinomial s (f + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
      (f_1 a ^ (f a + p.1) * s.noncommProd (fun (i : α) ↦ f_1 i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s f) : R) *
      (f_1 a ^ p.1 * s.noncommProd (fun (i : α) ↦ f_1 i ^ f i) ⋯)

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

Premises used: not_imp_comm, zero_add, And.right, And.left, Iff.mp