awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
hab : a ≠ b
⊢ (f a)! * (f b)! * multinomial {a, b} f = (f a + f b)!

Tactic:
simpa [Finset.sum_pair hab, Finset.prod_pair hab] using multinomial_spec {a, b} f

Premises used: Finset.sum_pair, Finset.prod_pair, Insert.insert, Nat.multinomial_spec, Singleton.singleton
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
h₁ : f a = 1
⊢ multinomial {a, b} f = (f b).succ

Tactic:
simp [h, h₁]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
simp :
  ((f a).succ + (f b).succ).choose (f a).succ =
    ((f a).succ + if b = a then (f a).succ else f b).choose (f a).succ + (f a + (f b).succ).choose (f a)
⊢ multinomial {a, b}
      (Function.update (β := fun (a : α) ↦ ℕ) (Function.update (β := fun (a : α) ↦ ℕ) f a (f a).succ) b (f b).succ) =
    multinomial {a, b} (Function.update (β := fun (a : α) ↦ ℕ) f a (f a).succ) +
      multinomial {a, b} (Function.update (β := fun (a : α) ↦ ℕ) f b (f b).succ)

Tactic:
simp only [binomial_eq_choose, Function.update_apply,
    h, Ne, ite_true, ite_false, not_false_eq_true]

Premises used: ite_false, Function.update_apply, Ne, ite_true, not_false_eq_true, Nat.binomial_eq_choose
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
rw :
  ((f a).succ + (f b).succ).choose (f a).succ = ((f a).succ + f b).choose (f a).succ + (f a + (f b).succ).choose (f a)
⊢ ((f a).succ + (f b).succ).choose (f a).succ =
    ((f a).succ + if b = a then (f a).succ else f b).choose (f a).succ + (f a + (f b).succ).choose (f a)

Tactic:
rw [if_neg h.symm]

Premises used: Ne.symm, if_neg
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
rw :
  (f a + (f b).succ).choose (f a) + (f a + (f b).succ).choose (f a).succ =
    (f a + (f b).succ).choose (f a).succ + (f a + (f b).succ).choose (f a)
⊢ ((f a).succ + (f b).succ).choose (f a).succ = ((f a).succ + f b).choose (f a).succ + (f a + (f b).succ).choose (f a)

Tactic:
rw [add_succ, choose_succ_succ, succ_add_eq_add_succ]

Premises used: Nat.choose_succ_succ, Nat.add_succ, Nat.succ_add_eq_add_succ
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
⊢ (f a + (f b).succ).choose (f a) + (f a + (f b).succ).choose (f a).succ =
    (f a + (f b).succ).choose (f a).succ + (f a + (f b).succ).choose (f a)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
rw : (f a + f b).succ * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ
⊢ (f a + f b).succ * multinomial {a, b} f =
    (f a).succ * multinomial {a, b} (Function.update (β := fun (a : α) ↦ ℕ) f a (f a).succ)

Tactic:
rw [binomial_eq_choose h, binomial_eq_choose h, mul_comm (f a).succ, Function.update_self,
    Function.update_of_ne h.symm]

Premises used: Ne.symm, mul_comm, Function.update_self, Nat.succ, Nat.binomial_eq_choose, Function.update_of_ne
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
rw : (f a + f b + 1) * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ
rw₁ : (f a + f b + 1).choose (f a + 1) * (f a + 1) = ((f a).succ + f b).choose (f a).succ * (f a).succ
rw₂ rw₃ : (f a + f b + 1).choose (f a + 1) * (f a + 1) = (f a + f b).succ.choose (f a).succ * (f a).succ
⊢ (f a + f b).succ * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ

Tactic:
rw [succ_eq_add_one, add_one_mul_choose_eq (f a + f b) (f a), succ_add (f a) (f b)]

Premises used: Nat.succ_eq_add_one, HAdd.hAdd, Nat.add_one_mul_choose_eq, Nat.succ_add
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
a b : ℕ
rw : (![a, b] 0 + ![a, b] 1)! / ((![a, b] 0)! * (![a, b] 1)!) = (a + b)! / (a ! * b !)
⊢ multinomial univ ![a, b] = (a + b)! / (a ! * b !)

