awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
i :
  (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!
have i₁ : HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
  HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
    ∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)!
Tactic: calc
    (2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
      ≤ ((2 * ∑ i ∈ s, f i) ^ (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!) * ∏ i ∈ s, (f i)! := by
      gcongr; exact Nat.factorial_two_mul_le _
    _ = ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)! := by
      rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]; ring
    _ ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)! := by
      gcongr
      rw [← doubleFactorial_two_mul]
      exact doubleFactorial_le_factorial _
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
i :
  (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
i₁ :
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      ∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)!
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!
have i₂ : HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
    ∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)! ≤
  HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!
Tactic: calc
    (2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
      ≤ ((2 * ∑ i ∈ s, f i) ^ (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!) * ∏ i ∈ s, (f i)! := by
      gcongr; exact Nat.factorial_two_mul_le _
    _ = ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)! := by
      rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]; ring
    _ ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)! := by
      gcongr
      rw [← doubleFactorial_two_mul]
      exact doubleFactorial_le_factorial _
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ s
⊢ (↑(fill x m s) : Multiset α).countPerms = n.choose (↑m : ℕ) * (↑s : Multiset α).countPerms
have rw : (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) *
    (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms =
  n.choose (↑m : ℕ) * (↑s : Multiset α).countPerms
Tactic: rw [Multiset.countPerms_filter_ne x]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (hypothesis)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ s
⊢ (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) *
      (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms =
    n.choose (↑m : ℕ) * (↑s : Multiset α).countPerms
have hx₁ : x ∉ (↑s : Multiset α)
Tactic: rw [← mem_coe] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) *
      (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms =
    n.choose (↑m : ℕ) * (↑s : Multiset α).countPerms
have refine_1 : (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) = n.choose (↑m : ℕ)
Tactic: refine congrArg₂ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_1 : (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) = n.choose (↑m : ℕ)
⊢ (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) *
      (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms =
    n.choose (↑m : ℕ) * (↑s : Multiset α).countPerms
have refine_2 : (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms = (↑s : Multiset α).countPerms
Tactic: refine congrArg₂ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) = n.choose (↑m : ℕ)
have refine_1 : n.choose (Multiset.count x (↑(fill x m s) : Multiset α)) = n.choose (↑m : ℕ)
Tactic: rw [card_coe, count_coe_fill_self_of_notMem hx]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_1 : n.choose (Multiset.count x (↑(fill x m s) : Multiset α)) = n.choose (↑m : ℕ)
⊢ (↑(fill x m s) : Multiset α).card.choose (Multiset.count x (↑(fill x m s) : Multiset α)) = n.choose (↑m : ℕ)
have refine_1₁ : n.choose (↑m : ℕ) = n.choose (↑m : ℕ)
Tactic: rw [card_coe, count_coe_fill_self_of_notMem hx]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ (Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α)).countPerms = (↑s : Multiset α).countPerms
have refine_2 : Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α) = (↑s : Multiset α)
Tactic: refine congrArg _ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑(fill x m s) : Multiset α) = (↑s : Multiset α)
have refine_2 : Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑s : Multiset α) +
    Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) =
  (↑s : Multiset α)
Tactic: rw [coe_fill, coe_replicate, Multiset.filter_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑s : Multiset α) +
      Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) =
    (↑s : Multiset α)
have refine_2 : (↑s : Multiset α) + Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) = (↑s : Multiset α)
Tactic: rw [Multiset.filter_eq_self.mpr]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
refine_2 :
  (↑s : Multiset α) + Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) = (↑s : Multiset α)
⊢ Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (↑s : Multiset α) +
      Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) =
    (↑s : Multiset α)
have refine_2₁ : ∀ a ∈ (↑s : Multiset α), x ≠ a
Tactic: rw [Multiset.filter_eq_self.mpr]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ (↑s : Multiset α) + Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) = (↑s : Multiset α)
have refine_2 : Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) = 0
Tactic: rw [add_eq_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
n : ℕ
α : Type u_1
inst : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - (↑m : ℕ))
x : α
hx : x ∉ (↑s : Multiset α)
⊢ Multiset.filter (fun (x_1 : α) ↦ x ≠ x_1) (Multiset.replicate (↑m : ℕ) x) = 0
have refine_2 : ∀ a ∈ Multiset.replicate (↑m : ℕ) x, ¬x ≠ a
Tactic: rw [Multiset.filter_eq_nil]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ Nat.multinomial s (⇑d : (a : σ) → ℕ) = d.multinomial
have rw : (∑ i ∈ s, (d : (a : σ) → ℕ) i)! / ∏ i ∈ s, ((d : (a : σ) → ℕ) i)! =
  (∑ x ∈ s, id ((d : (a : σ) → ℕ) x))! / ∏ x ∈ s, ((d : (a : σ) → ℕ) x)!
Tactic: rw [Nat.multinomial, Finsupp.multinomial,
    sum_of_support_subset _ h _ (by simp), prod_of_support_subset _ h _ (by simp)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : DecidableEq α
l_1 : List α
x : α
l : List α
⊢ (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) (a : α) ↦ a) = (x :: l).sum
have simp : ((HAdd.hAdd (α := ℕ →₀ α) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp)).sum
    fun (x : ℕ) (a : α) ↦ a) =
  x + l.sum
