awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
inr : (n / d).factorization + d.factorization = n.factorization
inr₁ : (n / d * d).factorization = n.factorization
inr₂ inr₃ : n.factorization = n.factorization
⊢ (n / d).factorization + d.factorization = n.factorization - d.factorization + d.factorization

Tactic:
rw [tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h, ←
    Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,
    Nat.div_mul_cancel h]

Premises used: Iff.mpr, Nat.div_mul_cancel, Nat.factorization_mul, tsub_add_cancel_of_le, LT.lt.ne', Nat.factorization_le_iff_dvd, Nat.le_of_dvd, Nat.div_pos, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
pp : Prime p
h : p ∣ n
⊢ p ∣ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
dvd_pow_self p (Prime.factorization_pos_of_dvd pp hn h).ne'

Premises used: Nat.Prime.factorization_pos_of_dvd, dvd_pow_self, LT.lt.ne'
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
hn : n ≠ 0
rw :
  ¬LE.le (α := ℕ) (1 : ℕ)
      (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ¬p ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [Nat.Prime.dvd_iff_one_le_factorization hp (ordCompl_pos p hn).ne']

Premises used: Nat.Prime.dvd_iff_one_le_factorization, LT.lt.ne', Nat.ordCompl_pos
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
hn : n ≠ 0
rw :
  ¬LE.le (α := ℕ) (1 : ℕ)
      ((n.factorization - (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ)
          p :
        ℕ)
⊢ ¬LE.le (α := ℕ) (1 : ℕ)
      (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [Nat.factorization_div (Nat.ordProj_dvd n p)]

Premises used: Nat.factorization_div, Nat.ordProj_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬LE.le (α := ℕ) (1 : ℕ)
      ((n.factorization - (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ)
          p :
        ℕ)

Tactic:
simp [hp.factorization]

Premises used: Nat.Prime.factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ p.Coprime (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
(or_iff_left (not_dvd_ordCompl hp hn)).mp <| coprime_or_dvd_of_prime hp _

Premises used: Nat.not_dvd_ordCompl, Iff.mp, or_iff_left, Nat.coprime_or_dvd_of_prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n = 0
⊢ (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : ¬n = 0
pp : ¬Prime p
⊢ (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization

Tactic:
simp [pp]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : ¬n = 0
⊢ Prime p

Tactic:
if pp : p.Prime then ?_ else
    simp [pp]

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : ¬n = 0
pp : Prime p
h :
  ∀ (q : ℕ),
    Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
      ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization

Tactic:
ext q
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
h :
  ∀ (pp : Prime q),
    Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) q ((n.factorization : (a : ℕ) → ℕ) q : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
      ((Finsupp.erase q n.factorization : (a : ℕ) → ℕ) q : ℕ)
h₁ :
  ∀ (hqp : q ≠ p),
    Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
      ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
rcases eq_or_ne q p with (rfl | hqp)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
h : ¬Prime q ∨ ¬False ∨ n / HPow.hPow (β := ℕ) q ((n.factorization : (a : ℕ) → ℕ) q : ℕ) = 0
⊢ Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) q ((n.factorization : (a : ℕ) → ℕ) q : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase q n.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]

Premises used: Finsupp.erase_same, Nat.not_dvd_ordCompl, Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ ¬Prime q ∨ ¬False ∨ n / HPow.hPow (β := ℕ) q ((n.factorization : (a : ℕ) → ℕ) q : ℕ) = 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
h :
  Eq (α := ℕ)
    ((n.factorization - (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q :
      ℕ)
    ((n.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]

Premises used: Finsupp.erase_ne, Nat.factorization_div, Nat.ordProj_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ Eq (α := ℕ)
    ((n.factorization - (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q :
      ℕ)
    ((n.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
simp [pp.factorization, hqp.symm]

Premises used: Nat.Prime.factorization, Ne.symm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
if :
  ∀ (hn : n = 0),
    (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization
if₁ :
  ∀ (hn : ¬n = 0),
    (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization
if₂ :
  ∀ (hn : n = 0),
    (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization
if₃ if₄ :
  ∀ (hn : ¬n = 0),
    (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization
⊢ (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization

Tactic:
if hn : n = 0 then simp [hn] else
  if pp : p.Prime then ?_ else
    simp [pp]
  ext q
  rcases eq_or_ne q p with (rfl | hqp)
  · simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]
    simp
  · rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]
    simp [pp.factorization, hqp.symm]

Premises used: Finsupp.erase_same, Nat.Prime, Nat.factorization_div, Nat.ordProj_dvd, Nat.factorization_eq_zero_iff, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p k : ℕ
hp : Prime p
⊢ HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) = p ^ k

Tactic:
simp [hp]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p k : ℕ
hp : Prime p
ha : p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
hb : Ne (α := ℕ) 1 0
h :
  ∀ (p_1 : ℕ),
    Eq (α := ℕ)
      (((p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) p_1 :
        ℕ)
      ((factorization 1 : (a : ℕ) → ℕ) p_1 : ℕ)
⊢ p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
apply Nat.eq_of_factorization_eq

Premises used: Nat.eq_of_factorization_eq
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p k : ℕ
hp : Prime p
⊢ p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0

Tactic:
pos_iff_ne_zero.mp (ordCompl_pos p (pow_ne_zero k hp.ne_zero))

Premises used: pow_ne_zero, Nat.ordCompl_pos, Nat.Prime.ne_zero, Iff.mp, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p k : ℕ
hp : Prime p
⊢ p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0

Tactic:
exact pos_iff_ne_zero.mp (ordCompl_pos p (pow_ne_zero k hp.ne_zero))

Premises used: pow_ne_zero, Nat.ordCompl_pos, Nat.Prime.ne_zero, Iff.mp, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p k : ℕ
hp : Prime p
⊢ Ne (α := ℕ) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p k : ℕ
hp : Prime p
⊢ Ne (α := ℕ) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p k : ℕ
hp : Prime p
⊢ ∀ (p_1 : ℕ),
    Eq (α := ℕ)
      (((p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) p_1 :
        ℕ)
      ((factorization 1 : (a : ℕ) → ℕ) p_1 : ℕ)

Tactic:
simp [Prime.factorization_pow hp]

Premises used: Nat.Prime.factorization_pow
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n k p : ℕ
hp : Prime p
rw :
  p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) *
      (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₁ :
  1 * (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₂ rw₃ :
  n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) =
    n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ p ^ k * n / HPow.hPow (β := ℕ) p (((p ^ k * n).factorization : (a : ℕ) → ℕ) p : ℕ) =
    n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [ordCompl_mul, ordCompl_self_pow hp, one_mul]

Premises used: Nat.ordCompl_mul, one_mul, Nat.ordCompl_self_pow
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
mp : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n → n = 0 ∨ ¬p ∣ n
mpr : n = 0 ∨ ¬p ∣ n → n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n ↔ n = 0 ∨ ¬p ∣ n

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
pos : ∀ (n_zero : n = 0), n = 0 ∨ ¬p ∣ n
neg : ∀ (n_zero : ¬n = 0), n = 0 ∨ ¬p ∣ n
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
by_cases n_zero : n = 0
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
n_zero : n = 0
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
simp [n_zero]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
n_zero : ¬n = 0
neg : ¬p ∣ n
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
n_zero : ¬n = 0
neg : ¬p ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ¬p ∣ n

Tactic:
rw [← h]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
n_zero : ¬n = 0
⊢ ¬p ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
not_dvd_ordCompl hp n_zero

Premises used: Nat.not_dvd_ordCompl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
n_zero : ¬n = 0
⊢ ¬p ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
exact not_dvd_ordCompl hp n_zero

Premises used: Nat.not_dvd_ordCompl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
n_eq_zero : n = 0
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n

Tactic:
simp [n_eq_zero]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : Prime p
not_dvd : ¬p ∣ n
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n

Tactic:
simp [Nat.factorization_eq_zero_of_not_dvd not_dvd]

Premises used: Nat.factorization_eq_zero_of_not_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
rw : m / HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) = m
⊢ p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ) = m

Tactic:
rw [ordCompl_self_pow_mul m k hp]

Premises used: Nat.ordCompl_self_pow_mul
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ m / HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) = m

Tactic:
(ordCompl_eq_self_iff_zero_or_not_dvd m hp).mpr (Or.inr hm)

Premises used: Iff.mpr, Nat.ordCompl_eq_self_iff_zero_or_not_dvd, Or.inr
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ m / HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) = m

Tactic:
exact (ordCompl_eq_self_iff_zero_or_not_dvd m hp).mpr (Or.inr hm)

Premises used: Iff.mpr, Nat.ordCompl_eq_self_iff_zero_or_not_dvd, Or.inr
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
k m p : ℕ
hp : Prime p
rw : m / HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) = m ↔ m = 0 ∨ ¬p ∣ m
rw₁ rw₂ : m = 0 ∨ ¬p ∣ m ↔ m = 0 ∨ ¬p ∣ m
⊢ p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ) = m ↔ m = 0 ∨ ¬p ∣ m

Tactic:
rw [ordCompl_self_pow_mul m k hp, ordCompl_eq_self_iff_zero_or_not_dvd m hp]

Premises used: Nat.ordCompl_self_pow_mul, Nat.ordCompl_eq_self_iff_zero_or_not_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
k x p : ℕ
hp : Prime p
hx : p ^ k ∣ x
obtain :
  ∀ (m : ℕ),
    p ^ k * m / p ^ k / HPow.hPow (β := ℕ) p (((p ^ k * m / p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) =
      p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ x / p ^ k / HPow.hPow (β := ℕ) p (((x / p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) =
    x / HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
obtain ⟨m, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
k p : ℕ
hp : Prime p
m : ℕ
rw :
  m / HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) =
    p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ)
rw₁ rw₂ :
  p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ) =
    p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ p ^ k * m / p ^ k / HPow.hPow (β := ℕ) p (((p ^ k * m / p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) =
    p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [Nat.mul_div_cancel_left m (pow_pos hp.pos k), ← ordCompl_self_pow_mul m k hp]

Premises used: pow_pos, Nat.mul_div_cancel_left, Nat.Prime.pos, Nat.ordCompl_self_pow_mul
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
x p : ℕ
hp : Prime p
hx : p ∣ x
⊢ HPow.hPow (β := ℕ) p 1 ∣ x

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
x p : ℕ
hp : Prime p
hx : p ∣ x
⊢ x / p / HPow.hPow (β := ℕ) p (((x / p).factorization : (a : ℕ) → ℕ) p : ℕ) =
    x / HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simpa [pow_one] using ordCompl_div_pow_of_dvd 1 hp (show p ^ 1 ∣ x by simpa)

Premises used: pow_one, Nat.ordCompl_div_pow_of_dvd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n = 0
⊢ d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [hn0]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : d = 0
⊢ d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [hd0] at hpd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
rw : d.factorization ≤ Finsupp.erase p n.factorization
⊢ d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]

Premises used: LT.lt.ne', Nat.factorization_le_iff_dvd, Nat.ordCompl_pos, Nat.factorization_ordCompl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
hqp : q = p
⊢ LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) q : ℕ) ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
simp [factorization_eq_zero_iff, hqp, hpd]

Premises used: Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
hqp : ¬q = p
⊢ LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) q : ℕ) ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

Premises used: Iff.mpr, Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
if :
  ∀ (hqp : q = p),
    LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) q : ℕ) ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
if₁ :
  ∀ (hqp : ¬q = p),
    LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) q : ℕ) ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
if₂ :
  ∀ (hqp : q = p),
    LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) q : ℕ) ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
if₃ if₄ :
  ∀ (hqp : ¬q = p),
    LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) q : ℕ) ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) q : ℕ) ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
