awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hp : Prime p
mp : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n → n = 0 ∨ ¬p ∣ n
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n ↔ n = 0 ∨ ¬p ∣ n
have mpr : n = 0 ∨ ¬p ∣ n → n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hp : Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
⊢ n = 0 ∨ ¬p ∣ n
have pos : ∀ (n_zero : n = 0), n = 0 ∨ ¬p ∣ n
Tactic: by_cases n_zero : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
⊢ n = 0 ∨ ¬p ∣ n
have neg : ∀ (n_zero : ¬n = 0), n = 0 ∨ ¬p ∣ n
Tactic: by_cases n_zero : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hp : Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n
have neg : ¬p ∣ n
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hp : Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
n_zero : ¬n = 0
⊢ ¬p ∣ n
have neg : ¬p ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ) = m
have rw : m / HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) = m
Tactic: rw [ordCompl_self_pow_mul m k hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
k m p : ℕ
hp : Prime p
⊢ p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ) = m ↔ m = 0 ∨ ¬p ∣ m
have rw : m / HPow.hPow (β := ℕ) p ((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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
k m p : ℕ
hp : Prime p
rw : m / HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) = m ↔ m = 0 ∨ ¬p ∣ m
⊢ p ^ k * m / HPow.hPow (β := ℕ) p (((p ^ k * m).factorization : (a : ℕ) → ℕ) p : ℕ) = m ↔ m = 0 ∨ ¬p ∣ m
have rw₁ : m = 0 ∨ ¬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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
k x p : ℕ
hp : Prime p
hx : p ^ k ∣ x
⊢ x / p ^ k / HPow.hPow (β := ℕ) p (((x / p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) =
    x / HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)
have 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 : ℕ)
Tactic: obtain ⟨m, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
k p : ℕ
hp : Prime p
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 : ℕ)
have rw : m / HPow.hPow (β := ℕ) p ((m.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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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 : ℕ)
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: rw [Nat.mul_div_cancel_left m (pow_pos hp.pos k), ← ordCompl_self_pow_mul m k hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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 : ℕ)
have rw : d.factorization ≤ Finsupp.erase p n.factorization
Tactic: rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
⊢ LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) q : ℕ) ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
have if : ∀ (hqp : q = p),
  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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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 : ℕ)
⊢ LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) q : ℕ) ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
have if₁ : ∀ (hqp : ¬q = p),
  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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
