awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.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 ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
simp_rw :
  ∀ (hm : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤),
    HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
        (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
      ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
⊢ ∀ (hm : emultiplicity p (p * n)! ≠ ⊤),
    emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1

Tactic:
simp_rw [← prod_Ico_id_eq_factorial, Finset.emultiplicity_prod hp', ← sum_Ico_consecutive _ h1 h3,
    add_assoc]

Premises used: Finset.emultiplicity_prod, add_assoc, Finset.prod_Ico_id_eq_factorial, Finset.sum_Ico_consecutive
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.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 ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤
rw : ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
rw₁ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1
rw₂ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (emultiplicity p p + emultiplicity p (n + 1)) =
    emultiplicity p (n + 1) + 1
rw₃ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
rw₄ : ∑ x ∈ Ico (p * n + 1) (p * (n + 1)), 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
rw₅ : 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
rw₆ : 1 + emultiplicity p (n + 1) = emultiplicity p (n + 1) + 1
rw₇ rw₈ : emultiplicity p (n + 1) + 1 = emultiplicity p (n + 1) + 1
⊢ HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)

Tactic:
rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]

Premises used: Finset.sum_Ico_succ_top, zero_add, add_comm, Nat.Prime.emultiplicity_self, Finset.sum_const_zero, Nat.Prime.emultiplicity_mul, OfNat.ofNat, Finset.sum_congr, rfl, WithTop.add_left_inj
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
⊢ emultiplicity p (p * 0)! = emultiplicity p 0! + (↑0 : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
succ :
  emultiplicity p n ! + (↑n : ℕ∞) + emultiplicity p (n + 1) + 1 =
    emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞) + 1
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (n + 1)! + (↑(n + 1) : ℕ∞)

Tactic:
simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul,
      cast_add, cast_one, ← add_assoc]

Premises used: Nat.factorial_succ, add_assoc, Nat.cast_add, Nat.Prime.emultiplicity_mul, Nat.Prime.emultiplicity_factorial_mul_succ, Nat.cast_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
succ :
  emultiplicity p n ! + (↑n : ℕ∞) + emultiplicity p (n + 1) = emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞)
⊢ emultiplicity p n ! + (↑n : ℕ∞) + emultiplicity p (n + 1) + 1 =
    emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞) + 1

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
succ :
  emultiplicity p (n + 1) + (emultiplicity p n ! + (↑n : ℕ∞)) =
    emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞)
succ₁ succ₂ :
  emultiplicity p (n + 1) + (emultiplicity p n ! + (↑n : ℕ∞)) =
    emultiplicity p (n + 1) + (emultiplicity p n ! + (↑n : ℕ∞))
⊢ emultiplicity p n ! + (↑n : ℕ∞) + emultiplicity p (n + 1) = emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞)

Tactic:
rw [add_comm, add_assoc]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
zero : emultiplicity p (p * 0)! = emultiplicity p 0! + (↑0 : ℕ∞)
succ :
  ∀ (n : ℕ) (ih : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)),
    emultiplicity p (p * (n + 1))! = emultiplicity p (n + 1)! + (↑(n + 1) : ℕ∞)
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul,
      cast_add, cast_one, ← add_assoc]
    congr 1
    rw [add_comm, add_assoc]

Premises used: Nat.factorial_succ, add_assoc, add_comm, Nat.cast_add, Nat.zero, Nat.Prime.emultiplicity_mul, Nat.Prime.emultiplicity_factorial_mul_succ, Nat.succ, Nat.cast_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
rw : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
⊢ multiplicity p (p ^ n)! = ∑ i ∈ range n, p ^ i

Tactic:
rw [← ENat.coe_inj, ← (Nat.finiteMultiplicity_iff.2
      ⟨hp.ne_one, (p ^ n).factorial_pos⟩).emultiplicity_eq_multiplicity]