if hqp : q = p then
    simp [factorization_eq_zero_iff, hqp, hpd]
  else
    simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

Premises used: Iff.mpr, Nat.factorization_le_iff_dvd, Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
if : ∀ (hd0 : d = 0), d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₁ : ∀ (hd0 : ¬d = 0), d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₂ : ∀ (hd0 : d = 0), d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₃ if₄ : ∀ (hd0 : ¬d = 0), d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
if hd0 : d = 0 then simp [hd0] at hpd else
  rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
  intro q
  if hqp : q = p then
    simp [factorization_eq_zero_iff, hqp, hpd]
  else
    simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

Premises used: Nat.factorization_ordCompl, Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
if : ∀ (hn0 : n = 0), d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₁ : ∀ (hn0 : ¬n = 0), d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₂ : ∀ (hn0 : n = 0), d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₃ if₄ : ∀ (hn0 : ¬n = 0), d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
if hn0 : n = 0 then simp [hn0] else
  if hd0 : d = 0 then simp [hd0] at hpd else
  rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
  intro q
  if hqp : q = p then
    simp [factorization_eq_zero_iff, hqp, hpd]
  else
    simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

Premises used: Nat.factorization_ordCompl, Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ≠ 1
⊢ ∃ (e : ℕ) (n' : ℕ), ¬p ∣ n' ∧ n = p ^ e * n'

Tactic:
let ⟨a', h₁, h₂⟩ :=
    (Nat.finiteMultiplicity_iff.mpr ⟨hp, Nat.pos_of_ne_zero hn⟩).exists_eq_pow_mul_and_not_dvd
  ⟨_, a', h₂, h₁⟩

Premises used: Iff.mpr, Dvd.dvd, HMul.hMul, FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd, Exists, multiplicity, And, Nat.pos_of_ne_zero, HPow.hPow, And.intro, Exists.intro, _private.0.Nat.exists_eq_pow_mul_and_not_dvd.match_1, Eq, Not, Nat.finiteMultiplicity_iff
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ ∃ (k : ℕ) (m : ℕ), Odd m ∧ n = HPow.hPow (α := ℕ) 2 k * m

Tactic:
let ⟨k, m, hm, hn⟩ := exists_eq_pow_mul_and_not_dvd hn 2 (succ_ne_self 1)
  ⟨k, m, not_even_iff_odd.1 (mt Even.two_dvd hm), hn⟩

Premises used: _private.0.Nat.exists_eq_two_pow_mul_odd.match_1, HMul.hMul, Odd, Nat.succ_ne_self, Exists, mt, Nat.not_even_iff_odd, And, HPow.hPow, Even.two_dvd, And.intro, Exists.intro, Iff.mp, Nat.exists_eq_pow_mul_and_not_dvd, OfNat.ofNat, Eq
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization

Tactic:
⟨factorization_div, ?_⟩

Premises used: Iff.intro, Nat.factorization_div
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
refine : (n / d).factorization = n.factorization - d.factorization → d ∣ n
⊢ d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization

Tactic:
refine ⟨factorization_div, ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
inl : ∀ (hdn : d ≤ d), (d / d).factorization = d.factorization - d.factorization → d ∣ d
inr : ∀ (hd_lt_n : d < n), (n / d).factorization = n.factorization - d.factorization → d ∣ n
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n

Tactic:
rcases eq_or_lt_of_le hdn with (rfl | hd_lt_n)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d : ℕ
hd : d ≠ 0
hdn : d ≤ d
⊢ (d / d).factorization = d.factorization - d.factorization → d ∣ d

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ n / d ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ n / d ≠ 0

Tactic:
have h1 : n / d ≠ 0 := by simp [*]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
inr : n ≤ n / d * d
⊢ d ∣ n

Tactic:
rw [dvd_iff_le_div_mul n d]

Premises used: Nat.dvd_iff_le_div_mul
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
inr : ∀ (h2 : ¬n ≤ n / d * d), False
⊢ n ≤ n / d * d

Tactic:
by_contra h2
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
h2 : ¬n ≤ n / d * d
inr :
  ∀ (p : ℕ)
    (hp : LT.lt (α := ℕ) (((n / d * d).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
⊢ False

Tactic:
obtain ⟨p, hp⟩ := exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2)

Premises used: not_le, Nat.exists_factorization_lt_of_lt, Iff.mp, mul_ne_zero