awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
inr₅ inr₆ inr₇ inr₈ : ∀ (hp : False), False
⊢ False

Tactic:
rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
    lt_self_iff_false] at hp

Premises used: lt_tsub_iff_right, Nat.factorization_mul, Finsupp.add_apply, lt_self_iff_false, Finsupp.tsub_apply
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 : ℕ)
inr :
  ∀ (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 : ℕ)

Tactic:
rcases em' p.Prime with (pp | pp)

Premises used: Nat.Prime, em'
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 : ℕ)

Tactic:
simp [pp]
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 : ℕ)
inr₁ :
  ∀ (ha0 : a ≠ 0),
    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 : ℕ)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
inr : LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [pow_dvd_pow_iff_le_right pp.one_lt]

Premises used: Nat.Prime.one_lt, Nat.pow_dvd_pow_iff_le_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
(factorization_le_iff_dvd ha0 hb0).2 hab p

Premises used: Iff.mpr, Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
exact (factorization_le_iff_dvd ha0 hb0).2 hab p

Premises used: Iff.mpr, Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 : ℕ)
inr :
  ∀ (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 : ℕ)

Tactic:
rcases em' p.Prime with (pp | pp)

Premises used: Nat.Prime, em'
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 : ℕ)

Tactic:
simp [pp, hab]
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 : ℕ)
inr₁ :
  ∀ (hb0 : b ≠ 0),
    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 : ℕ)

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    0 / HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 : ℕ)
inr₁ :
  ∀ (ha0 : a ≠ 0),
    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 : ℕ)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
cases hb0 (zero_dvd_iff.1 hab)

Premises used: zero_dvd_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0

Tactic:
have ha := (Nat.div_pos (ordProj_le p ha0) (ordProj_pos a p)).ne'
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
⊢ b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 0

Tactic:
have hb := (Nat.div_pos (ordProj_le p hb0) (ordProj_pos b p)).ne'
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
inr : Finsupp.erase p a.factorization ≤ Finsupp.erase p b.factorization
⊢ a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [← factorization_le_iff_dvd ha hb, factorization_ordCompl a p, factorization_ordCompl b p]

Premises used: Nat.factorization_le_iff_dvd, Nat.factorization_ordCompl
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 : ℕ)
inr₁ :
  ∀ (hqp : q ≠ p),
    LE.le (α := ℕ) ((Finsupp.erase p a.factorization : (a : ℕ) → ℕ) q : ℕ)
      ((Finsupp.erase p b.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ 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)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
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:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
inr : LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ LE.le (α := ℕ) ((Finsupp.erase p a.factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Finsupp.erase p b.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
simp_rw [erase_ne hqp]

Premises used: Finsupp.erase_ne
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
(factorization_le_iff_dvd ha0 hb0).2 hab q

Premises used: Iff.mpr, Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
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 (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
exact (factorization_le_iff_dvd ha0 hb0).2 hab q

Premises used: Iff.mpr, Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
⊢ (∀ (p : ℕ),
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
        b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    a ∣ b

Tactic:
⟨fun h => ?_, fun hab p => ordCompl_dvd_ordCompl_of_dvd hab p⟩

Premises used: Nat.ordCompl_dvd_ordCompl_of_dvd, Iff.intro
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
refine :
  ∀
    (h :
      ∀ (p : ℕ),
        a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
          b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)),
    a ∣ b
⊢ (∀ (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⟩
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
inr : ∀ (hb0 : b ≠ 0), a ∣ b
⊢ a ∣ b

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      0 / HPow.hPow (β := ℕ) p ((factorization 0 : (a : ℕ) → ℕ) p : ℕ)
⊢ a ∣ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
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

Tactic:
simpa [pa] using h a
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
h :
  ∀ (p : ℕ),
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
hb0 : b ≠ 0
⊢ Prime a

Tactic:
if pa : a.Prime then ?_ else simpa [pa] using h a

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
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

Tactic:
simpa [pb] using h b
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
⊢ Prime b

Tactic:
if pb : b.Prime then ?_ else simpa [pb] using h b

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
inr : a = b
⊢ a ∣ b

Tactic:
rw [prime_dvd_prime_iff_eq pa pb]

Premises used: Nat.prime_dvd_prime_iff_eq
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
inr : ∀ (hab : ¬a = b), False
⊢ a = b

Tactic:
by_contra hab
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
inr : a = 1
⊢ False

Tactic:
apply pa.ne_one

Premises used: Nat.Prime.ne_one
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
inr : b * a ∣ b
⊢ a = 1

Tactic:
rw [← Nat.dvd_one, ← Nat.mul_dvd_mul_iff_left hb0.bot_lt, mul_one]

Premises used: Nat.dvd_one, Nat.mul_dvd_mul_iff_left, mul_one, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
⊢ b * a ∣ b

Tactic:
simpa [Prime.factorization_self pb, Prime.factorization pa, hab] using h b

Premises used: Nat.Prime.factorization, Nat.Prime.factorization_self
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n d : ℕ
inl : d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0
inr : ∀ (hn : n ≠ 0), d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d : ℕ
⊢ d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n d : ℕ
hn : n ≠ 0
inr : 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n
inr₁ : ∀ (hd : d ≠ 0), d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
rcases eq_or_ne d 0 with (rfl | hd)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
inr : ∃ (x : ℕ) (x_1 : ℕ) (_ : Prime x) (_ : x ^ x_1 ∣ 0), ¬x ^ x_1 ∣ n
⊢ 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n

Tactic:
simp only [zero_dvd_iff, hn, false_iff, not_forall]

Premises used: zero_dvd_iff, false_iff, Classical.not_forall
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ ∃ (x : ℕ) (x_1 : ℕ) (_ : Prime x) (_ : x ^ x_1 ∣ 0), ¬x ^ x_1 ∣ n

Tactic:
⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (n.lt_two_pow_self).not_ge⟩

Premises used: dvd_zero, mt, Nat.prime_two, Nat.lt_two_pow_self, Exists.intro, LT.lt.not_ge, OfNat.ofNat, Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ ∃ (x : ℕ) (x_1 : ℕ) (_ : Prime x) (_ : x ^ x_1 ∣ 0), ¬x ^ x_1 ∣ n

Tactic:
exact ⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (n.lt_two_pow_self).not_ge⟩
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
⟨fun h p k _ hpkd => dvd_trans hpkd h, ?_⟩

Premises used: dvd_trans, Iff.intro
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
inr : (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → d ∣ n
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
refine ⟨fun h p k _ hpkd => dvd_trans hpkd h, ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
inr :
  (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) →
    ∀ (p : ℕ), Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → d ∣ n

Tactic:
rw [← factorization_prime_le_iff_dvd hd hn]

Premises used: Nat.factorization_prime_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
inr : HPow.hPow (β := ℕ) p ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
⊢ LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp_rw [← pp.pow_dvd_iff_le_factorization hn]

Premises used: Nat.Prime.pow_dvd_iff_le_factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ HPow.hPow (β := ℕ) p ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n

Tactic:
h p _ pp (ordProj_dvd _ _)

Premises used: Nat.ordProj_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ HPow.hPow (β := ℕ) p ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n

Tactic:
exact h p _ pp (ordProj_dvd _ _)

Premises used: Nat.ordProj_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
pos : ∀ (hn : n = 0), ∏ p ∈ n.primeFactors, p ∣ n
neg : ∀ (hn : ¬n = 0), ∏ p ∈ n.primeFactors, p ∣ n
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n = 0
pos : Dvd.dvd (α := ℕ) (∏ p ∈ primeFactors 0, p) 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
subst hn
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
⊢ Dvd.dvd (α := ℕ) (∏ p ∈ primeFactors 0, p) 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
simpa [prod_primeFactorsList hn] using (n.primeFactorsList : Multiset ℕ).toFinset_prod_dvd_prod

Premises used: Multiset.toFinset_prod_dvd_prod, Multiset.ofList, Nat.prod_primeFactorsList, Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
rw₁ rw₂ : a.factorization ⊓ b.factorization = a.factorization ⊓ b.factorization
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
rw [← this, factorization_prod_pow_eq_self_of_le_factorization inf_le_left]

Premises used: Nat.factorization_prod_pow_eq_self_of_le_factorization, inf_le_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
suffices : ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.gcd b
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
suffices (a.factorization ⊓ b.factorization).prod (· ^ ·) = gcd a b by
    rw [← this, factorization_prod_pow_eq_self_of_le_factorization inf_le_left]
-- Module: Mathlib.Data.Nat.Factorization.Basic
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
hd : ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
⊢ ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a.gcd b

Tactic:
apply gcd_greatest

Premises used: Nat.gcd_greatest
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ a

Tactic:
prod_pow_dvd_of_le_factorization inf_le_left

Premises used: Nat.prod_pow_dvd_of_le_factorization, inf_le_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ a

Tactic:
exact prod_pow_dvd_of_le_factorization inf_le_left

Premises used: Nat.prod_pow_dvd_of_le_factorization, inf_le_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ b

Tactic:
prod_pow_dvd_of_le_factorization inf_le_right

Premises used: inf_le_right, Nat.prod_pow_dvd_of_le_factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ b

Tactic:
exact prod_pow_dvd_of_le_factorization inf_le_right

Premises used: inf_le_right, Nat.prod_pow_dvd_of_le_factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
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)
hd₁ : ∀ (he_pos : e ≠ 0), e ∣ (a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
rcases eq_or_ne e 0 with (rfl | he_pos)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
hea : 0 ∣ a
heb : 0 ∣ b
⊢ Dvd.dvd (α := ℕ) 0 ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
absurd (zero_dvd_iff.mp hea) ha_pos

Premises used: zero_dvd_iff, absurd, Iff.mp