awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ha : a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have hb : b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
Tactic: have hb := (Nat.div_pos (ordProj_le p hb0) (ordProj_pos b p)).ne'
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
hb : b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : Finsupp.erase p a.factorization ≤ Finsupp.erase p b.factorization
Tactic: rw [← factorization_le_iff_dvd ha hb, factorization_ordCompl a p, factorization_ordCompl b p]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
hb : b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
q : ℕ
⊢ LE.le (α := ℕ) ((Finsupp.erase p a.factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p b.factorization : (a : ℕ) → ℕ) q : ℕ)
have inr : ∀ (pp : Prime q) (ha : a / HPow.hPow (β := ℕ) q ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ≠ 0)
  (hb : b / HPow.hPow (β := ℕ) q ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ≠ 0),
  LE.le (α := ℕ) ((Finsupp.erase q a.factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase q b.factorization : (a : ℕ) → ℕ) q : ℕ)
Tactic: rcases eq_or_ne q p with (rfl | hqp)
Cleared hypotheses: p, pp, ha, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
hb : b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
q : ℕ
inr :
  ∀ (pp : Prime q) (ha : a / HPow.hPow (β := ℕ) q ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ≠ 0)
    (hb : b / HPow.hPow (β := ℕ) q ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ≠ 0),
    LE.le (α := ℕ) ((Finsupp.erase q a.factorization : (a : ℕ) → ℕ) q : ℕ)
      ((Finsupp.erase q b.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ LE.le (α := ℕ) ((Finsupp.erase p a.factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p b.factorization : (a : ℕ) → ℕ) q : ℕ)
have inr₁ : ∀ (hqp : q ≠ p),
  LE.le (α := ℕ) ((Finsupp.erase p a.factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p b.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:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
hb : b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0
q : ℕ
hqp : q ≠ p
⊢ LE.le (α := ℕ) ((Finsupp.erase p a.factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p b.factorization : (a : ℕ) → ℕ) q : ℕ)
have inr : LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ)
Tactic: simp_rw [erase_ne hqp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
⊢ (∀ (p : ℕ),
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
        b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    a ∣ b
have refine : ∀
  (h :
    ∀ (p : ℕ),
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
        b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)),
  a ∣ b
Tactic: refine ⟨fun h => ?_, fun hab p => ordCompl_dvd_ordCompl_of_dvd hab p⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ a ∣ b
have inl : ∀
  (h :
    ∀ (p : ℕ),
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
        0 / HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ)),
  a ∣ 0
Tactic: rcases eq_or_ne b 0 with (rfl | hb0)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
inl :
  ∀
    (h :
      ∀ (p : ℕ),
        a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
          0 / HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ)),
    a ∣ 0
⊢ a ∣ b
have inr : ∀ (hb0 : b ≠ 0), a ∣ b
Tactic: rcases eq_or_ne b 0 with (rfl | hb0)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
a b : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
hb0 : b ≠ 0
⊢ a ∣ b
have pa : Prime a
Tactic: if pa : a.Prime then ?_ else simpa [pa] using h a
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
a b : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
hb0 : b ≠ 0
pa : Prime a
⊢ a ∣ b
have pb : Prime b
Tactic: if pb : b.Prime then ?_ else simpa [pb] using h b
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b
have inr : a = b
Tactic: rw [prime_dvd_prime_iff_eq pa pb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a = b
have inr : ∀ (hab : ¬a = b), False
Tactic: by_contra hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ False
have inr : a = 1
Tactic: apply pa.ne_one
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a = 1
have inr : b * a ∣ b
Tactic: rw [← Nat.dvd_one, ← Nat.mul_dvd_mul_iff_left hb0.bot_lt, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n d : ℕ
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
have inl : d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n d : ℕ
inl : d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
have inr : ∀ (hn : n ≠ 0), d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n d : ℕ
hn : n ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
have inr : 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n
Tactic: rcases eq_or_ne d 0 with (rfl | hd)
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n d : ℕ
hn : n ≠ 0
inr : 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
have inr₁ : ∀ (hd : d ≠ 0), d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
Tactic: rcases eq_or_ne d 0 with (rfl | hd)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n
have inr : ∃ (x : ℕ) (x_1 : ℕ) (_ : Prime x) (_ : x ^ x_1 ∣ 0), ¬x ^ x_1 ∣ n
Tactic: simp only [zero_dvd_iff, hn, false_iff, not_forall]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
have inr : (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → d ∣ n
Tactic: refine ⟨fun h p k _ hpkd => dvd_trans hpkd h, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → d ∣ n
have inr : (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) →
  ∀ (p : ℕ), Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [← factorization_prime_le_iff_dvd hd hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : HPow.hPow (β := ℕ) p ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
Tactic: simp_rw [← pp.pow_dvd_iff_le_factorization hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
⊢ ∏ p ∈ n.primeFactors, p ∣ n
have pos : ∀ (hn : n = 0), ∏ p ∈ n.primeFactors, p ∣ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
pos : ∀ (hn : n = 0), ∏ p ∈ n.primeFactors, p ∣ n
⊢ ∏ p ∈ n.primeFactors, p ∣ n
have neg : ∀ (hn : ¬n = 0), ∏ p ∈ n.primeFactors, p ∣ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n
have pos : Dvd.dvd (α := ℕ) (∏ p ∈ primeFactors 0, p) 0
Tactic: subst hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
this : ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.gcd b
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization
have rw : factorization ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.factorization ⊓ b.factorization
Tactic: rw [← this, factorization_prod_pow_eq_self_of_le_factorization inf_le_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
this : ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.gcd b
rw :
  factorization ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.factorization ⊓ b.factorization
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization
have rw₁ : a.factorization ⊓ b.factorization = a.factorization ⊓ b.factorization
Tactic: rw [← this, factorization_prod_pow_eq_self_of_le_factorization inf_le_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization
have suffices : ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.gcd b
Tactic: suffices (a.factorization ⊓ b.factorization).prod (· ^ ·) = gcd a b by
    rw [← this, factorization_prod_pow_eq_self_of_le_factorization inf_le_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.gcd b
have hda : ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ a
Tactic: apply gcd_greatest
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
hda : ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ a
⊢ ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.gcd b
have hdb : ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ b
Tactic: apply gcd_greatest
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
hda : ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ a
hdb : ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ b
⊢ ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.gcd b
have hd : ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
Tactic: apply gcd_greatest
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have hd : ∀ (hea : 0 ∣ a) (heb : 0 ∣ b), Dvd.dvd (α := ℕ) 0 ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
Tactic: rcases eq_or_ne e 0 with (rfl | he_pos)
Cleared hypotheses: e, hea, heb
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
hd :
  ∀ (hea : 0 ∣ a) (heb : 0 ∣ b), Dvd.dvd (α := ℕ) 0 ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have hd₁ : ∀ (he_pos : e ≠ 0), e ∣ (a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
Tactic: rcases eq_or_ne e 0 with (rfl | he_pos)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have hd : e.factorization ≤ a.factorization ⊓ b.factorization
Tactic: apply dvd_prod_pow_of_factorization_le he_pos
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e.factorization ≤ a.factorization ⊓ b.factorization
have hea' : e.factorization ≤ a.factorization
Tactic: have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : e.factorization ≤ a.factorization
⊢ e.factorization ≤ a.factorization ⊓ b.factorization
have heb' : e.factorization ≤ b.factorization
Tactic: have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.lcm b).factorization = a.factorization ⊔ b.factorization
have rw : a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization
Tactic: rw [← add_right_inj (a.gcd b).factorization, ←
    factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm,
    factorization_gcd ha hb, factorization_mul ha hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization
have h : ∀ (a_1 : ℕ),
  Eq (α := ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) a_1 : ℕ)
    ((a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) a_1 : ℕ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
have inl : (gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f
Tactic: obtain rfl | hm₀ := eq_or_ne m 0
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
inl : (gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
have inr : ∀ (hm₀ : m ≠ 0),
  (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
Tactic: obtain rfl | hm₀ := eq_or_ne m 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
have inr : (m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f
Tactic: obtain rfl | hn₀ := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
inr : (m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
have inr₁ : ∀ (hn₀ : n ≠ 0),
  (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
Tactic: obtain rfl | hn₀ := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
have inr : (m.gcd n).primeFactors.prod f * (m.primeFactors ∪ n.primeFactors).prod f = m.primeFactors.prod f * n.primeFactors.prod f
Tactic: rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
inr :
  (m.gcd n).primeFactors.prod f * (m.primeFactors ∪ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
have inr₁ : (m.primeFactors ∩ n.primeFactors).prod f * (m.primeFactors ∪ n.primeFactors).prod f =
  m.primeFactors.prod f * n.primeFactors.prod f
Tactic: rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
inr :
  (m.gcd n).primeFactors.prod f * (m.primeFactors ∪ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
inr₁ :
  (m.primeFactors ∩ n.primeFactors).prod f * (m.primeFactors ∪ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
have inr₂ : (m.primeFactors ∪ n.primeFactors).prod f * (m.primeFactors ∩ n.primeFactors).prod f =
  m.primeFactors.prod f * n.primeFactors.prod f
Tactic: rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
inr :
  (m.gcd n).primeFactors.prod f * (m.primeFactors ∪ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
inr₁ :
  (m.primeFactors ∩ n.primeFactors).prod f * (m.primeFactors ∪ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
inr₂ :
  (m.primeFactors ∪ n.primeFactors).prod f * (m.primeFactors ∩ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
have inr₃ : HMul.hMul (α := β) (∏ x ∈ m.primeFactors, f x) (∏ x ∈ n.primeFactors, f x) =
  m.primeFactors.prod f * n.primeFactors.prod f
Tactic: rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Eq (α := Set ℕ) ({i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} : Set ℕ) (Set.Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) : Set ℕ)
have h : ∀ (x : ℕ),
  Membership.mem (γ := Set ℕ) {i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} x ↔
    Membership.mem (γ := Set ℕ) (Set.Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) : Set ℕ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
pp : Prime p
⊢ Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) = {i ∈ Ico 1 n | p ^ i ∣ n}
have inl : Eq (α := Finset ℕ) (Icc 1 ((factorization 0 : (a : ℕ) → ℕ) p) : Finset ℕ) ({i ∈ Ico 1 0 | p ^ i ∣ 0} : Finset ℕ)
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
pp : Prime p
inl : Eq (α := Finset ℕ) (Icc 1 ((factorization 0 : (a : ℕ) → ℕ) p) : Finset ℕ) ({i ∈ Ico 1 0 | p ^ i ∣ 0} : Finset ℕ)
⊢ Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) = {i ∈ Ico 1 n | p ^ i ∣ n}
have inr : ∀ (hn : n ≠ 0), Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) = {i ∈ Ico 1 n | p ^ i ∣ n}
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) = {i ∈ Ico 1 n | p ^ i ∣ n}
have inr : ∀ (x : ℕ),
  Membership.mem (γ := Finset ℕ) (Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) : Finset ℕ) x ↔
    x ∈ {i ∈ Ico 1 n | p ^ i ∣ n}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
⊢ Membership.mem (γ := Finset ℕ) (Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) : Finset ℕ) x ↔
    x ∈ {i ∈ Ico 1 n | p ^ i ∣ n}
have inr : 1 ≤ x → x ≤ (n.factorization : (a : ℕ) → ℕ) p → x < n
Tactic: simp only [mem_Icc, Finset.mem_filter, mem_Ico, and_assoc, and_congr_right_iff,
    pp.pow_dvd_iff_le_factorization hn, iff_and_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
⊢ {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Icc 1 b | p ^ i ∣ n}
have h : ∀ (x : ℕ), x ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ x ∈ {i ∈ Icc 1 b | p ^ i ∣ n}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ x ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ x ∈ {i ∈ Icc 1 b | p ^ i ∣ n}
have h : p ^ x ∣ n → 1 ≤ x → (x < n ↔ x ≤ b)
Tactic: simp only [Finset.mem_filter, mem_Ico, mem_Icc, and_congr_left_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
⊢ {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Ico 1 b | p ^ i ∣ n}
have h : ∀ (i : ℕ), i ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ i ∈ {i ∈ Ico 1 b | p ^ i ∣ n}
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
⊢ i ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ i ∈ {i ∈ Ico 1 b | p ^ i ∣ n}
have h : p ^ i ∣ n → 1 ≤ i → (i < n ↔ i < b)
Tactic: simp only [Finset.mem_filter, mem_Ico, and_congr_left_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
⊢ p ^ i ∣ n → 1 ≤ i → (i < n ↔ i < b)
have h : ∀ (h1 : p ^ i ∣ n) (h2 : 1 ≤ i) (h : i < n), i < b
Tactic: refine fun h1 h2 ↦ ⟨fun h ↦ ?_, fun h ↦ lt_of_pow_dvd_right hn (Prime.one_lt pp) h1⟩