awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ) (hm : m ∈ Ico (p * n + 1) (p * (n + 1))), Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw :
  (factorization (∏ x ∈ Ico 1 (p * (n + 1) + 1), x) : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
rw₁ :
  ∑ x ∈ Ico 1 (p * (n + 1) + 1), (x.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
rw₂ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p)
      (∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), (i.factorization : (a : ℕ) → ℕ) p) =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
rw₃ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p)
      (∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), (i.factorization : (a : ℕ) → ℕ) p) =
    HAdd.hAdd (α := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ))
rw₄ :
  ∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p +
      HAdd.hAdd (α := ℕ) (β := ℕ) (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), (k.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((p * (n + 1)).factorization : (a : ℕ) → ℕ) p : ℕ) =
    HAdd.hAdd (α := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ))
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((p * n)!.factorization : (a : ℕ) → ℕ) p : ℕ)
        (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
      1
have rw₅ : ∑ i ∈ Ico 1 (p * n + 1), (i.factorization : (a : ℕ) → ℕ) p +
    HAdd.hAdd (α := ℕ) (β := ℕ) (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), (k.factorization : (a : ℕ) → ℕ) p : ℕ)
      (((p * (n + 1)).factorization : (a : ℕ) → ℕ) p : ℕ) =
  HAdd.hAdd (α := ℕ) ((factorization (∏ x ∈ Ico 1 (p * n + 1), x) : (a : ℕ) → ℕ) p : ℕ)
    (HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ))
Tactic: rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), ← sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2,
    ← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm,
    coe_add, Pi.add_apply, hp.factorization_self, sum_congr rfl h4, sum_const_zero, zero_add,
    add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : ((p * n)!.factorization : (a : ℕ) → ℕ) p = HAdd.hAdd (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) n
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (n + 1)
have succ : HAdd.hAdd (β := ℕ) (HAdd.hAdd (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) n)
      (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) +
    1 =
  HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) +
    (n + 1)
