awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi_1 : i < log p n + 1
hi : 1 < i
this : 3 ≤ p
⊢ n < p ^ i
have n₁ : 3 * p ≤ p * p
Tactic: calc
        n < 3 * p := hn
        _ ≤ p * p := by gcongr
        _ = p ^ 2 := (sq p).symm
        _ ≤ p ^ i := pow_right_mono₀ hp.one_lt.le hi
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi_1 : i < log p n + 1
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
have hn₁ : n < p ^ i
Tactic: replace hn : n < p ^ i := by
      have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm
      calc
        n < 3 * p := hn
        _ ≤ p * p := by gcongr
        _ = p ^ 2 := (sq p).symm
        _ ≤ p ^ i := pow_right_mono₀ hp.one_lt.le hi
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi_1 : i < log p n + 1
hi : 1 < i
hn : n < p ^ i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
have inr : k + (n - k) % p ^ i < p ^ i
Tactic: rwa [mod_eq_of_lt (lt_of_le_of_lt hkn hn), mod_eq_of_lt (lt_of_le_of_lt tsub_le_self hn),
      add_tsub_cancel_of_le hkn]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi_1 : i < log p n + 1
hi : 1 < i
hn : n < p ^ i
inr : k + (n - k) % p ^ i < p ^ i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
have inr₁ : k + (n - k) < p ^ i
Tactic: rwa [mod_eq_of_lt (lt_of_le_of_lt hkn hn), mod_eq_of_lt (lt_of_le_of_lt tsub_le_self hn),
      add_tsub_cancel_of_le hkn]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ Eq (α := ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have refine_1 : p ≠ 2
Tactic: refine factorization_choose_of_lt_three_mul ?_ p_le_n (p_le_n.trans ?_) big
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
refine_1 : p ≠ 2
⊢ Eq (α := ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have refine_2 : n ≤ 2 * n - n
Tactic: refine factorization_choose_of_lt_three_mul ?_ p_le_n (p_le_n.trans ?_) big
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n
have refine_2 : n ≤ n + n - n
Tactic: rw [two_mul, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
refine_2 : n ≤ n + n - n
⊢ n ≤ 2 * n - n
have refine_2₁ : n ≤ n
Tactic: rw [two_mul, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n_1 n : ℕ
hn : ∀ (h : n < p), Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h : n + 1 < p
⊢ Eq (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have succ : Eq (α := ℕ) ((((n + 1) * n !).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
      Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n_1 n : ℕ
hn : ∀ (h : n < p), Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h : n + 1 < p
succ : Eq (α := ℕ) ((((n + 1) * n !).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have succ₁ : Eq (α := ℕ) ((n.succ.factorization + n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
      Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n_1 n : ℕ
hn : ∀ (h : n < p), Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h : n + 1 < p
succ : Eq (α := ℕ) ((((n + 1) * n !).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ₁ : Eq (α := ℕ) ((n.succ.factorization + n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have succ₂ : HAdd.hAdd (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n.succ.factorization : (a : ℕ) → ℕ) (⇑n !.factorization : (a : ℕ) → ℕ)
    p =
  0
Tactic: rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
      Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n_1 n : ℕ
hn : ∀ (h : n < p), Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h : n + 1 < p
succ : Eq (α := ℕ) ((((n + 1) * n !).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ₁ : Eq (α := ℕ) ((n.succ.factorization + n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ₂ :
  HAdd.hAdd (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n.succ.factorization : (a : ℕ) → ℕ)
      (⇑n !.factorization : (a : ℕ) → ℕ) p =
    0
⊢ Eq (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have succ₃ : HAdd.hAdd (α := ℕ) (β := ℕ) ((n.succ.factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) = 0
Tactic: rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
      Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n_1 n : ℕ
hn : ∀ (h : n < p), Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h : n + 1 < p
succ : Eq (α := ℕ) ((((n + 1) * n !).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ₁ : Eq (α := ℕ) ((n.succ.factorization + n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ₂ :
  HAdd.hAdd (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n.succ.factorization : (a : ℕ) → ℕ)
      (⇑n !.factorization : (a : ℕ) → ℕ) p =
    0
succ₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((n.succ.factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) = 0
⊢ Eq (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have succ₄ : HAdd.hAdd (α := ℕ) (β := ℕ) ((n.succ.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) = 0
Tactic: rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
      Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n_1 n : ℕ
hn : ∀ (h : n < p), Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h : n + 1 < p
succ : Eq (α := ℕ) ((((n + 1) * n !).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ₁ : Eq (α := ℕ) ((n.succ.factorization + n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ₂ :
  HAdd.hAdd (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n.succ.factorization : (a : ℕ) → ℕ)
      (⇑n !.factorization : (a : ℕ) → ℕ) p =
    0
succ₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((n.succ.factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) = 0
succ₄ : HAdd.hAdd (α := ℕ) (β := ℕ) ((n.succ.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) = 0
⊢ Eq (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have succ₅ : Eq (α := ℕ) ((n.succ.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
      Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n_1 n : ℕ
hn : ∀ (h : n < p), Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h : n + 1 < p
succ : Eq (α := ℕ) ((((n + 1) * n !).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ₁ : Eq (α := ℕ) ((n.succ.factorization + n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ₂ :
  HAdd.hAdd (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n.succ.factorization : (a : ℕ) → ℕ)
      (⇑n !.factorization : (a : ℕ) → ℕ) p =
    0
succ₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((n.succ.factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) = 0
succ₄ : HAdd.hAdd (α := ℕ) (β := ℕ) ((n.succ.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) = 0
succ₅ : Eq (α := ℕ) ((n.succ.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have succ₆ : Eq (α := ℕ) 0 0
Tactic: rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
      Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n : ℕ
h : n < p
⊢ Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have zero : ∀ (h : 0 < p), Eq (α := ℕ) ((0!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
      Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n : ℕ
h : n < p
zero : ∀ (h : 0 < p), Eq (α := ℕ) ((0!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have succ : ∀ (n : ℕ) (hn : ∀ (h : n < p), Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)) (h : n + 1 < p),
  Eq (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
      Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : n < p
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have pos : ∀ (hnk : n < k), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: by_cases! hnk : n < k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : n < p
pos : ∀ (hnk : n < k), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have neg : ∀ (hnk : k ≤ n), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: by_cases! hnk : n < k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have neg : Eq (α := ℕ) (((n ! / (k ! * (n - k)!)).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [choose_eq_factorial_div_factorial hnk,
    factorization_div (factorial_mul_factorial_dvd_factorial hnk), Finsupp.coe_tsub,
    Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : n < p
hnk : k ≤ n
neg : Eq (α := ℕ) (((n ! / (k ! * (n - k)!)).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have neg₁ : Eq (α := ℕ) ((n !.factorization - (k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [choose_eq_factorial_div_factorial hnk,
    factorization_div (factorial_mul_factorial_dvd_factorial hnk), Finsupp.coe_tsub,
    Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : n < p
hnk : k ≤ n
neg : Eq (α := ℕ) (((n ! / (k ! * (n - k)!)).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg₁ : Eq (α := ℕ) ((n !.factorization - (k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have neg₂ : HSub.hSub (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n !.factorization : (a : ℕ) → ℕ)
    (⇑(k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p =
  0
Tactic: rw [choose_eq_factorial_div_factorial hnk,
    factorization_div (factorial_mul_factorial_dvd_factorial hnk), Finsupp.coe_tsub,
    Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : n < p
hnk : k ≤ n
neg : Eq (α := ℕ) (((n ! / (k ! * (n - k)!)).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg₁ : Eq (α := ℕ) ((n !.factorization - (k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg₂ :
  HSub.hSub (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n !.factorization : (a : ℕ) → ℕ)
      (⇑(k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p =
    0
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have neg₃ : HSub.hSub (α := ℕ) (β := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
    (((k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) =
  0
Tactic: rw [choose_eq_factorial_div_factorial hnk,
    factorization_div (factorial_mul_factorial_dvd_factorial hnk), Finsupp.coe_tsub,
    Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : n < p
hnk : k ≤ n
neg : Eq (α := ℕ) (((n ! / (k ! * (n - k)!)).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg₁ : Eq (α := ℕ) ((n !.factorization - (k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg₂ :
  HSub.hSub (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n !.factorization : (a : ℕ) → ℕ)
      (⇑(k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p =
    0
neg₃ :
  HSub.hSub (α := ℕ) (β := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
      (((k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) =
    0
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have neg₄ : HSub.hSub (α := ℕ) (β := ℕ) (0 : ℕ) (((k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) = 0
Tactic: rw [choose_eq_factorial_div_factorial hnk,
    factorization_div (factorial_mul_factorial_dvd_factorial hnk), Finsupp.coe_tsub,
    Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : n < p
hnk : k ≤ n
neg : Eq (α := ℕ) (((n ! / (k ! * (n - k)!)).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg₁ : Eq (α := ℕ) ((n !.factorization - (k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
neg₂ :
  HSub.hSub (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑n !.factorization : (a : ℕ) → ℕ)
      (⇑(k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p =
    0
neg₃ :
  HSub.hSub (α := ℕ) (β := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
      (((k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) =
    0
neg₄ : HSub.hSub (α := ℕ) (β := ℕ) (0 : ℕ) (((k ! * (n - k)!).factorization : (a : ℕ) → ℕ) p : ℕ) = 0
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have neg₅ : Eq (α := ℕ) 0 0
Tactic: rw [choose_eq_factorial_div_factorial hnk,
    factorization_div (factorial_mul_factorial_dvd_factorial hnk), Finsupp.coe_tsub,
    Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
| n.choose k
have rw : (n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
Tactic: rw [← prod_factorization_pow_eq_self (choose_ne_zero hkn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
⊢ ∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) = n.choose k
have conv_rhs : Eq (α := ℕ) (∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ))
  ((n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
Tactic: conv_rhs => rw [← prod_factorization_pow_eq_self (choose_ne_zero hkn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
⊢ Eq (α := ℕ) (∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ))
    ((n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
have rw : Eq (α := ℕ) ((n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
  (∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ))
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
⊢ Eq (α := ℕ) ((n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
    (∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ))
have h : (n.choose k).factorization.support ⊆ Finset.range (n + 1)
Tactic: apply Finset.prod_subset
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
h : (n.choose k).factorization.support ⊆ Finset.range (n + 1)
⊢ Eq (α := ℕ) ((n.choose k).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
    (∏ p ∈ Finset.range (n + 1), HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ))
have hf : ∀ x ∈ Finset.range (n + 1),
  x ∉ (n.choose k).factorization.support →
    Eq (α := ℕ) ((fun (x1 x2 : ℕ) ↦ x1 ^ x2) x (((n.choose k).factorization : (a : ℕ) → ℕ) x)) 1
Tactic: apply Finset.prod_subset
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p ∈ Finset.range (n + 1)
have h : p < n + 1
Tactic: rw [Finset.mem_range]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p < n + 1
have h : ∀ (hp : n + 1 ≤ p), p ∉ (n.choose k).factorization.support
Tactic: contrapose! hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ p ∉ (n.choose k).factorization.support
have h : ¬Ne (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
h : ¬Ne (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ p ∉ (n.choose k).factorization.support
have h₁ : Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
h : ¬Ne (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h₁ : Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ p ∉ (n.choose k).factorization.support
have h₂ : Eq (α := ℕ) 0 0
Tactic: rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n : ℕ
⊢ ∏ p ∈ Finset.range (2 * n + 1), HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) =
    n.centralBinom
have hkn : n ≤ 2 * n
Tactic: apply prod_pow_factorization_choose
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (hypothesis)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
⊢ (↑(n.choose k) : ℤ) ≡ HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ) [ZMOD
    (↑p : ℤ)]
have decompose : HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
Tactic: have decompose : ((X : (ZMod p)[X]) + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p) := by
    simpa using add_pow_eq_mul_pow_add_pow_div_char (X : (ZMod p)[X]) 1 p _
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
⊢ (↑(n.choose k) : ℤ) ≡ HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ) [ZMOD
    (↑p : ℤ)]
have simp : (HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)).coeff k =
  (Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
    (HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ))
Tactic: simp only [← ZMod.intCast_eq_intCast_iff,
    ← coeff_X_add_one_pow _ n k, ← eq_intCast (Int.castRingHom (ZMod p)), ← coeff_map,
    Polynomial.map_pow, Polynomial.map_add, Polynomial.map_one, map_X, decompose]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
⊢ (HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)).coeff k =
    (Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
      (HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ))
have simp : Eq (α := ZMod p)
  (coeff
      (∑ i ∈ range (n % p + 1),
        ∑ j ∈ range (n / p + 1),
          HPow.hPow (α := (ZMod p)[X]) X i * (↑((n % p).choose i) : (ZMod p)[X]) *
            (HPow.hPow (α := (ZMod p)[X]) X (p * j) * (↑((n / p).choose j) : (ZMod p)[X])))
      k :
    ZMod p)
  ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
      (HMul.hMul (α := ℤ) (↑((n % p).choose (k % p)) : ℤ) (↑((n / p).choose (k / p)) : ℤ)) :
    ZMod p)
Tactic: simp only [add_pow, one_pow, mul_one, ← pow_mul, sum_mul_sum]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
| coeff
    (∑ i ∈ range (n % p + 1),
      ∑ j ∈ range (n / p + 1),
        HPow.hPow (α := (ZMod p)[X]) X i * (↑((n % p).choose i) : (ZMod p)[X]) *
          (HPow.hPow (α := (ZMod p)[X]) X (p * j) * (↑((n / p).choose j) : (ZMod p)[X])))
    k
have h : ∀ (k k' : ℕ),
  HPow.hPow (α := (ZMod p)[X]) X k * (↑((n % p).choose k) : (ZMod p)[X]) *
    (HPow.hPow (α := (ZMod p)[X]) X (p * k') * (↑((n / p).choose k') : (ZMod p)[X]))
Tactic: enter [1, 2, k, 2, k']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k_1 p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
k k' : ℕ
| HPow.hPow (α := (ZMod p)[X]) X k * (↑((n % p).choose k) : (ZMod p)[X]) *
    (HPow.hPow (α := (ZMod p)[X]) X (p * k') * (↑((n / p).choose k') : (ZMod p)[X]))
have h : HPow.hPow (α := (ZMod p)[X]) X (k + p * k') * (↑((n % p).choose k * (n / p).choose k') : (ZMod p)[X])
Tactic: rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Lucas (goal)
Goal:
n k p : ℕ
inst : Fact (Nat.Prime p)
decompose :
  HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ n =
    HAdd.hAdd (α := (ZMod p)[X]) X 1 ^ (n % p) * (HPow.hPow (α := (ZMod p)[X]) X p + 1) ^ (n / p)
| coeff
    (∑ i ∈ range (n % p + 1),
      ∑ j ∈ range (n / p + 1),
        HPow.hPow (α := (ZMod p)[X]) X i * (↑((n % p).choose i) : (ZMod p)[X]) *
          (HPow.hPow (α := (ZMod p)[X]) X (p * j) * (↑((n / p).choose j) : (ZMod p)[X])))
    k
have h : ∀ (k k' : ℕ), HPow.hPow (α := (ZMod p)[X]) X (k + p * k') * (↑((n % p).choose k * (n / p).choose k') : (ZMod p)[X])
Tactic: enter [1, 2, k, 2, k']
    rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]