Tactic:
rw [multinomial, Fin.sum_univ_two, Fin.prod_univ_two]

Premises used: Nat.multinomial, Fin.prod_univ_two, Fin.sum_univ_two
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
a b : ℕ
⊢ (![a, b] 0 + ![a, b] 1)! / ((![a, b] 0)! * (![a, b] 1)!) = (a + b)! / (a ! * b !)

Tactic:
dsimp only [Matrix.cons_val]

Premises used: Matrix.cons_val
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
a b c : ℕ
rw :
  (![a, b, c] 0 + ![a, b, c] 1 + ![a, b, c] 2)! / ((![a, b, c] 0)! * (![a, b, c] 1)! * (![a, b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)
⊢ multinomial univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)

Tactic:
rw [multinomial, Fin.sum_univ_three, Fin.prod_univ_three]

Premises used: Nat.multinomial, Fin.sum_univ_three, Fin.prod_univ_three
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
a b c : ℕ
⊢ (![a, b, c] 0 + ![a, b, c] 1 + ![a, b, c] 2)! / ((![a, b, c] 0)! * (![a, b, c] 1)! * (![a, b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α →₀ ℕ
⊢ f.multinomial = Nat.multinomial f.support (⇑f : (a : α) → ℕ)

Tactic:
rfl

Premises used: Nat.multinomial, Finsupp.sum, Finsupp.prod, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
e_a : (∑ i ∈ f.support, (f : (a : α) → ℕ) i)! = (∑ i ∈ s, (f : (a : α) → ℕ) i)!
e_a₁ : Eq (α := ℕ) (∏ i ∈ f.support, ((f : (a : α) → ℕ) i)!) (∏ i ∈ s, ((f : (a : α) → ℕ) i)!)
⊢ (∑ i ∈ f.support, (f : (a : α) → ℕ) i)! / ∏ i ∈ f.support, ((f : (a : α) → ℕ) i)! =
    (∑ i ∈ s, (f : (a : α) → ℕ) i)! / ∏ i ∈ s, ((f : (a : α) → ℕ) i)!

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ (∑ i ∈ f.support, (f : (a : α) → ℕ) i)! = (∑ i ∈ s, (f : (a : α) → ℕ) i)!

Tactic:
simp [Finset.sum_subset h]

Premises used: Finset.sum_subset
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
e_a : ∀ x ∈ s, x ∉ f.support → ((f : (a : α) → ℕ) x)! = 1
⊢ Eq (α := ℕ) (∏ i ∈ f.support, ((f : (a : α) → ℕ) i)!) (∏ i ∈ s, ((f : (a : α) → ℕ) i)!)

Tactic:
rw [Finset.prod_subset h]

Premises used: Finset.prod_subset
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ ∀ x ∈ s, x ∉ f.support → ((f : (a : α) → ℕ) x)! = 1

Tactic:
grind [Nat.factorial_eq_one]

Premises used: Nat.factorial_eq_one
-- Module: Mathlib.Data.Nat.Choose.Multinomial
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 :
  ∀ (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 : α) → ℕ)

Tactic:
by_cases h : a ∈ f.support

Premises used: Finsupp.support
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
pos :
  Nat.choose (∑ x ∈ f.support, (f : (a : α) → ℕ) x) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.support.erase a) (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.support.erase a) (⇑(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 : α) → ℕ)

Tactic:
rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.notMem_erase a _),
        Finset.add_sum_erase _ f h, support_update_zero]

Premises used: Finset.add_sum_erase, Nat.multinomial_insert, Finsupp.support_update_zero, Finset.notMem_erase, Finset.insert_erase, DFunLike.coe
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
pos :
  Nat.multinomial (f.support.erase a) (⇑f : (a : α) → ℕ) =
    Nat.multinomial (f.support.erase a) (⇑(f.update a 0) : (a : α) → ℕ)