⊢ d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have if : ∀ (hd0 : d = 0), 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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 : ℕ)
⊢ d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have if₁ : ∀ (hd0 : ¬d = 0), 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
⊢ d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have if : ∀ (hn0 : n = 0), 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
if : ∀ (hn0 : n = 0), d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ d ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have if₁ : ∀ (hn0 : ¬n = 0), 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization
have refine : (n / d).factorization = n.factorization - d.factorization → d ∣ n
Tactic: refine ⟨factorization_div, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n
have inl : ∀ (hdn : d ≤ d), (d / d).factorization = d.factorization - d.factorization → d ∣ d
Tactic: rcases eq_or_lt_of_le hdn with (rfl | hd_lt_n)
Cleared hypotheses: n, hdn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
inl : ∀ (hdn : d ≤ d), (d / d).factorization = d.factorization - d.factorization → d ∣ d
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n
have inr : ∀ (hd_lt_n : d < n), (n / d).factorization = n.factorization - d.factorization → d ∣ n
Tactic: rcases eq_or_lt_of_le hdn with (rfl | hd_lt_n)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n
have h1 : n / d ≠ 0
Tactic: have h1 : n / d ≠ 0 := by simp [*]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
⊢ d ∣ n
have inr : n ≤ n / d * d
Tactic: rw [dvd_iff_le_div_mul n d]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
⊢ n ≤ n / d * d
have inr : ∀ (h2 : ¬n ≤ n / d * d), False
Tactic: by_contra h2
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
⊢ False
have inr : ∀ (p : ℕ)
  (hp : LT.lt (α := ℕ) (((n / d * d).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)), False
Tactic: obtain ⟨p, hp⟩ := exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
p : ℕ
hp : LT.lt (α := ℕ) (((n / d * d).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ False
have inr : ∀
  (hp :
    LT.lt (α := ℕ) (((n / d).factorization + d.factorization : (a : ℕ) → ℕ) p : ℕ)
      ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
  False
Tactic: rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
    lt_self_iff_false] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
p : ℕ
hp : LT.lt (α := ℕ) (((n / d * d).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
inr :
  ∀
    (hp :
      LT.lt (α := ℕ) (((n / d).factorization + d.factorization : (a : ℕ) → ℕ) p : ℕ)
        ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
⊢ False
have inr₁ : ∀
  (hp :
    HAdd.hAdd (α := ℕ) (β := ℕ) (((n / d).factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) <
      (n.factorization : (a : ℕ) → ℕ) p),
  False
Tactic: rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
    lt_self_iff_false] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
p : ℕ
hp : LT.lt (α := ℕ) (((n / d * d).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
inr :
  ∀
    (hp :
      LT.lt (α := ℕ) (((n / d).factorization + d.factorization : (a : ℕ) → ℕ) p : ℕ)
        ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
inr₁ :
  ∀
    (hp :
      HAdd.hAdd (α := ℕ) (β := ℕ) (((n / d).factorization : (a : ℕ) → ℕ) p : ℕ)
          ((d.factorization : (a : ℕ) → ℕ) p : ℕ) <
        (n.factorization : (a : ℕ) → ℕ) p),
    False
⊢ False
have inr₂ : ∀
  (hp :
    ((n / d).factorization : (a : ℕ) → ℕ) p <
      HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ)),
  False
Tactic: rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
    lt_self_iff_false] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
p : ℕ
hp : LT.lt (α := ℕ) (((n / d * d).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
inr :
  ∀
    (hp :
      LT.lt (α := ℕ) (((n / d).factorization + d.factorization : (a : ℕ) → ℕ) p : ℕ)
        ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
inr₁ :
  ∀
    (hp :
      HAdd.hAdd (α := ℕ) (β := ℕ) (((n / d).factorization : (a : ℕ) → ℕ) p : ℕ)
          ((d.factorization : (a : ℕ) → ℕ) p : ℕ) <
        (n.factorization : (a : ℕ) → ℕ) p),
    False
inr₂ :
  ∀
    (hp :
      ((n / d).factorization : (a : ℕ) → ℕ) p <
        HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
⊢ False
have inr₃ : ∀
  (hp :
    (n.factorization - d.factorization : (a : ℕ) → ℕ) p <
      HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ)),
  False
Tactic: rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
    lt_self_iff_false] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
p : ℕ
hp : LT.lt (α := ℕ) (((n / d * d).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
inr :
  ∀
    (hp :
      LT.lt (α := ℕ) (((n / d).factorization + d.factorization : (a : ℕ) → ℕ) p : ℕ)
        ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
inr₁ :
  ∀
    (hp :
      HAdd.hAdd (α := ℕ) (β := ℕ) (((n / d).factorization : (a : ℕ) → ℕ) p : ℕ)
          ((d.factorization : (a : ℕ) → ℕ) p : ℕ) <
        (n.factorization : (a : ℕ) → ℕ) p),
    False
inr₂ :
  ∀
    (hp :
      ((n / d).factorization : (a : ℕ) → ℕ) p <
        HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
inr₃ :
  ∀
    (hp :
      (n.factorization - d.factorization : (a : ℕ) → ℕ) p <
        HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
⊢ False
have inr₄ : ∀
  (hp :
    HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) <
      HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ)),
  False
Tactic: rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
    lt_self_iff_false] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
p : ℕ
hp : LT.lt (α := ℕ) (((n / d * d).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
inr :
  ∀
    (hp :
      LT.lt (α := ℕ) (((n / d).factorization + d.factorization : (a : ℕ) → ℕ) p : ℕ)
        ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
inr₁ :
  ∀
    (hp :
      HAdd.hAdd (α := ℕ) (β := ℕ) (((n / d).factorization : (a : ℕ) → ℕ) p : ℕ)
          ((d.factorization : (a : ℕ) → ℕ) p : ℕ) <
        (n.factorization : (a : ℕ) → ℕ) p),
    False
inr₂ :
  ∀
    (hp :
      ((n / d).factorization : (a : ℕ) → ℕ) p <
        HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
inr₃ :
  ∀
    (hp :
      (n.factorization - d.factorization : (a : ℕ) → ℕ) p <
        HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
inr₄ :
  ∀
    (hp :
      HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) <
        HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ)),
    False
⊢ False
have inr₅ : ∀ (hp : False), False
Tactic: rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
    lt_self_iff_false] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
⊢ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inl : ∀ (pp : ¬Prime p),
  HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases em' p.Prime with (pp | pp)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
inl :
  ∀ (pp : ¬Prime p),
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : ∀ (pp : Prime p),
  HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases em' p.Prime with (pp | pp)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : ∀ (hab : 0 ∣ b),
  HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases eq_or_ne a 0 with (rfl | ha0)
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
inr :
  ∀ (hab : 0 ∣ b),
    HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) ∣
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr₁ : ∀ (ha0 : a ≠ 0),
  HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases eq_or_ne a 0 with (rfl | ha0)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [pow_dvd_pow_iff_le_right pp.one_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inl : ∀ (pp : ¬Prime p),
  a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases em' p.Prime with (pp | pp)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
inl :
  ∀ (pp : ¬Prime p),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : ∀ (pp : Prime p),
  a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases em' p.Prime with (pp | pp)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : ∀ (hab : a ∣ 0),
  a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    0 / HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases eq_or_ne b 0 with (rfl | hb0)
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
inr :
  ∀ (hab : a ∣ 0),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      0 / HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ)
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr₁ : ∀ (hb0 : b ≠ 0),
  a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases eq_or_ne b 0 with (rfl | hb0)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : ∀ (hab : 0 ∣ b),
  0 / HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases eq_or_ne a 0 with (rfl | ha0)
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
inr :
  ∀ (hab : 0 ∣ b),
    0 / HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr₁ : ∀ (ha0 : a ≠ 0),
  a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases eq_or_ne a 0 with (rfl | ha0)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have ha : a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
Tactic: have ha := (Nat.div_pos (ordProj_le p ha0) (ordProj_pos a p)).ne'