awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p x : ℕ
h : x + 1 ≤ 0
h_1 : x + 1 ≠ 0
⊢ (factorization 0 : (a : ℕ) → ℕ) p ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) (((choose 0 (x + 1)).factorization : (a : ℕ) → ℕ) p : ℕ)
      (((x + 1).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
rw :
  LE.le (α := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ)
    ((((n + 1).choose (k + 1) * (k + 1)).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ((n + 1).factorization : (a : ℕ) → ℕ) p ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((((n + 1).choose (k + 1)).factorization : (a : ℕ) → ℕ) p : ℕ)
      (((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]

Premises used: Nat.factorization_mul, Ne.symm, Pi.add_apply, Finsupp.coe_add, Nat.choose_pos, Nat.zero_ne_add_one, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ k + 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
refine : n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)
⊢ LE.le (α := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ)
    ((((n + 1).choose (k + 1) * (k + 1)).factorization : (a : ℕ) → ℕ) p : ℕ)

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))

Premises used: Nat.mul_ne_zero, Ne.symm, Nat.choose_pos, Nat.zero_ne_add_one, Nat.factorization_le_factorization_of_dvd_right, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
rw : n + 1 ∣ (n + 1) * n.choose k
⊢ n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)

Tactic:
rw [← add_one_mul_choose_eq]

Premises used: Nat.add_one_mul_choose_eq
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ n + 1 ∣ (n + 1) * n.choose k

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ n + 1 ∣ (n + 1) * n.choose k

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
a₁ :
  n ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ) =
    n

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ _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:
simp +contextual [Finset.disjoint_right, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]

Premises used: pow_pos, Nat.Prime.pos, Nat.mod_lt, Nat.dvd_iff_mod_eq_zero, Finset.disjoint_right
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ _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 _)]
-- Module: Mathlib.Data.Nat.Choose.Factorization
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})
a : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ) ≤
    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]

Premises used: lt_of_le_of_lt, Nat.Prime.one_lt, Nat.factorization_eq_card_pow_dvd_of_lt, Nat.lt_succ_self, Finset.filter_union_right, Nat.pow_lt_pow_succ, Nat.log_pow, Nat.factorization_choose, Finset.card_union_of_disjoint, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Choose.Factorization
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}) ≤ #(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
-- Module: Mathlib.Data.Nat.Choose.Factorization
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)
a a₁ a₂ 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
⊢ #({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

Premises used: Nat.card_Ico, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
a :
  ((p ^ n).factorization : (a : ℕ) → ℕ) p ≤
    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 : ℕ)

Tactic:
nth_rewrite 1 [← factorization_pow_self (n := n) hp]

Premises used: Nat.factorization_pow_self
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).factorization : (a : ℕ) → ℕ) p ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
factorization_le_factorization_choose_add hkn hk0

Premises used: Nat.factorization_le_factorization_choose_add
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).factorization : (a : ℕ) → ℕ) p ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((k.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
exact factorization_le_factorization_choose_add hkn hk0

Premises used: Nat.factorization_le_factorization_choose_add
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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 : ℕ)
⊢ (((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p = HSub.hSub (β := ℕ) n ((k.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
nth_rewrite 2 [← factorization_choose_prime_pow_add_factorization hp hkn hk0]

Premises used: Nat.factorization_choose_prime_pow_add_factorization
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
rw rw₁ :
  Eq (α := ℕ) ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
    ((((p ^ n).choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (((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:
rw [Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
pos :
  ∀ (h : Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n
neg :
  ∀ (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

Tactic:
by_cases h : (choose n k).factorization p = 0

Premises used: Nat.choose, DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Prime p

Tactic:
have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_not_prime h
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
⊢ k ≤ n

Tactic:
le_of_not_gt fun hnk => h ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
refine : ∀ (hnk : n < k), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ k ≤ n

Tactic:
refine le_of_not_gt fun hnk => h ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
hnk : n < k
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp [choose_eq_zero_of_lt hnk]

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
⊢ k ≤ n

Tactic:
have hkn : k ≤ n := by
    refine le_of_not_gt fun hnk => h ?_
    simp [choose_eq_zero_of_lt hnk]
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
hkn : k ≤ n
neg : #({i ∈ Ico 1 (log p n + 1) | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) ≤ log p n
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ log p n

Tactic:
rw [factorization_choose hp hkn (Nat.lt_add_one _)]

Premises used: Nat.lt_add_one, Nat.factorization_choose
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
hkn : k ≤ n
⊢ #({i ∈ Ico 1 (log p n + 1) | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) ≤ log p n

Tactic:
(card_filter_le ..).trans_eq (Nat.card_Ico _ _)

Premises used: LE.le.trans_eq, Nat.card_Ico, Finset.card_filter_le
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
h : ¬Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
hp : Prime p
hkn : k ≤ n
⊢ #({i ∈ Ico 1 (log p n + 1) | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) ≤ log p n

Tactic:
exact (card_filter_le ..).trans_eq (Nat.card_Ico _ _)

Premises used: LE.le.trans_eq, Nat.card_Ico, Finset.card_filter_le
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hn : 0 < n
⊢ HPow.hPow (β := ℕ) p (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) ≤ n

Tactic:
pow_le_of_le_log hn.ne' factorization_choose_le_log

Premises used: Nat.factorization_choose_le_log, LT.lt.ne', Nat.pow_le_of_le_log
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
p_large : n < HPow.hPow (β := ℕ) p 2
apply : log p n ≤ 1
⊢ LE.le (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
apply factorization_choose_le_log.trans

Premises used: Nat.factorization_choose_le_log, LE.le.trans
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
p_large : n < HPow.hPow (β := ℕ) p 2
inl : ∀ (p_large : 0 < HPow.hPow (β := ℕ) p 2), log p 0 ≤ 1
inr : ∀ (hn0 : n ≠ 0), log p n ≤ 1
⊢ log p n ≤ 1

Tactic:
rcases eq_or_ne n 0 with (rfl | hn0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p k : ℕ
p_large : 0 < HPow.hPow (β := ℕ) p 2
⊢ log p 0 ≤ 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
p_large : n < HPow.hPow (β := ℕ) p 2
hn0 : n ≠ 0
⊢ log p n ≤ 1

Tactic:
Nat.lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)

Premises used: Nat.lt_succ_iff, Iff.mp, Nat.log_lt_of_lt_pow
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
p_large : n < HPow.hPow (β := ℕ) p 2
hn0 : n ≠ 0
⊢ log p n ≤ 1

Tactic:
exact Nat.lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)

Premises used: Nat.lt_succ_iff, Iff.mp, Nat.log_lt_of_lt_pow
-- Module: Mathlib.Data.Nat.Choose.Factorization
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 : ℕ)
inr : ∀ (hp : Prime p), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rcases em' p.Prime with hp | hp

Premises used: Nat.Prime, em'
-- Module: Mathlib.Data.Nat.Choose.Factorization
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 : ℕ)

Tactic:
factorization_eq_zero_of_not_prime (choose n k) hp

Premises used: Nat.choose, Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.Data.Nat.Choose.Factorization
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 : ℕ)

Tactic:
exact factorization_eq_zero_of_not_prime (choose n k) hp

Premises used: Nat.choose, Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.Data.Nat.Choose.Factorization
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 : ℕ)
inr₁ : ∀ (hkn : k ≤ n), Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rcases lt_or_ge n k with hnk | hkn

Premises used: lt_or_ge
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hnk : n < k
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp [choose_eq_zero_of_lt hnk]

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
inr : ∀ ⦃x : ℕ⦄, 1 ≤ x → x < log p n + 1 → k % p ^ x + (n - k) % p ^ x < p ^ x
⊢ Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp only [factorization_choose hp hkn (Nat.lt_add_one _), card_eq_zero, filter_eq_empty_iff,
    mem_Ico, not_le, and_imp]

Premises used: not_le, and_imp, Nat.lt_add_one, Finset.filter_eq_empty_iff, Finset.card_eq_zero, Nat.factorization_choose, Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
inr₁ : ∀ (hi : 1 < i), k % p ^ i + (n - k) % p ^ i < p ^ i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i

Tactic:
rcases eq_or_lt_of_le hi₁ with (rfl | hi)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
inr : p + k % p + (p + (n - k) % p) < succ 2 * p
⊢ k % HPow.hPow (β := ℕ) p 1 + (n - k) % HPow.hPow (β := ℕ) p 1 < HPow.hPow (β := ℕ) p 1

Tactic:
rw [pow_one, ← add_lt_add_iff_left (2 * p), ← succ_mul, two_mul, add_add_add_comm]

Premises used: HMul.hMul, two_mul, Nat.succ_mul, pow_one, add_add_add_comm, OfNat.ofNat, add_lt_add_iff_left
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
rwa₁ : k + (n - k) < succ 2 * p
rwa₂ rwa₃ rwa₄ rwa₅ : n < succ 2 * p
⊢ p * (k / p) + k % p + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p

Tactic:
rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn]

Premises used: Nat.div_add_mod, add_tsub_cancel_of_le
-- Module: Mathlib.Data.Nat.Choose.Factorization
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 + (p + (n - k) % p) < succ 2 * p

Tactic:
exact
      lt_of_le_of_lt
        (add_le_add
          (add_le_add_left (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk)) (k % p))
          (add_le_add_left (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk'))
            ((n - k) % p)))
        (by rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn])

Premises used: Iff.mpr, lt_of_le_of_lt, HSub.hSub, Nat.Prime.pos, add_le_add_left, HMod.hMod, Nat.add_le_add, Nat.one_le_div_iff, le_mul_of_one_le_right'
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
⊢ 3 ≤ p

Tactic:
have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm
-- Module: Mathlib.Data.Nat.Choose.Factorization
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 < 3 * p

Tactic:
hn
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
⊢ 3 * p ≤ p * p

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
⊢ p * p = HPow.hPow (β := ℕ) p 2

Tactic:
(sq p).symm

Premises used: sq, Eq.symm
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
⊢ HPow.hPow (β := ℕ) p 2 ≤ p ^ i

Tactic:
pow_right_mono₀ hp.one_lt.le hi

Premises used: Nat.Prime.one_lt, LT.lt.le, pow_right_mono₀
-- Module: Mathlib.Data.Nat.Choose.Factorization
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₁ : 3 * p ≤ p * p
⊢ n < p ^ i

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

Premises used: Nat.Prime.one_lt, LT.lt.le, sq, pow_right_mono₀, Eq.symm
-- Module: Mathlib.Data.Nat.Choose.Factorization
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

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
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
inr₁ : k + (n - k) < p ^ i
inr₂ inr₃ inr₄ inr₅ : n < p ^ i
⊢ k % p ^ i + (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]

Premises used: lt_of_le_of_lt, Nat.mod_eq_of_lt, tsub_le_self, add_tsub_cancel_of_le
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ Eq (α := ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
factorization_choose_of_lt_three_mul ?_ p_le_n (p_le_n.trans ?_) big

Premises used: Nat.centralBinom, Nat.factorization_choose_of_lt_three_mul, LE.le.trans
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
refine_1 : p ≠ 2
refine_2 : n ≤ 2 * n - n
⊢ Eq (α := ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
refine factorization_choose_of_lt_three_mul ?_ p_le_n (p_le_n.trans ?_) big

Premises used: Nat.factorization_choose_of_lt_three_mul, LE.le.trans
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
refine_2 : n ≤ n + n - n
refine_2₁ refine_2₂ : n ≤ n
⊢ n ≤ 2 * n - n

Tactic:
rw [two_mul, add_tsub_cancel_left]

Premises used: two_mul, add_tsub_cancel_left
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n : ℕ
h : 0 < p
⊢ Eq (α := ℕ) ((0!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Factorization
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 : ℕ)
succ₆ succ₇ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) (((n + 1)!.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]

Premises used: Nat.factorial_succ, Nat.factorization_mul, Pi.add_apply, Finsupp.coe_add, Nat.factorial_ne_zero, Nat.succ_ne_zero, Nat.lt_of_succ_lt, add_zero, Nat.factorization_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n : ℕ
h : n < p
zero : ∀ (h : 0 < p), Eq (α := ℕ) ((0!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
succ :
  ∀ (n : ℕ) (hn : ∀ (h : n < p), Eq (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)) (h : n + 1 < p),
    Eq (α := ℕ) (((n + 1)!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((n !.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]

Premises used: Nat.factorial_succ, Nat.factorization_mul, Pi.add_apply, Finsupp.coe_add, Nat.factorial_ne_zero, Nat.succ_ne_zero, Nat.zero, add_zero, Nat.factorization_eq_zero_of_lt, Nat.succ