⊢ Nat.choose (∑ x ∈ f.support, (f : (a : α) → ℕ) x) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.support.erase a) (⇑f : (a : α) → ℕ) =
    Nat.choose (f.sum fun (x : α) ↦ id) ((f : (a : α) → ℕ) a) *
      Nat.multinomial (f.support.erase a) (⇑(f.update a 0) : (a : α) → ℕ)

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial (f.support.erase a) (⇑f : (a : α) → ℕ) =
    Nat.multinomial (f.support.erase a) (⇑(f.update a 0) : (a : α) → ℕ)

Tactic:
Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm

Premises used: Finset.mem_erase, And.left, Nat.multinomial_congr, Iff.mp, OfNat.ofNat, Eq.symm, DFunLike.coe, Function.update_of_ne
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial (f.support.erase a) (⇑f : (a : α) → ℕ) =
    Nat.multinomial (f.support.erase a) (⇑(f.update a 0) : (a : α) → ℕ)

Tactic:
exact Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm

Premises used: Finset.mem_erase, And.left, Nat.multinomial_congr, Iff.mp, OfNat.ofNat, Eq.symm, DFunLike.coe, Function.update_of_ne
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∉ f.support
⊢ Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ)

Tactic:
rw [notMem_support_iff] at h

Premises used: Finsupp.notMem_support_iff
-- Module: Mathlib.Data.Nat.Choose.Multinomial
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 : α) → ℕ)
neg₄ neg₅ : Nat.multinomial f.support (⇑f : (a : α) → ℕ) = Nat.multinomial f.support (⇑f : (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 : α) → ℕ)

Tactic:
rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]

Premises used: Finsupp.update_self, Nat.choose_zero_right, one_mul
-- Module: Mathlib.Data.Nat.Choose.Multinomial
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 : α) → ℕ)
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 : α) → ℕ)
⊢ 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]

Premises used: Finsupp.notMem_support_iff, Finsupp.update_self, Finsupp.support, Finsupp.support_update_zero, Nat.choose_zero_right, one_mul
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
a : α
m : Multiset α
⊢ Finsupp.multinomial.{u_1} (α := α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) =
    Nat.choose (Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) fun (x : α) ↦ id)
        ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a) *
      Finsupp.multinomial (Finsupp.update ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) a 0)

Tactic:
Finsupp.multinomial_update a _

Premises used: Finsupp.multinomial_update
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
a : α
m : Multiset α
h : m.card = Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) fun (x : α) ↦ id
h₁ :
  Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (filter (fun (x : α) ↦ a ≠ x) m) : α →₀ ℕ)
    (Finsupp.update ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) a 0 : α →₀ ℕ)
⊢ 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))

Tactic:
convert! Finsupp.multinomial_update a _

Premises used: Finsupp.multinomial_update
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
a : α
m : Multiset α
h :
  m.card =
    card.{u_1} (α := α) ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m))
h₁ h₂ : m.card = m.card
⊢ m.card = Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) fun (x : α) ↦ id

Tactic:
rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]

Premises used: Finsupp.card_toMultiset, Multiset.toFinsupp_toMultiset
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
a : α
m : Multiset α
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 : ℕ)
⊢ Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (filter (fun (x : α) ↦ a ≠ x) m) : α →₀ ℕ)
    (Finsupp.update ((toFinsupp : (a : Multiset α) → α →₀ ℕ) m) a 0 : α →₀ ℕ)

Tactic:
ext1 a
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
a_1 : α
m : Multiset α
a : α
h :
  (if a_1 ≠ a then count a m else 0) =
    Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0 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 : ℕ)

Tactic:
rw [toFinsupp_apply, count_filter, Finsupp.coe_update]