Premises used: Iff.mpr, FiniteMultiplicity.emultiplicity_eq_multiplicity, ENat.coe_inj, Nat.Prime.ne_one, HPow.hPow, And.intro, Nat.factorial_pos, Nat.finiteMultiplicity_iff
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
⊢ emultiplicity p (HPow.hPow (β := ℕ) p 0)! = (↑(∑ i ∈ range 0, p ^ i) : ℕ∞)

Tactic:
simp [hp.emultiplicity_one]

Premises used: Nat.Prime.emultiplicity_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
succ : emultiplicity p (p * p ^ n)! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
succ₁ : emultiplicity p (p ^ n)! + (↑(p ^ n) : ℕ∞) = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
succ₂ : HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ range n, p ^ i) : ℕ∞) (↑(p ^ n) : ℕ∞) = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
succ₃ : HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ range n, p ^ i) : ℕ∞) (↑(p ^ n) : ℕ∞) = (↑(∑ x ∈ range n, p ^ x + p ^ n) : ℕ∞)
succ₄ succ₅ :
  HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ range n, p ^ i) : ℕ∞) (↑(p ^ n) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(∑ x ∈ range n, p ^ x) : ℕ∞) (↑(p ^ n) : ℕ∞)
⊢ emultiplicity p (p ^ (n + 1))! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)

Tactic:
rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]

Premises used: Nat.pow_succ', Nat.Prime.emultiplicity_factorial_mul, ENat.coe_add, Finset.sum_range_succ
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
zero : emultiplicity p (HPow.hPow (β := ℕ) p 0)! = (↑(∑ i ∈ range 0, p ^ i) : ℕ∞)
succ :
  ∀ (n : ℕ) (h : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)),
    emultiplicity p (p ^ (n + 1))! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
⊢ emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)

Tactic:
induction n with
  | zero => simp [hp.emultiplicity_one]
  | succ n h =>
    rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]

Premises used: Nat.pow_succ', Nat.Prime.emultiplicity_factorial_mul, Nat.Prime.emultiplicity_one, Nat.zero, Nat.succ, ENat.coe_add, Finset.sum_range_succ
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n r b : ℕ
hp : Prime p
hbn : log p n < b
rw : p ^ r ∣ n ! ↔ (↑r : WithTop ℕ) ≤ (↑(∑ i ∈ Ico 1 b, n / p ^ i) : WithTop ℕ)
rw₁ : p ^ r ∣ n ! ↔ LE.le (α := WithTop ℕ) (↑r : WithTop ℕ) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : WithTop ℕ)
rw₂ : p ^ r ∣ n ! ↔ (↑r : WithTop ℕ) ≤ emultiplicity p n !
rw₃ rw₄ : (↑r : ℕ∞) ≤ emultiplicity p n ! ↔ (↑r : WithTop ℕ) ≤ emultiplicity p n !
⊢ p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i

Tactic:
rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hp.emultiplicity_factorial hbn,
    pow_dvd_iff_le_emultiplicity]

Premises used: ENat.some_eq_coe, Nat.Prime.emultiplicity_factorial, pow_dvd_iff_le_emultiplicity, WithTop.coe_le_coe
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n : ℕ
rw : LE.le (α := ℕ∞) (↑(∑ i ∈ Ico 1 (log p n).succ, n / p ^ i) : ℕ∞) (↑(n / (p - 1)) : ℕ∞)
⊢ emultiplicity p n ! ≤ (↑(n / (p - 1)) : ℕ∞)

Tactic:
rw [hp.emultiplicity_factorial (lt_succ_self _)]

Premises used: Nat.Prime.emultiplicity_factorial, Nat.lt_succ_self
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n : ℕ
a : ∑ i ∈ Ico 1 (log p n).succ, n / p ^ i ≤ n / (p - 1)
⊢ LE.le (α := ℕ∞) (↑(∑ i ∈ Ico 1 (log p n).succ, n / p ^ i) : ℕ∞) (↑(n / (p - 1)) : ℕ∞)

