awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (hypothesis)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∉ f.support
⊢ Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
have h₁ : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ)
Tactic: rw [notMem_support_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ)
⊢ Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
have neg : Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
  Nat.choose (f.sum fun (x : α) ↦ id) 0 * Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
Tactic: rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ)
neg :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) 0 * Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
⊢ Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
have neg₁ : Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
  1 * Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
Tactic: rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ)
neg :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) 0 * Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
neg₁ :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    1 * Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
⊢ Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
have neg₂ : Nat.multinomial f.support (⇑f : (a : α) → ℕ) = Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
Tactic: rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ)
neg :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) 0 * Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
neg₁ :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    1 * Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
neg₂ :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) = Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
⊢ Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
have neg₃ : Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
  Nat.multinomial (f.update a ((f : (a : α) → ℕ) a)).support (⇑(f.update a ((f : (a : α) → ℕ) a)) : (a : α) → ℕ)
Tactic: rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ)
neg :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) 0 * Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
neg₁ :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    1 * Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
neg₂ :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) = Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
neg₃ :
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.multinomial (f.update a ((f : (a : α) → ℕ) a)).support (⇑(f.update a ((f : (a : α) → ℕ) a)) : (a : α) → ℕ)
⊢ Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
have neg₄ : Nat.multinomial f.support (⇑f : (a : α) → ℕ) = Nat.multinomial f.support (⇑f : (a : α) → ℕ)
Tactic: rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
have pos : ∀ (h : a ∈ f.support),
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
Tactic: classical
    by_cases h : a ∈ f.support
    · rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.notMem_erase a _),
        Finset.add_sum_erase _ f h, support_update_zero]
      congr 1
      exact Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm
    rw [notMem_support_iff] at h
    rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
pos :
  ∀ (h : a ∈ f.support),
    Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
      Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
        Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
⊢ Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
have neg : ∀ (h : a ∉ f.support),
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
Tactic: classical
    by_cases h : a ∈ f.support
    · rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.notMem_erase a _),
        Finset.add_sum_erase _ f h, support_update_zero]
      congr 1
      exact Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm
    rw [notMem_support_iff] at h
    rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
pos :
  ∀ (h : a ∈ f.support),
    Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
      Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
        Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
neg neg₁ :
  ∀ (h : a ∉ f.support),
    Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
      Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
        Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
⊢ Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
have neg₂ : ∀ (h : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ)),
  Nat.multinomial f.support (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.update a 0).support (⇑(f.update a 0) : (a : α) → ℕ)
Tactic: classical
    by_cases h : a ∈ f.support
    · rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.notMem_erase a _),
        Finset.add_sum_erase _ f h, support_update_zero]
      congr 1
      exact Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm
    rw [notMem_support_iff] at h
    rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
m : Multiset α
⊢ Finsupp.multinomial.{u_1} (α := α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) =
    m.card.choose (count a m) *
      Finsupp.multinomial.{u_1} (α := α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (filter (fun (x : α) ↦ a ≠ x) m))
have h : m.card = Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) fun (x : α) ↦ id
Tactic: convert! Finsupp.multinomial_update a _
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
m : Multiset α
h : m.card = Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) fun (x : α) ↦ id
⊢ Finsupp.multinomial.{u_1} (α := α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) =
    m.card.choose (count a m) *
      Finsupp.multinomial.{u_1} (α := α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (filter (fun (x : α) ↦ a ≠ x) m))
have h₁ : Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (filter (fun (x : α) ↦ a ≠ x) m) : α →₀ ℕ)
  (Finsupp.update ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) a 0 : α →₀ ℕ)
Tactic: convert! Finsupp.multinomial_update a _
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
m : Multiset α
⊢ m.card = Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) fun (x : α) ↦ id
have h : m.card =
  card.{u_1} (α := α) ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m))
Tactic: rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
m : Multiset α
h :
  m.card =
    card.{u_1} (α := α) ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m))
⊢ m.card = Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) fun (x : α) ↦ id
have h₁ : m.card = m.card
Tactic: rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
m : Multiset α
⊢ Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (filter (fun (x : α) ↦ a ≠ x) m) : α →₀ ℕ)
    (Finsupp.update ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) a 0 : α →₀ ℕ)
have h : ∀ (a_1 : α),
  Eq (α := ℕ)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) (filter (fun (x : α) ↦ a ≠ x) m) : α →₀ ℕ) : (a : α) → ℕ) a_1 : ℕ)
    ((Finsupp.update ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) a 0 : (a : α) → ℕ) a_1 : ℕ)
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a_1 : α
m : Multiset α
a : α
⊢ Eq (α := ℕ)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) (filter (fun (x : α) ↦ a_1 ≠ x) m) : α →₀ ℕ) : (a : α) → ℕ) a : ℕ)
    ((Finsupp.update ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) a_1 0 : (a : α) → ℕ) a : ℕ)
have h : (if a_1 ≠ a then count a m else 0) =
  Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0 a
Tactic: rw [toFinsupp_apply, count_filter, Finsupp.coe_update]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a_1 : α
m : Multiset α
a : α
⊢ (if a_1 ≠ a then count a m else 0) =
    Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0 a
have pos : ∀ (h : a_1 ≠ a),
  count a m =
    Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0 a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a_1 : α
m : Multiset α
a : α
pos :
  ∀ (h : a_1 ≠ a),
    count a m =
      Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0
        a
⊢ (if a_1 ≠ a then count a m else 0) =
    Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0 a
