awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b /
      (HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
have rw : a * b /
    (HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) =
  a * b /
    (HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
Tactic: rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b p : ℕ
ha : ¬a = 0
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
have if : ∀ (hb : b = 0),
  a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
Tactic: if hb : b = 0 then simp [hb] else
  simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b p : ℕ
ha : ¬a = 0
if :
  ∀ (hb : b = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
have if₁ : ∀ (hb : ¬b = 0),
  a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
Tactic: if hb : b = 0 then simp [hb] else
  simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b p : ℕ
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
have if : ∀ (ha : a = 0),
  a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
Tactic: if ha : a = 0 then simp [ha] else
  if hb : b = 0 then simp [hb] else
  simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b p : ℕ
if :
  ∀ (ha : a = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
have if₁ : ∀ (ha : ¬a = 0),
  a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
Tactic: if ha : a = 0 then simp [ha] else
  if hb : b = 0 then simp [hb] else
  simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hn : n ≠ 0
⊢ (n.factorization : (a : ℕ) → ℕ) p < n
have pos : ∀ (pp : Prime p), (n.factorization : (a : ℕ) → ℕ) p < n
Tactic: by_cases pp : p.Prime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hn : n ≠ 0
pos : ∀ (pp : Prime p), (n.factorization : (a : ℕ) → ℕ) p < n
⊢ (n.factorization : (a : ℕ) → ℕ) p < n
have neg : ∀ (pp : ¬Prime p), (n.factorization : (a : ℕ) → ℕ) p < n
Tactic: by_cases pp : p.Prime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b
have if : ∀ (pp : Prime p), (n.factorization : (a : ℕ) → ℕ) p ≤ b
Tactic: if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_not_prime n pp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
if : ∀ (pp : Prime p), (n.factorization : (a : ℕ) → ℕ) p ≤ b
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b
have if₁ : ∀ (pp : ¬Prime p), (n.factorization : (a : ℕ) → ℕ) p ≤ b
Tactic: if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_not_prime n pp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
hb : n ≤ p ^ b
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b
have if : ∀ (hn : n = 0), (n.factorization : (a : ℕ) → ℕ) p ≤ b
Tactic: if hn : n = 0 then simp [hn] else
  if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_not_prime n pp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
hb : n ≤ p ^ b
if : ∀ (hn : n = 0), (n.factorization : (a : ℕ) → ℕ) p ≤ b
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b
have if₁ : ∀ (hn : ¬n = 0), (n.factorization : (a : ℕ) → ℕ) p ≤ b
Tactic: if hn : n = 0 then simp [hn] else
  if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_not_prime n pp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ),
      Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    d ∣ n
have rw : (∀ (p : ℕ), Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
  d.factorization ≤ n.factorization
Tactic: rw [← factorization_le_iff_dvd hd hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ),
      Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    d.factorization ≤ n.factorization
have refine : ∀
  (h :
    ∀ (p : ℕ), Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ))
  (p : ℕ) (hp : ¬Prime p),
  LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: refine ⟨fun h p => (em p.Prime).elim (h p) fun hp => ?_, fun h p _ => h p⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
p : ℕ
hp : ¬Prime p
⊢ LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have simp_rw : LE.le (α := ℕ) 0 0
Tactic: simp_rw [factorization_eq_zero_of_not_prime _ hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hb : b ≠ 0
⊢ a.factorization ≤ (a * b).factorization
have inl : factorization 0 ≤ (0 * b).factorization
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hb : b ≠ 0
inl : factorization 0 ≤ (0 * b).factorization
⊢ a.factorization ≤ (a * b).factorization
have inr : ∀ (ha : a ≠ 0), a.factorization ≤ (a * b).factorization
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a.factorization ≤ (a * b).factorization
have inr : a ∣ a * b
Tactic: rw [factorization_le_iff_dvd ha <| mul_ne_zero ha hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (a * b).factorization
have rw : b.factorization ≤ (b * a).factorization
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
have rw : (p ^ k).factorization ≤ n.factorization ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
Tactic: rw [← factorization_le_iff_dvd (Nat.pow_pos pp.pos).ne' hn, pp.factorization_pow, single_le_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
rw : (p ^ k).factorization ≤ n.factorization ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
⊢ p ^ k ∣ n ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
have rw₁ : single p k ≤ n.factorization ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
Tactic: rw [← factorization_le_iff_dvd (Nat.pow_pos pp.pos).ne' hn, pp.factorization_pow, single_le_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
rw : (p ^ k).factorization ≤ n.factorization ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
rw₁ : single p k ≤ n.factorization ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
⊢ p ^ k ∣ n ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
have rw₂ : k ≤ (n.factorization : (a : ℕ) → ℕ) p ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
Tactic: rw [← factorization_le_iff_dvd (Nat.pow_pos pp.pos).ne' hn, pp.factorization_pow, single_le_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ p ^ k ∣ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : p ^ k ∣ n ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
Tactic: rw [pow_dvd_pow_iff_le_right pp.one_lt, pp.pow_dvd_iff_le_factorization hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
rw : p ^ k ∣ n ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
⊢ p ^ k ∣ n ↔ p ^ k ∣ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₁ : k ≤ (n.factorization : (a : ℕ) → ℕ) p ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
Tactic: rw [pow_dvd_pow_iff_le_right pp.one_lt, pp.pow_dvd_iff_le_factorization hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
a b : ℕ
ha : a ≠ 0
hab : a < b
⊢ ∃ (p : ℕ), LT.lt (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have hb : b ≠ 0
Tactic: have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hab : a < b
hb : b ≠ 0
⊢ ∃ (p : ℕ), LT.lt (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have contrapose! : ∀ (hab : ∀ (p : ℕ), LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
  b ≤ a
Tactic: contrapose! hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (p : ℕ), LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ b ≤ a
have hab₁ : b ∣ a
Tactic: rw [← Finsupp.le_def, factorization_le_iff_dvd hb ha] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
h : d ∣ n
⊢ (n / d).factorization = n.factorization - d.factorization
have inl : ∀ (h : 0 ∣ n), (n / 0).factorization = n.factorization - factorization 0
Tactic: rcases eq_or_ne d 0 with (rfl | hd)
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
h : d ∣ n
inl : ∀ (h : 0 ∣ n), (n / 0).factorization = n.factorization - factorization 0
⊢ (n / d).factorization = n.factorization - d.factorization
have inr : ∀ (hd : d ≠ 0), (n / d).factorization = n.factorization - d.factorization
Tactic: rcases eq_or_ne d 0 with (rfl | hd)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization
have inr : ∀ (h : d ∣ 0), (0 / d).factorization = factorization 0 - d.factorization
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
h : d ∣ n
hd : d ≠ 0
inr : ∀ (h : d ∣ 0), (0 / d).factorization = factorization 0 - d.factorization
⊢ (n / d).factorization = n.factorization - d.factorization
have inr₁ : ∀ (hn : n ≠ 0), (n / d).factorization = n.factorization - d.factorization
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization
have inr : Eq (α := ℕ →₀ ℕ) ((fun (x : ℕ →₀ ℕ) ↦ x + d.factorization) (n / d).factorization)
  ((fun (x : ℕ →₀ ℕ) ↦ x + d.factorization) (n.factorization - d.factorization))
Tactic: apply add_left_injective d.factorization
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization + d.factorization = n.factorization - d.factorization + d.factorization
have inr : (n / d).factorization + d.factorization = n.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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
inr : (n / d).factorization + d.factorization = n.factorization
⊢ (n / d).factorization + d.factorization = n.factorization - d.factorization + d.factorization
have inr₁ : (n / d * d).factorization = n.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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
⊢ (n / d).factorization + d.factorization = n.factorization - d.factorization + d.factorization
have inr₂ : n.factorization = n.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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬p ∣ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : ¬LE.le (α := ℕ) (1 : ℕ)
    (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [Nat.Prime.dvd_iff_one_le_factorization hp (ordCompl_pos p hn).ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬LE.le (α := ℕ) (1 : ℕ)
      (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : ¬LE.le (α := ℕ) (1 : ℕ)
    ((n.factorization - (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) p :
      ℕ)
Tactic: rw [Nat.factorization_div (Nat.ordProj_dvd n p)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
n p : ℕ
hn : ¬n = 0
⊢ (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization
have pp : Prime p
Tactic: if pp : p.Prime then ?_ else
    simp [pp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hn : ¬n = 0
pp : Prime p
⊢ (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization
have h : ∀ (q : ℕ),
  Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
Tactic: ext q
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
⊢ Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
have h : ∀ (pp : Prime q),
  Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) q ((n.factorization : (a : ℕ) → ℕ) q : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase q n.factorization : (a : ℕ) → ℕ) q : ℕ)
Tactic: rcases eq_or_ne q p with (rfl | hqp)
Cleared hypotheses: p, pp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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 : ℕ)
⊢ Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
have h₁ : ∀ (hqp : q ≠ p),
  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)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) q ((n.factorization : (a : ℕ) → ℕ) q : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase q n.factorization : (a : ℕ) → ℕ) q : ℕ)
have h : ¬Prime q ∨ ¬False ∨ n / HPow.hPow (β := ℕ) q ((n.factorization : (a : ℕ) → ℕ) q : ℕ) = 0
Tactic: simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p n.factorization : (a : ℕ) → ℕ) q : ℕ)
have h : Eq (α := ℕ)
  ((n.factorization - (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
  ((n.factorization : (a : ℕ) → ℕ) q : ℕ)
Tactic: rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
⊢ (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization = Finsupp.erase p n.factorization
have if : ∀ (hn : n = 0),
  (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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
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
have if₁ : ∀ (hn : ¬n = 0),
  (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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p k : ℕ
hp : Prime p
⊢ p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have ha : p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
Tactic: apply Nat.eq_of_factorization_eq
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p k : ℕ
hp : Prime p
ha : p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
⊢ p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have hb : Ne (α := ℕ) 1 0
Tactic: apply Nat.eq_of_factorization_eq
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p k : ℕ
hp : Prime p
ha : p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
hb : Ne (α := ℕ) 1 0
⊢ p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have h : ∀ (p_1 : ℕ),
  Eq (α := ℕ)
    (((p ^ k / HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) p_1 : ℕ)
    ((factorization 1 : (a : ℕ) → ℕ) p_1 : ℕ)
Tactic: apply Nat.eq_of_factorization_eq
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n k p : ℕ
hp : Prime p
⊢ p ^ k * n / HPow.hPow (β := ℕ) p (((p ^ k * n).factorization : (a : ℕ) → ℕ) p : ℕ) =
    n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have 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 : ℕ)
Tactic: rw [ordCompl_mul, ordCompl_self_pow hp, one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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 : ℕ)
⊢ p ^ k * n / HPow.hPow (β := ℕ) p (((p ^ k * n).factorization : (a : ℕ) → ℕ) p : ℕ) =
    n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₁ : 1 * (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) =
  n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [ordCompl_mul, ordCompl_self_pow hp, one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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 : ℕ)
⊢ p ^ k * n / HPow.hPow (β := ℕ) p (((p ^ k * n).factorization : (a : ℕ) → ℕ) p : ℕ) =
    n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₂ : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) =
  n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [ordCompl_mul, ordCompl_self_pow hp, one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n ↔ n = 0 ∨ ¬p ∣ n
have mp : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n → n = 0 ∨ ¬p ∣ n
Tactic: constructor