Tactic: simp [factorization_factorial_mul_succ hp, ih, factorial_succ,
      factorization_mul (zero_ne_add_one n).symm (factorial_ne_zero n)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ ((p * n)!.factorization : (a : ℕ) → ℕ) p = HAdd.hAdd (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) n
have zero : ((p * 0)!.factorization : (a : ℕ) → ℕ) p = HAdd.hAdd (α := ℕ) (β := ℕ) ((0!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp [factorization_factorial_mul_succ hp, ih, factorial_succ,
      factorization_mul (zero_ne_add_one n).symm (factorial_ne_zero n)]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
n p : ℕ
hp : Prime p
zero :
  ((p * 0)!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((0!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ ((p * n)!.factorization : (a : ℕ) → ℕ) p = HAdd.hAdd (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) n
have succ : ∀ (n : ℕ)
  (ih : ((p * n)!.factorization : (a : ℕ) → ℕ) p = HAdd.hAdd (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) n),
  ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp [factorization_factorial_mul_succ hp, ih, factorial_succ,
      factorization_mul (zero_ne_add_one n).symm (factorial_ne_zero n)]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ (n !.factorization : (a : ℕ) → ℕ) p ≤ n / (p - 1)
have rw : ∑ i ∈ Ico 1 (log p n + 1), n / p ^ i ≤ n / (p - 1)
Tactic: rw [factorization_factorial hp (Nat.lt_add_one (log p n))]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((((n + k).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      (((k ! * n !).factorization : (a : ℕ) → ℕ) p : ℕ) =
    HAdd.hAdd (β := ℕ) (#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}))
      (((k ! * n !).factorization : (a : ℕ) → ℕ) p : ℕ)
have h2 : (n + k).choose k * k ! * n ! = (n + k)!
Tactic: have h2 := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((((n + k).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      (((k ! * n !).factorization : (a : ℕ) → ℕ) p : ℕ) =
    HAdd.hAdd (β := ℕ) (#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}))
      (((k ! * n !).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 b, k / p ^ i) (∑ i ∈ Ico 1 b, (n + k - k) / p ^ i) +
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n + k - k) % p ^ i}) =
  #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) +
    HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 b, k / p ^ i) (∑ i ∈ Ico 1 b, n / p ^ i)
Tactic: rw [← Pi.add_apply, ← coe_add, ← factorization_mul (ne_of_gt <| choose_pos (le_add_left k n))
      (by positivity), ← mul_assoc, h2,
      factorization_factorial hp hnb, factorization_mul (factorial_ne_zero k) (factorial_ne_zero n),
      coe_add, Pi.add_apply, factorization_factorial hp ((log_mono_right (le_add_left k n)).trans_lt
      hnb), factorization_factorial hp ((log_mono_right (le_add_left n k)).trans_lt
      (add_comm n k ▸ hnb)), multiplicity_choose_aux hp (le_add_left k n)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ (((n + k).choose k).factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})
have h₁ : HAdd.hAdd (α := ℕ) (β := ℕ) ((((n + k).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
    (((k ! * n !).factorization : (a : ℕ) → ℕ) p : ℕ) =
  HAdd.hAdd (β := ℕ) (#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}))
    (((k ! * n !).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: have h₁ : (choose (n + k) k).factorization p + (k ! * n !).factorization p
    = #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i} + (k ! * n !).factorization p := by
    have h2 := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
    rw [← Pi.add_apply, ← coe_add, ← factorization_mul (ne_of_gt <| choose_pos (le_add_left k n))
      (by positivity), ← mul_assoc, h2,
      factorization_factorial hp hnb, factorization_mul (factorial_ne_zero k) (factorial_ne_zero n),
      coe_add, Pi.add_apply, factorization_factorial hp ((log_mono_right (le_add_left k n)).trans_lt
      hnb), factorization_factorial hp ((log_mono_right (le_add_left n k)).trans_lt
      (add_comm n k ▸ hnb)), multiplicity_choose_aux hp (le_add_left k n)]
    simp only [add_tsub_cancel_right, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})
have rw : Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
  ((((n - k + k).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [← factorization_choose' hp ((Nat.sub_add_cancel hkn).symm ▸ hnb), Nat.sub_add_cancel hkn]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
rw :
  Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
    ((((n - k + k).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})
have rw₁ : Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [← factorization_choose' hp ((Nat.sub_add_cancel hkn).symm ▸ hnb), Nat.sub_add_cancel hkn]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
a b c : ℕ
h : b ∣ c
hb : b ≠ 0
hc : c ≠ 0
⊢ LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a : ℕ) ((c.factorization : (a : ℕ) → ℕ) a : ℕ)
have obtain : ∀ (k : ℕ) (hc : b * k ≠ 0),
  LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a : ℕ) (((b * k).factorization : (a : ℕ) → ℕ) a : ℕ)
Tactic: obtain ⟨k, rfl⟩ := h
Cleared hypotheses: c, h, hc
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ ((n + 1).factorization : (a : ℕ) → ℕ) p ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((((n + 1).choose (k + 1)).factorization : (a : ℕ) → ℕ) p : ℕ)
      (((k + 1).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : LE.le (α := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ)
  ((((n + 1).choose (k + 1) * (k + 1)).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [← Pi.add_apply, ← coe_add, ← factorization_mul (ne_of_gt <| choose_pos hkn)
      (zero_ne_add_one k).symm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ LE.le (α := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ)
    ((((n + 1).choose (k + 1) * (k + 1)).factorization : (a : ℕ) → ℕ) p : ℕ)
have refine : n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)
Tactic: refine factorization_le_factorization_of_dvd_right ?_ (zero_ne_add_one n).symm
      (Nat.mul_ne_zero (ne_of_gt <| choose_pos hkn) (by positivity))
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)
have rw : n + 1 ∣ (n + 1) * n.choose k
Tactic: rw [← add_one_mul_choose_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ) =
    n
have a : HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
    ((k.factorization : (a : ℕ) → ℕ) p : ℕ) ≤
  n
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
a :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ) ≤
    n
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ) =
    n
have a₁ : n ≤
  HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
    ((k.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ) ≤
    n
have hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
Tactic: have hdisj : Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
        {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
      simp +contextual [Finset.disjoint_right, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ) ≤
    n
have a : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
Tactic: rw [factorization_choose hp hkn (lt_succ_self _), factorization_eq_card_pow_dvd_of_lt hp
      hk0.bot_lt (lt_of_le_of_lt hkn <| Nat.pow_lt_pow_succ hp.one_lt), log_pow hp.one_lt,
      ← card_union_of_disjoint hdisj, filter_union_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
have filter_le_Ico : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ #(Ico 1 n.succ)
Tactic: have filter_le_Ico := (Ico 1 n.succ).card_filter_le
      fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
filter_le_Ico : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ #(Ico 1 n.succ)
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
have a : ∀ (filter_le_Ico : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n.succ - 1),
  #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
Tactic: rwa [card_Ico 1 n.succ] at filter_le_Ico
Cleared hypotheses: filter_le_Ico
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ n ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ)
have a : ((p ^ n).factorization : (a : ℕ) → ℕ) p ≤
  HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
    ((k.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: nth_rewrite 1 [← factorization_pow_self (n := n) hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ (((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p = HSub.hSub (β := ℕ) n ((k.factorization : (a : ℕ) → ℕ) p : ℕ)
have nth_rewrite : (((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p =
  HSub.hSub (β := ℕ)
    (HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ))
    ((k.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: nth_rewrite 2 [← factorization_choose_prime_pow_add_factorization hp hkn hk0]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ (((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p =
    HSub.hSub (β := ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
        ((k.factorization : (a : ℕ) → ℕ) p : ℕ))
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : Eq (α := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
  ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n
have pos : ∀ (h : Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
  ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n
Tactic: by_cases h : (choose n k).factorization p = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
pos :
  ∀ (h : Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n
have neg : ∀ (h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
  ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n
Tactic: by_cases h : (choose n k).factorization p = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n
have hp : Prime p
Tactic: have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_not_prime h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
⊢ k ≤ n
have refine : ∀ (hnk : n < k), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: refine le_of_not_gt fun hnk => h ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (hypothesis)
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n
have hkn : k ≤ n
Tactic: have hkn : k ≤ n := by
    refine le_of_not_gt fun hnk => h ?_
    simp [choose_eq_zero_of_lt hnk]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
hkn : k ≤ n
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n
have neg : #({i ∈ Ico 1 (log p n + 1) | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) ≤ log p n
Tactic: rw [factorization_choose hp hkn (Nat.lt_add_one _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
p_large : n < HPow.hPow (β := ℕ) p 2
⊢ LE.le (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have apply : log p n ≤ 1
Tactic: apply factorization_choose_le_log.trans
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
p_large : n < HPow.hPow (β := ℕ) p 2
⊢ log p n ≤ 1
have inl : ∀ (p_large : 0 < HPow.hPow (β := ℕ) p 2), log p 0 ≤ 1
Tactic: rcases eq_or_ne n 0 with (rfl | hn0)
Cleared hypotheses: n, p_large
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Factorization (goal)
Goal:
p n k : ℕ
p_large : n < HPow.hPow (β := ℕ) p 2
inl : ∀ (p_large : 0 < HPow.hPow (β := ℕ) p 2), log p 0 ≤ 1
⊢ log p n ≤ 1
have inr : ∀ (hn0 : n ≠ 0), log p n ≤ 1
Tactic: rcases eq_or_ne n 0 with (rfl | hn0)
-- 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
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have inl : ∀ (hp : ¬Prime p), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rcases em' p.Prime with hp | hp
-- 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
inl : ∀ (hp : ¬Prime p), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have inr : ∀ (hp : Prime p), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rcases em' p.Prime with hp | hp
-- 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
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have inr : ∀ (hnk : n < k), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rcases lt_or_ge n k with hnk | 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
hn : n < 3 * p
hp : Prime p
inr : ∀ (hnk : n < k), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have inr₁ : ∀ (hkn : k ≤ n), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rcases lt_or_ge n k with hnk | 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
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have inr : ∀ ⦃x : ℕ⦄, 1 ≤ x → x < log p n + 1 → k % p ^ x + (n - k) % p ^ x < p ^ x
Tactic: simp only [factorization_choose hp hkn (Nat.lt_add_one _), card_eq_zero, filter_eq_empty_iff,
    mem_Ico, not_le, and_imp]
-- 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 : i < log p n + 1
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
have inr : ∀ (hi₁ : LE.le (α := ℕ) 1 1) (hi : 1 < log p n + 1),
  k % HPow.hPow (β := ℕ) p 1 + (n - k) % HPow.hPow (β := ℕ) p 1 < HPow.hPow (β := ℕ) p 1
Tactic: rcases eq_or_lt_of_le hi₁ with (rfl | hi)
Cleared hypotheses: i, hi₁, hi
-- 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 : i < log p n + 1
inr :
  ∀ (hi₁ : LE.le (α := ℕ) 1 1) (hi : 1 < log p n + 1),
    k % HPow.hPow (β := ℕ) p 1 + (n - k) % HPow.hPow (β := ℕ) p 1 < HPow.hPow (β := ℕ) p 1
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
have inr₁ : ∀ (hi : 1 < i), k % p ^ i + (n - k) % p ^ i < p ^ i
Tactic: rcases eq_or_lt_of_le hi₁ with (rfl | hi)
-- 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
hi₁ : LE.le (α := ℕ) 1 1
hi : 1 < log p n + 1
⊢ k % HPow.hPow (β := ℕ) p 1 + (n - k) % HPow.hPow (β := ℕ) p 1 < HPow.hPow (β := ℕ) p 1
have inr : p + k % p + (p + (n - k) % p) < succ 2 * p
Tactic: rw [pow_one, ← add_lt_add_iff_left (2 * p), ← succ_mul, two_mul, add_add_add_comm]
-- 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
hi₁ : LE.le (α := ℕ) 1 1
hi : 1 < log p n + 1
⊢ p * (k / p) + k % p + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p
have rwa : k + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p
Tactic: rwa [div_add_mod, div_add_mod, 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
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : LE.le (α := ℕ) 1 1
hi : 1 < log p n + 1
rwa : k + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p
⊢ p * (k / p) + k % p + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p
have rwa₁ : k + (n - k) < succ 2 * p
Tactic: rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn]
-- 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
⊢ n < p ^ i
have this : 3 ≤ p
Tactic: have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm