awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
inl : choose 0 k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
inr : ∀ (hn : n > 0), n.choose k ≤ HPow.hPow (α := ℕ) 2 n
⊢ n.choose k ≤ HPow.hPow (α := ℕ) 2 n

Tactic:
obtain (rfl | hn) := eq_zero_or_pos n

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
k : ℕ
inl : choose 0 0 ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
inl₁ : ∀ (n : ℕ), choose 0 (n + 1) ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ choose 0 k ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0

Tactic:
cases k
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
⊢ choose 0 0 ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n : ℕ
⊢ choose 0 (n + 1) ≤ HPow.hPow (α := ℕ) (β := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ HPow.hPow (α := ℕ) 2 n

Tactic:
(Nat.choose_lt_two_pow _ _ hn).le

Premises used: Nat.choose_lt_two_pow, LT.lt.le
-- Module: Mathlib.Data.Nat.Choose.Bounds
Goal:
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ HPow.hPow (α := ℕ) 2 n

Tactic:
exact (Nat.choose_lt_two_pow _ _ hn).le

Premises used: Nat.choose_lt_two_pow, LT.lt.le
-- Module: Mathlib.Data.Nat.Choose.Cast
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
h : a ≤ b
⊢ ∀ {n : ℕ}, Ne.{u_1 + 1} (α := K) (↑n ! : K) 0

Tactic:
have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_pos _).ne'
-- Module: Mathlib.Data.Nat.Choose.Cast
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := K) (↑n ! : K) 0
rw : (↑(b.choose a) : K) * HMul.hMul (α := K) (↑a ! : K) (↑(b - a)! : K) = (↑b ! : K)
⊢ (↑(b.choose a) : K) = (↑b ! : K) / HMul.hMul (α := K) (↑a ! : K) (↑(b - a)! : K)

Tactic:
rw [eq_div_iff_mul_eq (mul_ne_zero this this)]

Premises used: eq_div_iff_mul_eq, mul_ne_zero
-- Module: Mathlib.Data.Nat.Choose.Cast
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, Ne.{u_1 + 1} (α := K) (↑n ! : K) 0
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  ∀ (this : ∀ {n : ℕ}, ¬n ! = 0), b.choose a * (a ! * (b - a)!) = b !
rw_mod_cast₆ : ∀ (this : ∀ {n : ℕ}, ¬n ! = 0), b.choose a * a ! * (b - a)! = b !
⊢ (↑(b.choose a) : K) * HMul.hMul (α := K) (↑a ! : K) (↑(b - a)! : K) = (↑b ! : K)

Tactic:
rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]

Premises used: mul_assoc, Nat.choose_mul_factorial_mul_factorial
-- Module: Mathlib.Data.Nat.Choose.Cast
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
rw :
  (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑(a + b - a)! : K) =
    (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K)
rw₁ rw₂ :
  (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K) =
    (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K)
⊢ (↑((a + b).choose a) : K) = (↑(a + b)! : K) / HMul.hMul (α := K) (↑a ! : K) (↑b ! : K)

Tactic:
rw [cast_choose K (le_add_right _ _), Nat.add_sub_cancel_left]

Premises used: Nat.le_add_right, Nat.add_sub_cancel_left, Nat.cast_choose
-- Module: Mathlib.Data.Nat.Choose.Cast
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : ℕ
rw : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.descFactorial 2) : K) 2
rw₁ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2! * a.choose 2) : K) 2
rw₂ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(2 * a.choose 2) : K) 2
rw₃ : (↑(a.choose 2) : K) = HDiv.hDiv (α := K) (↑(a.choose 2 * 2) : K) 2
rw₄ : (↑(a.choose 2) : K) = HMul.hMul (α := K) (↑(a.choose 2) : K) (↑2 : K) / 2
rw₅ : (↑(a.choose 2) : K) = HMul.hMul (α := K) (↑(a.choose 2) : K) 2 / 2
rw₆ rw₇ : HMul.hMul (α := K) (↑(a.choose 2) : K) 2 = HMul.hMul (α := K) (↑(a.choose 2) : K) 2
⊢ (↑(a.choose 2) : K) = (↑a : K) * HSub.hSub (α := K) (↑a : K) 1 / 2

Tactic:
rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
    cast_mul, cast_two, eq_div_iff_mul_eq two_ne_zero]

Premises used: Nat.cast_descFactorial_two, two_ne_zero, Nat.factorial_two, Nat.cast_mul, eq_div_iff_mul_eq, mul_comm, Nat.descFactorial_eq_factorial_mul_choose, Nat.cast_two
-- Module: Mathlib.Data.Nat.Choose.Dvd
Goal:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
⊢ p ∣ (a + b)!

Tactic:
have h₁ : p ∣ (a + b)! := hp.dvd_factorial.2 h
-- Module: Mathlib.Data.Nat.Choose.Dvd
Goal:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : p ∣ (a + b)!
⊢ (p ∣ (a + b).choose a ∨ p ≤ a) ∨ p ≤ b

Tactic:
rw [← add_choose_mul_factorial_mul_factorial, ← choose_symm_add, hp.dvd_mul, hp.dvd_mul,
    hp.dvd_factorial, hp.dvd_factorial] at h₁

Premises used: Nat.Prime.dvd_factorial, Nat.choose_symm_add, Nat.add_choose_mul_factorial_mul_factorial, Nat.Prime.dvd_mul
-- Module: Mathlib.Data.Nat.Choose.Dvd
Goal:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ (a + b).choose a ∨ p ≤ a) ∨ p ≤ b
⊢ p ∣ (a + b).choose a

Tactic:
(h₁.resolve_right hbp.not_ge).resolve_right hap.not_ge

Premises used: Or.resolve_right, LT.lt.not_ge
-- Module: Mathlib.Data.Nat.Choose.Dvd
Goal:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ (a + b).choose a ∨ p ≤ a) ∨ p ≤ b
⊢ p ∣ (a + b).choose a

Tactic:
exact (h₁.resolve_right hbp.not_ge).resolve_right hap.not_ge

Premises used: Or.resolve_right, LT.lt.not_ge
-- Module: Mathlib.Data.Nat.Choose.Dvd
Goal:
p a b : ℕ
hp : Prime p
ha : a < p
hab : b - a < p
h : p ≤ b
⊢ p ∣ b.choose a

Tactic:
have : a + (b - a) = b := Nat.add_sub_of_le (ha.le.trans h)
  this ▸ hp.dvd_choose_add ha hab (this.symm ▸ h)

Premises used: Eq.rec, Nat.add_sub_of_le, LT.lt.le, Nat.Prime.dvd_choose_add, LE.le.trans, Eq.symm
-- Module: Mathlib.Data.Nat.Choose.Dvd
Goal:
p k : ℕ
hp : Prime p
hk : k ≠ 0
hkp : k < p
⊢ p ∣ p.choose k

Tactic:
hp.dvd_choose hkp (sub_lt ((zero_le _).trans_lt hkp) <| zero_lt_of_ne_zero hk) le_rfl

Premises used: Nat.zero_le, le_rfl, Nat.Prime.dvd_choose, Nat.sub_lt, Nat.zero_lt_of_ne_zero, LE.le.trans_lt
-- Module: Mathlib.Data.Nat.Choose.Dvd
Goal:
p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
rw : p.Coprime (b.descFactorial a / a !)
⊢ p.Coprime (b.choose a)

Tactic:
rw [Nat.choose_eq_descFactorial_div_factorial]

Premises used: Nat.choose_eq_descFactorial_div_factorial
-- Module: Mathlib.Data.Nat.Choose.Dvd
Goal:
p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.descFactorial a / a !)

Tactic:
(hp.coprime_descFactorial_of_lt_of_le hb ha).coprime_div_right
    (Nat.factorial_dvd_descFactorial b a)

Premises used: Nat.Coprime.coprime_div_right, Nat.factorial_dvd_descFactorial, Nat.Prime.coprime_descFactorial_of_lt_of_le
-- Module: Mathlib.Data.Nat.Choose.Dvd
Goal:
p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.descFactorial a / a !)

Tactic:
exact (hp.coprime_descFactorial_of_lt_of_le hb ha).coprime_div_right
    (Nat.factorial_dvd_descFactorial b a)

Premises used: Nat.Coprime.coprime_div_right, Nat.factorial_dvd_descFactorial, Nat.Prime.coprime_descFactorial_of_lt_of_le
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
b : ℕ
h : log p 0 < b
⊢ Eq (α := ℕ) ((0!.factorization : (a : ℕ) → ℕ) p : ℕ) (∑ i ∈ Ico 1 b, 0 / p ^ i : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
rw :
  (((n + 1) * n !).factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₁ :
  ((n + 1).factorization + n !.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₂ :
  HAdd.hAdd (α := (a : ℕ) → ℕ) (β := (a : ℕ) → ℕ) (⇑(n + 1).factorization : (a : ℕ) → ℕ)
      (⇑n !.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₃ rw₄ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ((n + 1)!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [factorial_succ, factorization_mul (zero_ne_add_one n).symm n.factorial_ne_zero,
          coe_add, Pi.add_apply]

Premises used: Nat.factorial_succ, Nat.factorization_mul, Ne.symm, Pi.add_apply, Finsupp.coe_add, Nat.factorial_ne_zero, Nat.zero_ne_add_one
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
rw : ((n + 1).factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 b | p ^ i ∣ n + 1})
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) (((n + 1).factorization : (a : ℕ) → ℕ) p : ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) =
    #({i ∈ Ico 1 b | p ^ i ∣ n + 1}) + ∑ i ∈ Ico 1 b, n / p ^ i

Tactic:
rw [factorization_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), add_left_inj]

Premises used: Nat.le_succ, add_left_inj, LE.le.trans_lt, Nat.log_mono_right
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ((n + 1).factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 b | p ^ i ∣ n + 1})

Tactic:
apply factorization_eq_card_pow_dvd_of_lt hp (zero_lt_succ n)
          (lt_pow_of_log_lt hp.one_lt hb)

Premises used: Nat.Prime.one_lt, Nat.factorization_eq_card_pow_dvd_of_lt, Nat.zero_lt_succ, Nat.lt_pow_of_log_lt
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ #({i ∈ Ico 1 b | p ^ i ∣ n + 1}) + ∑ i ∈ Ico 1 b, n / p ^ i =
    ∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0)

Tactic:
simp [Nat.add_comm, sum_add_distrib, sum_boole]

Premises used: Finset.sum_add_distrib, Finset.sum_boole, Nat.add_comm
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n p : ℕ
hp : Prime p
⊢ HMul.hMul (β := ℕ) (p - 1) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) = n - (p.digits n).sum

Tactic:
simp only [factorization_factorial hp <| lt_succ_of_lt <| Nat.lt_add_one (log p n),
    ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range,
    ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]

Premises used: Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.factorization_factorial, Nat.lt_add_one, Finset.sum_Ico_add', Nat.Ico_zero_eq_range, Nat.lt_succ_of_lt, Nat.log, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n p : ℕ
hp : Prime p
⊢ 2 ≤ p

Tactic:
have h0 : 2 ≤ p := hp.two_le
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
⊢ 1 ≤ p * n + 1

Tactic:
have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
linarith :
  p * (n + 1) < p * n + 1 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 (↑p : ℤ) +
        ((↑p : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - (HMul.hMul (α := ℤ) (↑p : ℤ) (↑n : ℤ) + 1)) =
      0
linarith₁ : p * (n + 1) < p * n + 1 → GT.gt (α := ℤ) 2 0
⊢ p * n + 1 ≤ p * (n + 1)

Tactic:
linarith
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)

Tactic:
have h2 : p * n + 1 ≤ p * (n + 1) := by linarith
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1

Tactic:
have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by lia
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
h : ¬p ∣ m
⊢ Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
apply factorization_eq_zero_of_not_dvd

Premises used: Nat.factorization_eq_zero_of_not_dvd
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ¬p ∣ m

Tactic:
not_dvd_of_lt_of_lt_mul_succ (mem_Ico.mp hm).left (mem_Ico.mp hm).right

Premises used: Nat.not_dvd_of_lt_of_lt_mul_succ, And.right, And.left, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ¬p ∣ m

Tactic:
exact not_dvd_of_lt_of_lt_mul_succ (mem_Ico.mp hm).left (mem_Ico.mp hm).right

Premises used: Nat.not_dvd_of_lt_of_lt_mul_succ, And.right, And.left, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Choose.Factorization
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
⊢ ∀ (m : ℕ) (hm : m ∈ Ico (p * n + 1) (p * (n + 1))), Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
have h4 m (hm : m ∈ Ico (p * n + 1) (p * (n + 1))) : m.factorization p = 0 := by
    apply factorization_eq_zero_of_not_dvd
    exact not_dvd_of_lt_of_lt_mul_succ (mem_Ico.mp hm).left (mem_Ico.mp hm).right
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
⊢ ((p * 0)!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((0!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : ((p * n)!.factorization : (a : ℕ) → ℕ) p = HAdd.hAdd (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) n
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)
⊢ ((p * (n + 1))!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (((n + 1)!.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)]

Premises used: Nat.factorial_succ, Nat.factorization_mul, Ne.symm, Nat.factorial_ne_zero, Nat.factorization_factorial_mul_succ, Nat.zero_ne_add_one
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : ((p * n)!.factorization : (a : ℕ) → ℕ) p = HAdd.hAdd (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) n
⊢ 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:
ring
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
n p : ℕ
hp : Prime p
zero :
  ((p * 0)!.factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((0!.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
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)
⊢ ((p * n)!.factorization : (a : ℕ) → ℕ) p = HAdd.hAdd (α := ℕ) ((n !.factorization : (a : ℕ) → ℕ) p : ℕ) n

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

Premises used: Nat.factorial_succ, Nat.factorization_mul, Ne.symm, Nat.factorial_ne_zero, Nat.factorization_factorial_mul_succ, Nat.zero, Nat.succ, Nat.zero_ne_add_one
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
n : ℕ
rw : ∑ i ∈ Ico 1 (log p n + 1), n / p ^ i ≤ n / (p - 1)
⊢ (n !.factorization : (a : ℕ) → ℕ) p ≤ n / (p - 1)

Tactic:
rw [factorization_factorial hp (Nat.lt_add_one (log p n))]

Premises used: Nat.factorization_factorial, Nat.lt_add_one, Nat.log
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n + 1), n / p ^ i ≤ n / (p - 1)

Tactic:
Nat.geom_sum_Ico_le hp.two_le _ _

Premises used: Nat.Prime.two_le, Nat.geom_sum_Ico_le
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n + 1), n / p ^ i ≤ n / (p - 1)

Tactic:
exact Nat.geom_sum_Ico_le hp.two_le _ _

Premises used: Nat.Prime.two_le, Nat.geom_sum_Ico_le
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ Eq (α := ℕ) (∑ i ∈ Ico 1 b, n / p ^ i) (∑ i ∈ Ico 1 b, (k + (n - k)) / p ^ i)

Tactic:
simp only [add_tsub_cancel_of_le hkn]

Premises used: add_tsub_cancel_of_le
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ Eq (α := ℕ) (∑ i ∈ Ico 1 b, (k + (n - k)) / p ^ i)
    (∑ i ∈ Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0))

Tactic:
simp only [Nat.add_div (pow_pos hp.pos _)]

Premises used: pow_pos, Nat.add_div, Nat.Prime.pos
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i ∈ Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 b, k / p ^ i) (∑ i ∈ Ico 1 b, (n - k) / p ^ i) +
      #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})

Tactic:
simp [sum_add_distrib, sum_boole]

Premises used: Finset.sum_add_distrib, Finset.sum_boole
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ (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)
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ k ! * n ! ≠ 0

Tactic:
positivity
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
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)
⊢ 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:
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)]

Premises used: Nat.factorization_factorial, Nat.factorization_mul, mul_assoc, Nat.le_add_left, Nat.multiplicity_choose_aux, Pi.add_apply, Finsupp.coe_add, Nat.choose_pos, Nat.factorial_ne_zero, LE.le.trans_lt, Nat.ne_of_gt, Nat.log_mono_right
-- Module: Mathlib.Data.Nat.Choose.Factorization
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 (α := ℕ) (∑ 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:
simp only [add_tsub_cancel_right, add_comm]

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

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]
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
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 : ℕ)
⊢ (((n + k).choose k).factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})

Tactic:
Nat.add_right_cancel h₁

Premises used: Nat.add_right_cancel
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
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 : ℕ)
⊢ (((n + k).choose k).factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})

Tactic:
exact Nat.add_right_cancel h₁

Premises used: Nat.add_right_cancel
-- Module: Mathlib.Data.Nat.Choose.Factorization
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 : ℕ)
rw₁ rw₂ :
  Eq (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})

Tactic:
rw [← factorization_choose' hp ((Nat.sub_add_cancel hkn).symm ▸ hnb), Nat.sub_add_cancel hkn]

Premises used: Nat.factorization_choose', Nat.sub_add_cancel
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
a b c : ℕ
h : b ∣ c
hb : b ≠ 0
hc : c ≠ 0
obtain :
  ∀ (k : ℕ) (hc : b * k ≠ 0),
    LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a : ℕ) (((b * k).factorization : (a : ℕ) → ℕ) a : ℕ)
⊢ LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a : ℕ) ((c.factorization : (a : ℕ) → ℕ) a : ℕ)

Tactic:
obtain ⟨k, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
a b : ℕ
hb : b ≠ 0
k : ℕ
hc : b * k ≠ 0
⊢ LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a : ℕ) (((b * k).factorization : (a : ℕ) → ℕ) a : ℕ)

Tactic:
simp [factorization_mul hb (Nat.ne_zero_of_mul_ne_zero_right hc)]

Premises used: Nat.factorization_mul, Nat.ne_zero_of_mul_ne_zero_right
-- Module: Mathlib.Data.Nat.Choose.Factorization
Goal:
p n : ℕ
h : 0 ≤ n
h_1 : Ne (α := ℕ) 0 0
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n.choose 0).factorization : (a : ℕ) → ℕ) p : ℕ)
      ((factorization 0 : (a : ℕ) → ℕ) p : ℕ)

Tactic:
tauto