have neg : ∀ (h : ¬a_1 ≠ a),
  Eq (α := ℕ) (0 : ℕ)
    (Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0
        a :
      ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a_1 : α
m : Multiset α
a : α
h : a_1 ≠ a
⊢ count a m =
    Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0 a
have pos : count a m = (((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a
Tactic: rw [Function.update_of_ne h.symm, toFinsupp_apply]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a_1 : α
m : Multiset α
a : α
h : a_1 ≠ a
pos : count a m = (((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a
⊢ count a m =
    Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0 a
have pos₁ : count a m = count a m
Tactic: rw [Function.update_of_ne h.symm, toFinsupp_apply]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a_1 : α
m : Multiset α
a : α
h : ¬a_1 ≠ a
⊢ Eq (α := ℕ) (0 : ℕ)
    (Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0
        a :
      ℕ)
have neg : Eq (α := ℕ) (0 : ℕ)
  (Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a 0 a :
    ℕ)
Tactic: rw [not_ne_iff.1 h, Function.update_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a_1 : α
m : Multiset α
a : α
h : ¬a_1 ≠ a
neg :
  Eq (α := ℕ) (0 : ℕ)
    (Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a 0
        a :
      ℕ)
⊢ Eq (α := ℕ) (0 : ℕ)
    (Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0
        a :
      ℕ)
have neg₁ : Eq (α := ℕ) 0 0
Tactic: rw [not_ne_iff.1 h, Function.update_self]
-- 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
hc : (↑∅ : Set α).Pairwise (Commute on f)
n : ℕ
⊢ HPow.hPow (α := R) (∑ i ∈ ∅, f i) n =
    ∑ k ∈ piAntidiag ∅ n, HMul.hMul (α := R) (↑(multinomial ∅ k) : R) (noncommProd ∅ (fun (i : α) ↦ f i ^ k i) ⋯)
have empty : HPow.hPow (α := R) (β := ℕ) (∑ i ∈ ∅, f i) 0 =
  ∑ k ∈ piAntidiag ∅ 0, HMul.hMul (α := R) (↑(multinomial ∅ k) : R) (noncommProd ∅ (fun (i : α) ↦ f i ^ k i) sorry)
Tactic: cases n
Cleared hypotheses: n
-- 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
hc : (↑∅ : Set α).Pairwise (Commute on f)
n : ℕ
empty :
  HPow.hPow (α := R) (β := ℕ) (∑ i ∈ ∅, f i) 0 =
    ∑ k ∈ piAntidiag ∅ 0, HMul.hMul (α := R) (↑(multinomial ∅ k) : R) (noncommProd ∅ (fun (i : α) ↦ f i ^ k i) ⋯)
⊢ HPow.hPow (α := R) (∑ i ∈ ∅, f i) n =
    ∑ k ∈ piAntidiag ∅ n, HMul.hMul (α := R) (↑(multinomial ∅ k) : R) (noncommProd ∅ (fun (i : α) ↦ f i ^ k i) ⋯)
have empty₁ : ∀ (n : ℕ),
  HPow.hPow (α := R) (∑ i ∈ ∅, f i) (n + 1) =
    ∑ k ∈ piAntidiag ∅ (n + 1), HMul.hMul (α := R) (↑(multinomial ∅ k) : R) (noncommProd ∅ (fun (i : α) ↦ f i ^ k i) sorry)
Tactic: cases n
Cleared hypotheses: n
-- 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
s : Finset α
f : α → R
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) ⋯)
have cons : ∀ (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) sorry))
  (hc : (↑(cons a s has) : Set α).Pairwise (Commute on f)) (n : ℕ),
  HPow.hPow (α := R) (∑ i ∈ cons a s has, f i) n =
    ∑ k ∈ (cons a s has).piAntidiag n,
      HMul.hMul (α := R) (↑(multinomial (cons a s has) k) : R) ((cons a s has).noncommProd (fun (i : α) ↦ f i ^ k i) sorry)
Tactic: induction s using Finset.cons_induction generalizing n with
  | empty => cases n <;> simp
  | cons a s has ih => ?_
Cleared hypotheses: s, hc, n
-- 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 : ℕ
⊢ HPow.hPow (α := R) (∑ i ∈ cons a s has, f i) n =
    ∑ k ∈ (cons a s has).piAntidiag n,
      HMul.hMul (α := R) (↑(multinomial (cons a s has) k) : R) ((cons a s has).noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
have cons : (f a + ∑ x ∈ s, f x) ^ n =
  ∑ i ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∑ x ∈ map (addRightEmbedding fun (t : α) ↦ if t = a then i.1 else 0) (s.piAntidiag i.2),
      HMul.hMul (α := R) (↑(multinomial (cons a s has) x) : R) ((cons a s has).noncommProd (fun (i : α) ↦ f i ^ x i) sorry)
Tactic: rw [Finset.sum_cons, piAntidiag_cons, sum_disjiUnion]
-- 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 =
    ∑ i ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∑ x ∈ map (addRightEmbedding fun (t : α) ↦ if t = a then i.1 else 0) (s.piAntidiag i.2),
        HMul.hMul (α := R) (↑(multinomial (cons a s has) x) : R)
          ((cons a s has).noncommProd (fun (i : α) ↦ f i ^ x i) ⋯)
have cons : (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)) sorry)
Tactic: simp only [sum_map, Pi.add_apply, multinomial_cons,
    Pi.add_apply, if_true, Nat.cast_mul, noncommProd_cons,
    if_true, sum_add_distrib, sum_ite_eq', has, if_false, add_zero,
    addRightEmbedding_apply]
-- 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) ⋯))
⊢ (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 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) sorry)
Tactic: rw [sum_congr rfl this]
-- 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) ⋯))
⊢ (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) ⋯)
have 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) sorry)
Tactic: simp only [Nat.antidiagonal_eq_map, sum_map, Function.Embedding.coeFn_mk]
-- 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) ⋯))
⊢ (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) ⋯)
have 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) sorry))
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]