Tactic:
apply WithTop.coe_mono

Premises used: WithTop.coe_mono
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n).succ, 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.Multiplicity
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n).succ, 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.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
rw :
  emultiplicity p ((n + k).choose k * k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
⊢ emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)

Tactic:
rw [← hp.emultiplicity_mul, ← mul_assoc]

Premises used: mul_assoc, Nat.Prime.emultiplicity_mul
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ (n + k).choose k * k ! * n ! = (n + k)!

Tactic:
have := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (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) : ℕ∞)
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)

Tactic:
rw [this, hp.emultiplicity_factorial hnb, hp.emultiplicity_mul,
      hp.emultiplicity_factorial ((log_mono_right (le_add_left k n)).trans_lt hnb),
      hp.emultiplicity_factorial ((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.Prime.emultiplicity_factorial, Nat.le_add_left, Nat.multiplicity_choose_aux, Nat.Prime.emultiplicity_mul, LE.le.trans_lt, Nat.log_mono_right
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (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 [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)

Tactic:
have h₁ :
      emultiplicity p (choose (n + k) k) + emultiplicity p (k ! * n !) =
        #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i} + emultiplicity p (k ! * n !) := by
    rw [← hp.emultiplicity_mul, ← mul_assoc]
    have := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
    rw [this, hp.emultiplicity_factorial hnb, hp.emultiplicity_mul,
      hp.emultiplicity_factorial ((log_mono_right (le_add_left k n)).trans_lt hnb),
      hp.emultiplicity_factorial ((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 [add_comm]
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
⊢ emultiplicity p ((n + k).choose k) = (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞)

Tactic:
WithTop.add_right_cancel ?_ h₁

Premises used: WithTop.add_right_cancel, ENat
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
refine : emultiplicity p (k ! * n !) ≠ ⊤
⊢ emultiplicity p ((n + k).choose k) = (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞)

Tactic:
refine WithTop.add_right_cancel ?_ h₁

Premises used: WithTop.add_right_cancel
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
apply : FiniteMultiplicity p (k ! * n !)
⊢ emultiplicity p (k ! * n !) ≠ ⊤

Tactic:
apply finiteMultiplicity_iff_emultiplicity_ne_top.1

Premises used: finiteMultiplicity_iff_emultiplicity_ne_top, Iff.mp
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
⊢ FiniteMultiplicity p (k ! * n !)

Tactic:
Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, mul_pos (factorial_pos k) (factorial_pos n)⟩

Premises used: Iff.mpr, mul_pos, Nat.Prime.ne_one, And.intro, Nat.factorial_pos, Nat.finiteMultiplicity_iff
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
⊢ FiniteMultiplicity p (k ! * n !)

Tactic:
exact Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, mul_pos (factorial_pos k) (factorial_pos n)⟩

Premises used: Iff.mpr, mul_pos, Nat.Prime.ne_one, And.intro, Nat.factorial_pos, Nat.finiteMultiplicity_iff
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ n - k + k = n

Tactic:
have := Nat.sub_add_cancel hkn
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ emultiplicity p ((n - k + k).choose k) = (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})) : ℕ∞)

Tactic:
@emultiplicity_choose' p (n - k) k b hp _

Premises used: Nat.Prime.emultiplicity_choose'
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
h : n = n - k + k
convert! : log p (n - k + k) < b
⊢ emultiplicity p (n.choose k) = (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})) : ℕ∞)

Tactic:
convert! @emultiplicity_choose' p (n - k) k b hp _

Premises used: Nat.Prime.emultiplicity_choose'
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
h h₁ : n = n
⊢ n = n - k + k

Tactic:
rw [this]
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ log p (n - k + k) < b

Tactic:
this.symm ▸ hnb

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ log p (n - k + k) < b

Tactic:
exact this.symm ▸ hnb
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
x : ℕ
⊢ emultiplicity p x ≤ emultiplicity p (x.choose 0) + emultiplicity p 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ emultiplicity p 0 ≤ emultiplicity p (choose 0 (n + 1)) + emultiplicity p (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n k : ℕ
rw : emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1) * (k + 1))
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1)) + emultiplicity p (k + 1)

