awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
simp_rw :
  HMul.hMul (α := ℤ) (↑(choose 0 (k / p ^ a)) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₁ :
  HMul.hMul (α := ℤ) (↑(choose 0 0) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₂ :
  HMul.hMul (α := ℤ) (↑1 : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₃ :
  HMul.hMul (α := ℤ) 1 (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
have simp_rw₄ : (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
  ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
simp_rw :
  HMul.hMul (α := ℤ) (↑(choose 0 (k / p ^ a)) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₁ :
  HMul.hMul (α := ℤ) (↑(choose 0 0) : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₂ :
  HMul.hMul (α := ℤ) (↑1 : ℤ) (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₃ :
  HMul.hMul (α := ℤ) 1 (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
simp_rw₄ :
  (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
⊢ HMul.hMul (α := ℤ) (↑((n / p ^ a).choose (k / p ^ a)) : ℤ)
      (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
    ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
have simp_rw₅ : ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) ≡
  ∏ i ∈ range a, (↑((n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ n.choose k ≡ ∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]
have rw : (↑(n.choose k) : ℤ) ≡ (↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: rw [← Int.natCast_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
a b p : ℕ
inst : Fact (Nat.Prime p)
⊢ (↑((p * a).choose (p * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
have grw : HMul.hMul (α := ℤ) (↑((p * a % p).choose (p * b % p)) : ℤ) (↑((p * a / p).choose (p * b / p)) : ℤ) ≡
  (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: grw [choose_modEq_choose_mod_mul_choose_div]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
a b p : ℕ
inst : Fact (Nat.Prime p)
⊢ (p * a).choose (p * b) ≡ a.choose b [MOD p]
have rw : (↑((p * a).choose (p * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: rw [← Int.natCast_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
k_1 a b p : ℕ
inst : Fact (Nat.Prime p)
k : ℕ
ih : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (↑((p ^ (k + 1) * a).choose (p ^ (k + 1) * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
have succ : (↑((p * p ^ k * a).choose (p * p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
k_1 a b p : ℕ
inst : Fact (Nat.Prime p)
k : ℕ
ih : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ : (↑((p * p ^ k * a).choose (p * p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (↑((p ^ (k + 1) * a).choose (p ^ (k + 1) * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
have succ₁ : (↑((p * (p ^ k * a)).choose (p * p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
k_1 a b p : ℕ
inst : Fact (Nat.Prime p)
k : ℕ
ih : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ : (↑((p * p ^ k * a).choose (p * p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ₁ : (↑((p * (p ^ k * a)).choose (p * p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (↑((p ^ (k + 1) * a).choose (p ^ (k + 1) * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
have succ₂ : (↑((p * (p ^ k * a)).choose (p * (p ^ k * b))) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
k_1 a b p : ℕ
inst : Fact (Nat.Prime p)
k : ℕ
ih : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ : (↑((p * p ^ k * a).choose (p * p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ₁ : (↑((p * (p ^ k * a)).choose (p * p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ₂ : (↑((p * (p ^ k * a)).choose (p * (p ^ k * b))) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
succ₃ : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (↑((p ^ (k + 1) * a).choose (p ^ (k + 1) * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
have succ₄ : (↑(a.choose b) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
k a b p : ℕ
inst : Fact (Nat.Prime p)
⊢ (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
have zero : (↑((HPow.hPow (β := ℕ) p 0 * a).choose (HPow.hPow (β := ℕ) p 0 * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: induction k with
  | zero => simp [Int.ModEq.refl]
  | succ k ih =>
    grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
k a b p : ℕ
inst : Fact (Nat.Prime p)
zero : (↑((HPow.hPow (β := ℕ) p 0 * a).choose (HPow.hPow (β := ℕ) p 0 * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
⊢ (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
have succ : ∀ (k : ℕ) (ih : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]),
  (↑((p ^ (k + 1) * a).choose (p ^ (k + 1) * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: induction k with
  | zero => simp [Int.ModEq.refl]
  | succ k ih =>
    grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
k a b p : ℕ
inst : Fact (Nat.Prime p)
⊢ (p ^ k * a).choose (p ^ k * b) ≡ a.choose b [MOD p]
have rw : (↑((p ^ k * a).choose (p ^ k * b)) : ℤ) ≡ (↑(a.choose b) : ℤ) [ZMOD (↑p : ℤ)]
Tactic: rw [← Int.natCast_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ multinomial (cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
have rw : LT.lt (α := ℕ) 0 (∏ i ∈ cons a s ha, (f i)!)
Tactic: rw [multinomial, Nat.div_eq_iff_eq_mul_left _ (prod_factorial_dvd_factorial_sum _ _), prod_cons,
    multinomial, mul_assoc, mul_left_comm _ (f a)!,
    Nat.div_mul_cancel (prod_factorial_dvd_factorial_sum _ _), ← mul_assoc, Nat.choose_symm_add,
    Nat.add_choose_mul_factorial_mul_factorial, Finset.sum_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
ha : a ∉ s
f : α → ℕ
⊢ multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
have rw : multinomial (cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
Tactic: rw [← cons_eq_insert _ _ ha, multinomial_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
ha : a ∉ s
f : α → ℕ
rw : multinomial (cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
⊢ multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
have rw₁ : (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
Tactic: rw [← cons_eq_insert _ _ ha, multinomial_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α → ℕ
⊢ multinomial {a} f = 1
have rw : (f a + ∑ i ∈ ∅, f i).choose (f a) * multinomial ∅ f = 1
Tactic: rw [← cons_empty, multinomial_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ i ∈ insert a s, f i)! / ∏ i ∈ insert a s, (f i)! = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)
have rw : HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * (∑ x ∈ s, f x)! / (1! * ∏ x ∈ s, (f x)!) =
  (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)
Tactic: rw [Finset.sum_insert h, Finset.prod_insert h, h₁, add_comm, ← succ_eq_add_one, factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * (∑ x ∈ s, f x)! / (1! * ∏ x ∈ s, (f x)!) =
    (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)
have simp : HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! =
  (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)
Tactic: simp only [factorial, succ_eq_add_one, zero_add, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! =
    (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)
have rw : HAdd.hAdd (α := ℕ) (∑ x ∈ s, f x) 1 * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!) =
  (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)
Tactic: rw [Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)! = (∑ i ∈ s, g i)! / ∏ i ∈ s, (g i)!
have e_a : (∑ i ∈ s, f i)! = (∑ i ∈ s, g i)!
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
e_a : (∑ i ∈ s, f i)! = (∑ i ∈ s, g i)!
⊢ (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)! = (∑ i ∈ s, g i)! / ∏ i ∈ s, (g i)!
have e_a₁ : Eq (α := ℕ) (∏ i ∈ s, (f i)!) (∏ i ∈ s, (g i)!)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ (∑ i ∈ s, f i)! = (∑ i ∈ s, g i)!
have e_a : (s.sum g)! = (∑ i ∈ s, g i)!
Tactic: rw [Finset.sum_congr rfl h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
a : α
ha : a ∈ s
⊢ (f a)! = (g a)!
have rw : (g a)! = (g a)!
Tactic: rw [h a ha]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ multinomial s f = multinomial t g
have rw : (∑ i ∈ s, f i)! = (∑ i ∈ t, g i)!
Tactic: rw [← Nat.mul_right_inj (prod_ne_zero_iff.mpr (fun x _ ↦ factorial_ne_zero (g x))),
    multinomial_spec, prod_congr_of_eq_on_inter (g := fun a ↦ (f a)!) (s₂ := s) (by aesop)
    (by aesop) (by aesop), multinomial_spec s f]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ (∑ i ∈ s, f i)! = (∑ i ∈ t, g i)!
have e_a : Eq (α := ℕ) (∑ i ∈ s, f i) (∑ i ∈ t, g i)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
⊢ multinomial s (Pi.single (M := fun (a : α) ↦ ℕ) a n) = 1
have rw : (if a ∈ s then n else 0)! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
Tactic: rw [← Nat.mul_right_inj (prod_ne_zero_iff.mpr (fun _ _ ↦ factorial_ne_zero _)), mul_one,
    multinomial_spec, sum_pi_single']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
⊢ (if a ∈ s then n else 0)! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
have pos : ∀ (ha : a ∈ s), n ! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
pos : ∀ (ha : a ∈ s), n ! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
⊢ (if a ∈ s then n else 0)! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
have neg : ∀ (ha : a ∉ s), 0! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∈ s
⊢ n ! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
have pos : n ! = (Pi.single (M := fun (a : α) ↦ ℕ) a n a)!
Tactic: rw [Finset.prod_eq_single a (by simp_all) (by simp_all), Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∈ s
pos : n ! = (Pi.single (M := fun (a : α) ↦ ℕ) a n a)!
⊢ n ! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
have pos₁ : n ! = n !
Tactic: rw [Finset.prod_eq_single a (by simp_all) (by simp_all), Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∉ s
⊢ 0! = ∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!
have neg : Eq (α := ℕ) (∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!) 1
Tactic: rw [eq_comm, factorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∉ s
⊢ Eq (α := ℕ) (∏ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)!) 1
have neg : ∀ x ∈ s, (Pi.single (M := fun (a : α) ↦ ℕ) a n x)! = 1
Tactic: apply Finset.prod_eq_one
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∉ s
x : α
hb : x ∈ s
⊢ (Pi.single (M := fun (a : α) ↦ ℕ) a n x)! = 1
have neg : (if x = a then n else 0)! = 1
Tactic: rw [Pi.single_apply, if_neg (ne_of_mem_of_not_mem hb ha), factorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∉ s
x : α
hb : x ∈ s
neg : (if x = a then n else 0)! = 1
⊢ (Pi.single (M := fun (a : α) ↦ ℕ) a n x)! = 1
have neg₁ : 0! = 1
Tactic: rw [Pi.single_apply, if_neg (ne_of_mem_of_not_mem hb ha), factorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst : DecidableEq α
ha : a ∉ s
x : α
hb : x ∈ s
neg : (if x = a then n else 0)! = 1
neg₁ : 0! = 1
⊢ (Pi.single (M := fun (a : α) ↦ ℕ) a n x)! = 1
have neg₂ : Eq (α := ℕ) 1 1
Tactic: rw [Pi.single_apply, if_neg (ne_of_mem_of_not_mem hb ha), factorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
⊢ 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)
have 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)
Tactic: simp only [binomial_eq_choose, Function.update_apply,
    h, Ne, ite_true, ite_false, not_false_eq_true]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
⊢ ((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)
have 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)
Tactic: rw [if_neg h.symm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
⊢ ((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)
have 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)
Tactic: rw [add_succ, choose_succ_succ, succ_add_eq_add_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
f : α → ℕ
a b : α
inst : DecidableEq α
h : a ≠ b
⊢ (f a + f b).succ * multinomial {a, b} f =
    (f a).succ * multinomial {a, b} (Function.update (β := fun (a : α) ↦ ℕ) f a (f a).succ)
have 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
Tactic: rw [binomial_eq_choose h, binomial_eq_choose h, mul_comm (f a).succ, Function.update_self,
    Function.update_of_ne h.symm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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
⊢ (f a + f b).succ * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ
have 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
Tactic: rw [succ_eq_add_one, add_one_mul_choose_eq (f a + f b) (f a), succ_add (f a) (f b)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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
⊢ (f a + f b).succ * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ
have 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
Tactic: rw [succ_eq_add_one, add_one_mul_choose_eq (f a + f b) (f a), succ_add (f a) (f b)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
a b : ℕ
⊢ multinomial univ ![a, b] = (a + b)! / (a ! * b !)
have rw : (![a, b] 0 + ![a, b] 1)! / ((![a, b] 0)! * (![a, b] 1)!) = (a + b)! / (a ! * b !)
Tactic: rw [multinomial, Fin.sum_univ_two, Fin.prod_univ_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
a b c : ℕ
⊢ multinomial univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)
have 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 !)
Tactic: rw [multinomial, Fin.sum_univ_three, Fin.prod_univ_three]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ (∑ i ∈ f.support, (f : (a : α) → ℕ) i)! / ∏ i ∈ f.support, ((f : (a : α) → ℕ) i)! =
    (∑ i ∈ s, (f : (a : α) → ℕ) i)! / ∏ i ∈ s, ((f : (a : α) → ℕ) i)!
have e_a : (∑ i ∈ f.support, (f : (a : α) → ℕ) i)! = (∑ i ∈ s, (f : (a : α) → ℕ) i)!
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
e_a : (∑ 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)!
have e_a₁ : Eq (α := ℕ) (∏ i ∈ f.support, ((f : (a : α) → ℕ) i)!) (∏ i ∈ s, ((f : (a : α) → ℕ) i)!)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ Eq (α := ℕ) (∏ i ∈ f.support, ((f : (a : α) → ℕ) i)!) (∏ i ∈ s, ((f : (a : α) → ℕ) i)!)
have e_a : ∀ x ∈ s, x ∉ f.support → ((f : (a : α) → ℕ) x)! = 1
Tactic: rw [Finset.prod_subset h]
-- 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: by_cases h : a ∈ f.support
-- 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: by_cases h : a ∈ f.support
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
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 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 : α) → ℕ)
Tactic: rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.notMem_erase a _),
        Finset.add_sum_erase _ f h, support_update_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ 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 : α) → ℕ)
have pos : Nat.multinomial (f.support.erase a) (⇑f : (a : α) → ℕ) =
  Nat.multinomial (f.support.erase a) (⇑(f.update a 0) : (a : α) → ℕ)
Tactic: congr 1