Tactic: simp only [toFinsupp_cons_eq_single_add_embDomain, sum_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : DecidableEq α
l_1 : List α
x : α
l : List α
⊢ ((HAdd.hAdd (α := ℕ →₀ α) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp)).sum
      fun (x : ℕ) (a : α) ↦ a) =
    x + l.sum
have rw : HAdd.hAdd (α := α) (Finsupp.sum (Finsupp.single 0 x) fun (x : ℕ) (a : α) ↦ a)
    (Finsupp.sum (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp) fun (x : ℕ) (a : α) ↦ a) =
  x + l.sum
Tactic: rw [Finsupp.sum_add_index (by simp) (by simp)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
x : ℕ
l : List ℕ
⊢ Finsupp.multinomial (x :: l).toFinsupp = (x + l.sum).choose x * Finsupp.multinomial l.toFinsupp
have rw : Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) *
    Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) =
  (x + l.sum).choose x * Finsupp.multinomial l.toFinsupp
Tactic: rw [Finsupp.multinomial_update 0 (x :: l).toFinsupp]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
x : ℕ
l : List ℕ
⊢ Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) *
      Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) =
    (x + l.sum).choose x * Finsupp.multinomial l.toFinsupp
have e_a : Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) =
  (x + l.sum).choose x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
x : ℕ
l : List ℕ
e_a :
  Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) =
    (x + l.sum).choose x
⊢ Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) *
      Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) =
    (x + l.sum).choose x * Finsupp.multinomial l.toFinsupp
have e_a₁ : Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) = Finsupp.multinomial l.toFinsupp
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
x : ℕ
l : List ℕ
⊢ Nat.choose (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) (((x :: l).toFinsupp : (a : ℕ) → ℕ) 0) =
    (x + l.sum).choose x
have e_a : (Finsupp.sum (x :: l).toFinsupp fun (x : ℕ) ↦ id) = x + l.sum
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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
have 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 : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
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 : ℕ)
have 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 : ℕ)
Tactic: by_cases hi : i = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : ℕ)
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: by_cases hi : i = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (hypothesis)
Goal:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
⊢ Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) = Finsupp.multinomial l.toFinsupp
have this : (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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 : ℕ
⊢ (Finsupp.embDomain succEmb l.toFinsupp : (a : ℕ) → ℕ) (x + 1) =
    (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) l x).getD 0
have rw : (l.toFinsupp : (a : ℕ) → ℕ) (Exists.choose (p := fun (a : ℕ) ↦ (succEmb : (a : ℕ) → ℕ) a = x + 1) sorry) =
  (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) l x).getD 0
Tactic: rw [Finsupp.embDomain_apply, dif_pos ⟨x, by simp [succEmb]⟩]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (hypothesis)
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
⊢ Finsupp.multinomial (Finsupp.update (x :: l).toFinsupp 0 0) = Finsupp.multinomial l.toFinsupp
have h : ∀ (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]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m : Multiset ℕ
l_1 l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (y :: x :: l).multinomial = (x :: y :: l).multinomial
have 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
Tactic: simp only [List.multinomial_cons, ← mul_assoc, List.sum_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m : Multiset ℕ
l_1 l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (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
have 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
Tactic: rw [← Nat.choose_symm (Nat.le_add_right y _), add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m : Multiset ℕ
l_1 l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (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
have 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
Tactic: rw [add_left_comm, Nat.choose_mul (Nat.le_add_right _ _), add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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
⊢ l.multinomial = l''.multinomial
have trans₁ : l''.multinomial = l''.multinomial
Tactic: rw [ih, ih']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m : Multiset ℕ
l l' : List ℕ
h : (List.isSetoid ℕ : List ℕ → List ℕ → Prop) l l'
⊢ l.multinomial = l'.multinomial
have nil : List.multinomial [] = List.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']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m : Multiset ℕ
l l' : List ℕ
h : (List.isSetoid ℕ : List ℕ → List ℕ → Prop) l l'
nil : List.multinomial [] = List.multinomial []
⊢ l.multinomial = l'.multinomial
have cons : ∀ (x : ℕ) {l l' : List ℕ} (hl : l.Perm l') (hl' : l.multinomial = l'.multinomial),
  (x :: l).multinomial = (x :: 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']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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
⊢ l.multinomial = l'.multinomial
have swap : ∀ (x y : ℕ) (l : List ℕ), (y :: x :: l).multinomial = (x :: y :: 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']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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
⊢ l.multinomial = l'.multinomial
have 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
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']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
x : ℕ
m : Multiset ℕ
⊢ (x ::ₘ m).multinomial = (x + m.sum).choose x * m.multinomial
have obtain : ∀ (l : List ℕ), (x ::ₘ ⟦l⟧).multinomial = (x + sum ⟦l⟧).choose x * multinomial ⟦l⟧
Tactic: obtain ⟨l, rfl⟩ := Quotient.exists_rep m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m' : Multiset ℕ
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
have 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
Tactic: simp only [cons_add, sum_cons, sum_add, multinomial_cons, hind, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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).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
have 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
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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).choose m.sum =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x
have 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
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 _)]