awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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) (∑ 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) ⋯))
have 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) sorry) *
        (↑(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) sorry))
Tactic: simp only [ih (hc.mono (by simp)), sum_mul, mul_sum]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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) ⋯))
have 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) sorry) *
        (↑(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) sorry)
Tactic: refine sum_congr rfl fun i _ ↦ sum_congr rfl fun g _ ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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)
⊢ 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) ⋯)
have rw : (↑(n.choose i) : R) *
    (f a ^ i * HMul.hMul (α := R) (↑(multinomial s g) : R) (s.noncommProd (fun (i : α) ↦ f i ^ g i) sorry)) =
  HMul.hMul (α := R) (↑(n.choose i) : R) (↑(multinomial s g) : R) *
    (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) sorry)
Tactic: rw [← Nat.cast_comm, (Nat.commute_cast (f a ^ i) _).left_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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) ⋯)
⊢ 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) ⋯)
have rw₁ : (↑(n.choose i) : R) * ((↑(multinomial s g) : R) * (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) sorry)) =
  HMul.hMul (α := R) (↑(n.choose i) : R) (↑(multinomial s g) : R) *
    (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) sorry)
Tactic: rw [← Nat.cast_comm, (Nat.commute_cast (f a ^ i) _).left_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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) ⋯)
⊢ 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) ⋯)
have rw₂ : (↑(n.choose i) : R) * ((↑(multinomial s g) : R) * (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) sorry)) =
  (↑(n.choose i) : R) * ((↑(multinomial s g) : R) * (f a ^ i * s.noncommProd (fun (i : α) ↦ f i ^ g i) sorry))
Tactic: rw [← Nat.cast_comm, (Nat.commute_cast (f a ^ i) _).left_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : ℕ
⊢ (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)) ⋯)
have 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)) sorry))
    (∑ 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) sorry))
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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) ⋯))
have 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)) sorry) =
    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) sorry)
Tactic: refine fun p hp ↦ sum_congr rfl fun f hf ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (hypothesis)
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
⊢ 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) ⋯)
have hf₁ : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
Tactic: rw [mem_piAntidiag] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ 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) ⋯)
have 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)) sorry) =
  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) sorry)
Tactic: rw [not_imp_comm.1 (hf.2 _) has, zero_add, hf.1]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ 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) ⋯)
have cons : Eq.{u_2 + 1} (α := R) (↑((p.1 + p.2).choose p.1) : R) (↑(n.choose p.1) : R)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : Eq.{u_2 + 1} (α := R) (↑((p.1 + p.2).choose p.1) : R) (↑(n.choose p.1) : R)
⊢ 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) ⋯)
have cons₁ : Eq.{u_2 + 1} (α := R) (↑(multinomial s (f + fun (i : α) ↦ if i = a then p.1 else 0)) : R) (↑(multinomial s f) : R)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : Eq.{u_2 + 1} (α := R) (↑((p.1 + p.2).choose p.1) : R) (↑(n.choose p.1) : R)
cons₁ :
  Eq.{u_2 + 1} (α := R) (↑(multinomial s (f + fun (i : α) ↦ if i = a then p.1 else 0)) : R) (↑(multinomial s f) : R)
⊢ 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) ⋯)
have cons₂ : Eq.{u_2 + 1} (α := R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ (f i + if i = a then p.1 else 0)) sorry)
  (s.noncommProd (fun (i : α) ↦ f_1 i ^ f i) sorry)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ Eq.{u_2 + 1} (α := R) (↑((p.1 + p.2).choose p.1) : R) (↑(n.choose p.1) : R)
have cons : Eq.{u_2 + 1} (α := R) (↑(n.choose p.1) : R) (↑(n.choose p.1) : R)
Tactic: rw [mem_antidiagonal.1 hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ Eq.{u_2 + 1} (α := R) (↑(multinomial s (f + fun (i : α) ↦ if i = a then p.1 else 0)) : R) (↑(multinomial s f) : R)
have cons : ∀ a_1 ∈ s, HAdd.hAdd (β := (i : α) → ℕ) f (fun (i : α) ↦ if i = a then p.1 else 0) a_1 = f a_1
Tactic: rw [multinomial_congr]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
t : α
ht : t ∈ s
⊢ HAdd.hAdd (β := (i : α) → ℕ) f (fun (i : α) ↦ if i = a then p.1 else 0) t = f t
have cons : ¬t = a
Tactic: rw [Pi.add_apply, if_neg, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ Eq.{u_2 + 1} (α := R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ (f i + if i = a then p.1 else 0)) ⋯)
    (s.noncommProd (fun (i : α) ↦ f_1 i ^ f i) ⋯)
have cons : ∀ (t : α) (ht : t ∈ s), f_1 t ^ (f t + if t = a then p.1 else 0) = f_1 t ^ f t
Tactic: refine noncommProd_congr rfl (fun t ht ↦ ?_) _
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
t : α
ht : t ∈ s
⊢ f_1 t ^ (f t + if t = a then p.1 else 0) = f_1 t ^ f t
have cons : ¬t = a
Tactic: rw [if_neg, add_zero]