Premises used: Multiset.toFinsupp_apply, Finsupp.coe_update, Multiset.count_filter
-- Module: Mathlib.Data.Nat.Choose.Multinomial
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
neg :
  ∀ (h : ¬a_1 ≠ a),
    Eq (α := ℕ) (0 : ℕ)
      (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

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Nat.Choose.Multinomial
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
pos₁ pos₂ : count a m = count a m
⊢ count a m =
    Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0 a

Tactic:
rw [Function.update_of_ne h.symm, toFinsupp_apply]

Premises used: Multiset.toFinsupp_apply, Ne.symm, Function.update_of_ne
-- Module: Mathlib.Data.Nat.Choose.Multinomial
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 :
      ℕ)
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) (0 : ℕ)
    (Function.update (β := fun (a : α) ↦ ℕ) (⇑((toFinsupp : (a : Multiset α) → α →₀ ℕ) m : α →₀ ℕ) : (a : α) → ℕ) a_1 0
        a :
      ℕ)

Tactic:
rw [not_ne_iff.1 h, Function.update_self]

Premises used: not_ne_iff, Iff.mp, Function.update_self
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
inst : DecidableEq α
⊢ countPerms.{u_1} (α := α) 0 = 1

Tactic:
simp [countPerms, Finsupp.multinomial]

Premises used: Finsupp.multinomial, Multiset.countPerms
-- Module: Mathlib.Data.Nat.Choose.Multinomial
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) ⋯)
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) ⋯)
⊢ HPow.hPow (α := R) (∑ i ∈ ∅, f i) n =
    ∑ k ∈ piAntidiag ∅ n, HMul.hMul (α := R) (↑(multinomial ∅ k) : R) (noncommProd ∅ (fun (i : α) ↦ f i ^ k i) ⋯)

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f : α → R
hc : (↑∅ : Set α).Pairwise (Commute on f)
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ ∅, f i) 0 =
    ∑ k ∈ piAntidiag ∅ 0, HMul.hMul (α := R) (↑(multinomial ∅ k) : R) (noncommProd ∅ (fun (i : α) ↦ f i ^ k i) ⋯)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
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 + 1) =
    ∑ k ∈ piAntidiag ∅ (n + 1), HMul.hMul (α := R) (↑(multinomial ∅ k) : R) (noncommProd ∅ (fun (i : α) ↦ f i ^ k i) ⋯)

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

Tactic:
?_
-- Module: Mathlib.Data.Nat.Choose.Multinomial
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 : ℕ
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) ⋯))
    (hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ Finset.cons a s has, f i) n =
      ∑ k ∈ (Finset.cons a s has).piAntidiag n,
        HMul.hMul (α := R) (↑(multinomial (Finset.cons a s has) k) : R)
          ((Finset.cons a s has).noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
⊢ 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) ⋯)

Tactic:
induction s using Finset.cons_induction generalizing n with
  | empty => cases n <;> simp
  | cons a s has ih => ?_

Premises used: Finset.cons
-- 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 :
  (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 (Finset.cons a s has) x) : R)
          ((Finset.cons a s has).noncommProd (fun (i : α) ↦ f i ^ x i) ⋯)
⊢ HPow.hPow (α := R) (∑ i ∈ Finset.cons a s has, f i) n =
    ∑ k ∈ (Finset.cons a s has).piAntidiag n,
      HMul.hMul (α := R) (↑(multinomial (Finset.cons a s has) k) : R)
        ((Finset.cons a s has).noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)

Tactic:
rw [Finset.sum_cons, piAntidiag_cons, sum_disjiUnion]

Premises used: Finset.sum_cons, Finset.piAntidiag_cons, Finset.sum_disjiUnion
-- 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 :
  (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)) ⋯)
⊢ (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 (Finset.cons a s has) x) : R)
          ((Finset.cons a s has).noncommProd (fun (i : α) ↦ f i ^ x i) ⋯)

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]

Premises used: if_true, Finset.sum_ite_eq', addRightEmbedding_apply, Finset.sum_add_distrib, Finset.sum_map, if_false, Pi.add_apply, Nat.multinomial_cons, Nat.cast_mul, add_zero, Finset.noncommProd_cons
-- 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 : ℕ × ℕ
g : α → ℕ
⊢ (↑s : Set α) ⊆ (↑(cons a s has) : Set α)

Tactic:
simp