Tactic:
rw [← hp.emultiplicity_mul]

Premises used: Nat.Prime.emultiplicity_mul
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1) * (k + 1))

Tactic:
emultiplicity_le_emultiplicity_of_dvd_right ?_

Premises used: emultiplicity_le_emultiplicity_of_dvd_right
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n k : ℕ
refine : n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1) * (k + 1))

Tactic:
refine emultiplicity_le_emultiplicity_of_dvd_right ?_

Premises used: emultiplicity_le_emultiplicity_of_dvd_right
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n k : ℕ
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.Multiplicity
Goal:
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ (n + 1) * n.choose k

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ (n + 1) * n.choose k

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ 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 [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.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ 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 [disjoint_right, *, dvd_iff_mod_eq_zero,
          Nat.mod_lt _ (pow_pos hp.pos _)]
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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})
rw :
  LE.le (α := ℕ∞)
    (↑(#({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) +
          #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ∣ k})) :
      ℕ∞)
    (↑n : ℕ∞)
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ (↑n : ℕ∞)

Tactic:
rw [emultiplicity_choose hp hkn (lt_succ_self _),
        emultiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt
          (lt_succ_of_le (log_mono_right hkn)),
        ← Nat.cast_add]

Premises used: Nat.Prime.one_lt, Nat.lt_succ_self, Nat.Prime.emultiplicity_choose, Nat.lt_succ_of_le, Nat.cast_add, Nat.emultiplicity_eq_card_pow_dvd, Ne.bot_lt, Nat.ne_of_gt, Nat.log_mono_right
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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})
a :
  #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) +
      #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ∣ k}) ≤
    n
⊢ LE.le (α := ℕ∞)
    (↑(#({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) +
          #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ∣ k})) :
      ℕ∞)
    (↑n : ℕ∞)

Tactic:
apply WithTop.coe_mono

Premises used: WithTop.coe_mono
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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})
a : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
⊢ #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) +
      #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ∣ k}) ≤
    n

Tactic:
rw [log_pow hp.one_lt, ← card_union_of_disjoint hdisj, filter_union_right]

Premises used: Nat.Prime.one_lt, Finset.filter_union_right, Nat.log_pow, Finset.card_union_of_disjoint
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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})
⊢ #({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.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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})
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.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
rw : emultiplicity p (p ^ n) ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k
⊢ (↑n : ℕ∞) ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k

Tactic:
rw [← hp.emultiplicity_pow_self]

Premises used: Nat.Prime.emultiplicity_pow_self
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p (p ^ n) ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k

Tactic:
emultiplicity_le_emultiplicity_choose_add hp _ _

Premises used: Nat.Prime.emultiplicity_le_emultiplicity_choose_add
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p (p ^ n) ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k

Tactic:
exact emultiplicity_le_emultiplicity_choose_add hp _ _

Premises used: Nat.Prime.emultiplicity_le_emultiplicity_choose_add
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
rw :
  (↑(multiplicity p ((p ^ n).choose k)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(multiplicity p ((p ^ n).choose k)) : ℕ∞) (↑(multiplicity p k) : ℕ∞) -
      (↑(multiplicity p k) : ℕ∞)
⊢ emultiplicity p ((p ^ n).choose k) = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity p k) : ℕ∞)

Tactic:
rw [← emultiplicity_choose_prime_pow_add_emultiplicity hp hkn hk0,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, Nat.pos_of_ne_zero hk0⟩).emultiplicity_eq_multiplicity,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, choose_pos hkn⟩).emultiplicity_eq_multiplicity]

Premises used: Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicity, Iff.mpr, FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.choose_pos, Nat.pos_of_ne_zero, Nat.Prime.ne_one, And.intro, Nat.finiteMultiplicity_iff