awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
h :
  ∀ (i : ℕ),
    Eq (α := ℕ)
      (((HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 : (a : ℕ) → ℕ)
          i :
        ℕ)
      ((Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0 : (a : ℕ) → ℕ) i : ℕ)
⊢ (HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 =
    Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0

Tactic:
ext i
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
i : ℕ
pos :
  ∀ (hi : i = 0),
    Eq (α := ℕ)
      (((HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 : (a : ℕ) → ℕ)
          i :
        ℕ)
      ((Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0 : (a : ℕ) → ℕ) i : ℕ)
neg :
  ∀ (hi : ¬i = 0),
    Eq (α := ℕ)
      (((HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 : (a : ℕ) → ℕ)
          i :
        ℕ)
      ((Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0 : (a : ℕ) → ℕ) i : ℕ)
⊢ Eq (α := ℕ)
    (((HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 : (a : ℕ) → ℕ)
        i :
      ℕ)
    ((Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0 : (a : ℕ) → ℕ) i : ℕ)

Tactic:
by_cases hi : i = 0
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
i : ℕ
hi : i = 0
⊢ Eq (α := ℕ)
    (((HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 : (a : ℕ) → ℕ)
        i :
      ℕ)
    ((Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0 : (a : ℕ) → ℕ) i : ℕ)

Tactic:
simp [hi]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
i : ℕ
hi : ¬i = 0
⊢ Eq (α := ℕ)
    (((HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 : (a : ℕ) → ℕ)
        i :
      ℕ)
    ((Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0 : (a : ℕ) → ℕ) i : ℕ)

Tactic:
simp [Finsupp.update_apply, if_neg hi, Finsupp.single_eq_of_ne hi]

Premises used: Finsupp.single_eq_of_ne, Finsupp.update_apply, if_neg
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
⊢ (HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 =
    Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0

Tactic:
have : (Finsupp.single 0 x + l.toFinsupp.embDomain succEmb).update 0 0 =
    (l.toFinsupp.embDomain succEmb).update 0 0 := by
    ext i
    by_cases hi : i = 0
    · simp [hi]
    · simp [Finsupp.update_apply, if_neg hi, Finsupp.single_eq_of_ne hi]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x_1 : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
this :
  (HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x_1) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 =
    Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0
x : ℕ
⊢ (succEmb : (a : ℕ) → ℕ) x = x + 1

Tactic:
simp [succEmb]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x_1 : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
this :
  (HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x_1) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 =
    Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0
x : ℕ
rw :
  (l.toFinsupp : (a : ℕ) → ℕ) (Exists.choose (p := fun (a : ℕ) ↦ (succEmb : (a : ℕ) → ℕ) a = x + 1) ⋯) =
    (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) l x).getD 0
⊢ (Finsupp.embDomain succEmb l.toFinsupp : (a : ℕ) → ℕ) (x + 1) =
    (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) l x).getD 0

Tactic:
rw [Finsupp.embDomain_apply, dif_pos ⟨x, by simp [succEmb]⟩]

Premises used: Finsupp.embDomain_apply, dif_pos
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x_1 : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
this :
  (HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x_1) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 =
    Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0
x : ℕ
⊢ (l.toFinsupp : (a : ℕ) → ℕ) (Exists.choose (p := fun (a : ℕ) ↦ (succEmb : (a : ℕ) → ℕ) a = x + 1) ⋯) =
    (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) l x).getD 0

Tactic:
simp [succEmb]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
this :
  (HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 =
    Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0
⊢ ∀ (x : ℕ),
    (Finsupp.embDomain succEmb l.toFinsupp : (a : ℕ) → ℕ) (x + 1) =
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) l x).getD 0

Tactic:
have h (x) : (l.toFinsupp.embDomain succEmb) (x + 1) = l[x]?.getD 0 := by
    rw [Finsupp.embDomain_apply, dif_pos ⟨x, by simp [succEmb]⟩]
    simp [succEmb]
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
this :
  (HAdd.hAdd (α := ℕ →₀ ℕ) (Finsupp.single 0 x) (Finsupp.embDomain succEmb l.toFinsupp)).update 0 0 =
    Finsupp.update (Finsupp.embDomain succEmb l.toFinsupp) 0 0
h :
  ∀ (x : ℕ),
    (Finsupp.embDomain succEmb l.toFinsupp : (a : ℕ) → ℕ) (x + 1) =
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) l x).getD 0
⊢ Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) = Finsupp.multinomial l.toFinsupp

Tactic:
simp [toFinsupp_cons_eq_single_add_embDomain, Finsupp.multinomial_eq,
    succEmb, this, Nat.multinomial, h]

Premises used: List.toFinsupp_cons_eq_single_add_embDomain, Nat.multinomial, Finsupp.multinomial_eq
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
l l' : List ℕ
⊢ List.multinomial [] = List.multinomial []

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
l_1 l'_1 : List ℕ
x : ℕ
l l' : List ℕ
hl : l.Perm l'
hl' : l.multinomial = l'.multinomial
⊢ (x :: l).multinomial = (x :: l').multinomial

Tactic:
simp [List.multinomial_cons, hl', hl.sum_nat]

Premises used: List.multinomial_cons, List.Perm.sum_nat
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
l_1 l' : List ℕ
x y : ℕ
l : List ℕ
swap :
  (y + (x + l.sum)).choose y * (x + l.sum).choose x * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial
⊢ (y :: x :: l).multinomial = (x :: y :: l).multinomial

Tactic:
simp only [List.multinomial_cons, ← mul_assoc, List.sum_cons]

Premises used: mul_assoc, List.sum_cons, List.multinomial_cons
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
l_1 l' : List ℕ
x y : ℕ
l : List ℕ
swap :
  (y + (x + l.sum)).choose (x + l.sum) * (x + l.sum).choose x * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial
⊢ (y + (x + l.sum)).choose y * (x + l.sum).choose x * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial

Tactic:
rw [← Nat.choose_symm (Nat.le_add_right y _), add_tsub_cancel_left]

Premises used: Nat.le_add_right, add_tsub_cancel_left, Nat.choose_symm
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
l_1 l' : List ℕ
x y : ℕ
l : List ℕ
swap :
  (x + (y + l.sum)).choose x * (y + l.sum).choose (x + l.sum - x) * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial
⊢ (y + (x + l.sum)).choose (x + l.sum) * (x + l.sum).choose x * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial

Tactic:
rw [add_left_comm, Nat.choose_mul (Nat.le_add_right _ _), add_tsub_cancel_left]

Premises used: Nat.choose_mul, add_left_comm, Nat.le_add_right, add_tsub_cancel_left
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
l_1 l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (x + (y + l.sum)).choose x * (y + l.sum).choose (x + l.sum - x) * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial

Tactic:
simp [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left]

Premises used: Nat.le_add_right, add_tsub_cancel_left, Nat.choose_symm
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
l_1 l'_1 l l' l'' : List ℕ
h : l.Perm l'
h' : l'.Perm l''
ih : l.multinomial = l'.multinomial
ih' trans : l'.multinomial = l''.multinomial
trans₁ trans₂ : l''.multinomial = l''.multinomial
⊢ l.multinomial = l''.multinomial

Tactic:
rw [ih, ih']
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
l l' : List ℕ
h : (List.isSetoid ℕ : List ℕ → List ℕ → Prop) l l'
nil : List.multinomial [] = List.multinomial []
cons :
  ∀ (x : ℕ) {l l' : List ℕ} (hl : l.Perm l') (hl' : l.multinomial = l'.multinomial),
    (x :: l).multinomial = (x :: l').multinomial
swap : ∀ (x y : ℕ) (l : List ℕ), (y :: x :: l).multinomial = (x :: y :: l).multinomial
trans :
  ∀ {l l' l'' : List ℕ} (h : l.Perm l') (h' : l'.Perm l'') (ih : l.multinomial = l'.multinomial)
    (ih' : l'.multinomial = l''.multinomial), l.multinomial = l''.multinomial
⊢ l.multinomial = l'.multinomial

Tactic:
induction h with
  | nil => simp
  | @cons x l l' hl hl' => simp [List.multinomial_cons, hl', hl.sum_nat]
  | @swap x y l =>
    simp only [List.multinomial_cons, ← mul_assoc, List.sum_cons]
    rw [← Nat.choose_symm (Nat.le_add_right y _), add_tsub_cancel_left]
    rw [add_left_comm, Nat.choose_mul (Nat.le_add_right _ _), add_tsub_cancel_left]
    simp [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left]
  | @trans l l' l'' h h' ih ih' => rw [ih, ih']

Premises used: Nat.choose_mul, add_left_comm, mul_assoc, Nat.le_add_right, add_tsub_cancel_left, Multiset.cons, Nat.choose_symm, List.sum_cons, List.multinomial_cons
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
m : Multiset ℕ
obtain : ∀ (l : List ℕ), (x ::ₘ ⟦l⟧).multinomial = (x + sum ⟦l⟧).choose x * multinomial ⟦l⟧
⊢ (x ::ₘ m).multinomial = (x + m.sum).choose x * m.multinomial

Tactic:
obtain ⟨l, rfl⟩ := Quotient.exists_rep m

Premises used: Quotient.exists_rep, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
⊢ (x ::ₘ ⟦l⟧).multinomial = (x + sum ⟦l⟧).choose x * multinomial ⟦l⟧

Tactic:
List.multinomial_cons x l

Premises used: Multiset.sum, Multiset.foldr, List.sum, Finsupp.multinomial, List.multinomial_cons, Multiset.multinomial
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
x : ℕ
l : List ℕ
⊢ (x ::ₘ ⟦l⟧).multinomial = (x + sum ⟦l⟧).choose x * multinomial ⟦l⟧

Tactic:
exact List.multinomial_cons x l

Premises used: List.multinomial_cons
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
⊢ multinomial 0 = 1

Tactic:
rfl

Premises used: Finsupp.multinomial, Multiset.multinomial, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
n : ℕ
⊢ multinomial {n} = 1

Tactic:
simp [← cons_zero, multinomial_cons]

Premises used: Multiset.multinomial_cons, Multiset.cons_zero
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m' : Multiset ℕ
⊢ (0 + m').multinomial = (0 + m').sum.choose (sum 0) * multinomial 0 * m'.multinomial

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
cons :
  (x + (m.sum + m'.sum)).choose x * (m.sum + m'.sum).choose m.sum * m.multinomial * m'.multinomial =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x * m.multinomial * m'.multinomial
⊢ (x ::ₘ m + m').multinomial = (x ::ₘ m + m').sum.choose (x ::ₘ m).sum * (x ::ₘ m).multinomial * m'.multinomial

Tactic:
simp only [cons_add, sum_cons, sum_add, multinomial_cons, hind, ← mul_assoc]

Premises used: Multiset.sum_add, mul_assoc, Multiset.multinomial_cons, Multiset.cons_add, Multiset.sum_cons
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
cons :
  (x + (m.sum + m'.sum)).choose x * (m.sum + m'.sum).choose m.sum =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x
⊢ (x + (m.sum + m'.sum)).choose x * (m.sum + m'.sum).choose m.sum * m.multinomial * m'.multinomial =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x * m.multinomial * m'.multinomial

Tactic:
congr 2
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
cons :
  (x + (m.sum + m'.sum)).choose (x + (m.sum + m'.sum) - x) * (x + (m.sum + m'.sum) - x).choose (x + m.sum - x) =
    (x + (m.sum + m'.sum)).choose (m.sum + m'.sum) * (m.sum + m'.sum).choose m.sum
⊢ (x + (m.sum + m'.sum)).choose x * (m.sum + m'.sum).choose m.sum =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x

Tactic:
rw [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left, eq_comm,
      Nat.choose_mul (Nat.le_add_right _ _), ← Nat.choose_symm (Nat.le_add_right x _)]

Premises used: Nat.choose_mul, Nat.le_add_right, add_tsub_cancel_left, eq_comm, Nat.choose_symm
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose (x + (m.sum + m'.sum) - x) * (x + (m.sum + m'.sum) - x).choose (x + m.sum - x) =
    (x + (m.sum + m'.sum)).choose (m.sum + m'.sum) * (m.sum + m'.sum).choose m.sum

Tactic:
simp [add_tsub_cancel_left]

Premises used: add_tsub_cancel_left
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m m' : Multiset ℕ
empty : (0 + m').multinomial = (0 + m').sum.choose (sum 0) * multinomial 0 * m'.multinomial
cons :
  ∀ (x : ℕ) (m : Multiset ℕ) (hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial),
    (x ::ₘ m + m').multinomial = (x ::ₘ m + m').sum.choose (x ::ₘ m).sum * (x ::ₘ m).multinomial * m'.multinomial
⊢ (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial

Tactic:
induction m using Multiset.induction_on with
  | empty => simp
  | cons x m hind =>
    simp only [cons_add, sum_cons, sum_add, multinomial_cons, hind, ← mul_assoc]
    congr 2
    rw [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left, eq_comm,
      Nat.choose_mul (Nat.le_add_right _ _), ← Nat.choose_symm (Nat.le_add_right x _)]
    simp [add_tsub_cancel_left]

Premises used: Nat.choose_mul, Multiset.sum_add, mul_assoc, Nat.le_add_right, Multiset.multinomial_cons, add_tsub_cancel_left, Multiset.cons, Multiset.cons_add, eq_comm, Nat.choose_symm, Multiset.sum_cons
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
⊢ (HSMul.hSMul (α := ℕ) 0 m).multinomial =
    (Nat.multinomial (Finset.range 0) fun (x : ℕ) ↦ m.sum) * HPow.hPow (β := ℕ) m.multinomial 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k
⊢ k ∉ Finset.range k

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k
succ :
  (m.sum + k • m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + ∑ i ∈ Finset.range k, m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)
⊢ ((k + 1) • m).multinomial = (Nat.multinomial (Finset.range (k + 1)) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ (k + 1)

Tactic:
rw [succ_nsmul', multinomial_add, hk, Finset.range_add_one,
      Nat.multinomial_insert (by simp), sum_add, sum_nsmul, pow_succ']

Premises used: Multiset.sum_add, Multiset.multinomial_add, Multiset.sum_nsmul, Finset.range_add_one, succ_nsmul', Nat.multinomial_insert, pow_succ'
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k
succ :
  (m.sum + k * m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + k * m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)
⊢ (m.sum + k • m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + ∑ i ∈ Finset.range k, m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)

Tactic:
simp [smul_eq_mul, Finset.sum_const, Finset.card_range]

Premises used: Finset.card_range, smul_eq_mul, Finset.sum_const
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k
⊢ (m.sum + k * m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + k * m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
k : ℕ
m : Multiset ℕ
zero :
  (HSMul.hSMul (α := ℕ) 0 m).multinomial =
    (Nat.multinomial (Finset.range 0) fun (x : ℕ) ↦ m.sum) * HPow.hPow (β := ℕ) m.multinomial 0
succ :
  ∀ (k : ℕ) (hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k),
    ((k + 1) • m).multinomial = (Nat.multinomial (Finset.range (k + 1)) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ (k + 1)
⊢ (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k

Tactic:
induction k with
  | zero => simp
  | succ k hk =>
    rw [succ_nsmul', multinomial_add, hk, Finset.range_add_one,
      Nat.multinomial_insert (by simp), sum_add, sum_nsmul, pow_succ']
    simp [smul_eq_mul, Finset.sum_const, Finset.card_range]
    ring

Premises used: Multiset.sum_add, Multiset.multinomial_add, Finset.card_range, Multiset.sum_nsmul, Finset.range_add_one, succ_nsmul', Nat.multinomial_insert, smul_eq_mul, pow_succ', Finset.sum_const
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
k n : ℕ
⊢ (HSMul.hSMul (β := Multiset ℕ) k {n}).multinomial = Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ n

Tactic:
simp [multinomial_nsmul]

Premises used: Multiset.multinomial_nsmul
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
change : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * (↑(n.choose m) : R)

Tactic:
change (x + y) ^ n = ∑ m ∈ range (n + 1), t n m

Premises used: Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
n : ℕ
⊢ t n 0 = y ^ n

Tactic:
simp only [t, choose_zero_right, pow_zero, cast_one, mul_one, one_mul, Nat.sub_zero]

Premises used: pow_zero, Nat.sub_zero, mul_one, Nat.cast_one, Nat.choose_zero_right, one_mul
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
⊢ ∀ (n : ℕ), t n 0 = y ^ n

Tactic:
have h_first : ∀ n, t n 0 = y ^ n := fun n ↦ by
    simp only [t, choose_zero_right, pow_zero, cast_one, mul_one, one_mul, Nat.sub_zero]
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
n : ℕ
⊢ t n n.succ = 0

Tactic:
simp only [t, choose_succ_self, cast_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.cast_zero, Nat.choose_succ_self
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
⊢ ∀ (n : ℕ), t n n.succ = 0

Tactic:
have h_last : ∀ n, t n n.succ = 0 := fun n ↦ by
    simp only [t, choose_succ_self, cast_zero, mul_zero]
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
⊢ i ≤ n

Tactic:
have h_le : i ≤ n := le_of_lt_succ (mem_range.mp h_mem)
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
dsimp :
  x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.succ.choose i.succ) : R) =
    x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R)) + y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
⊢ t n.succ i.succ = x * t n i + y * t n i.succ

Tactic:
dsimp only [t]
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
rw :
  x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) +
      x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R)) + y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.succ.choose i.succ) : R) =
    x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R)) + y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))

Tactic:
rw [choose_succ_succ, cast_add, mul_add]

Premises used: Nat.choose_succ_succ, Nat.cast_add, mul_add
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
e_a : x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₁ :
  x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) +
      x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R)) + y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
e_a : x * x ^ i * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₁ : x * x ^ i * y ^ (n - i) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₂ : x * x ^ i * (y ^ (n - i) * (↑(n.choose i) : R)) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₃ : x * (x ^ i * (y ^ (n - i) * (↑(n.choose i) : R))) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₄ e_a₅ : x * (x ^ i * (y ^ (n - i) * (↑(n.choose i) : R))) = x * (x ^ i * (y ^ (n - i) * (↑(n.choose i) : R)))
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))

Tactic:
rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]

Premises used: mul_assoc, Nat.succ_sub_succ, pow_succ'