awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr : a.factorizationLCMLeft b ∣ a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
nth_rewrite 2 [← prod_factorization_pow_eq_self ha]

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr :
  a.factorizationLCMLeft b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((a.factorization : (a : ℕ) → ℕ) x : ℕ)
inr₁ : a.factorization.support ⊆ (a.lcm b).factorization.support
inr₂ : ∀ i ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) i 0 = 1
⊢ a.factorizationLCMLeft b ∣ a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
rw [prod_of_support_subset (s := (lcm a b).factorization.support)]

Premises used: Finsupp.prod_of_support_subset
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr :
  ∀ i ∈ (a.lcm b).factorization.support,
    (fun (p n : ℕ) ↦
          if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
          else 1)
        i (((a.lcm b).factorization : (a : ℕ) → ℕ) i) ∣
      HPow.hPow (β := ℕ) i ((a.factorization : (a : ℕ) → ℕ) i : ℕ)
⊢ a.factorizationLCMLeft b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((a.factorization : (a : ℕ) → ℕ) x : ℕ)

Tactic:
apply prod_dvd_prod_of_dvd

Premises used: Finset.prod_dvd_prod_of_dvd
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
pos :
  ∀ (le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
    HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  ∀ (le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
    1 ∣ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then
      HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)
    else 1) ∣
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
split_ifs with le
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
pos :
  HPow.hPow (β := ℕ) p ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [factorization_lcm ha hb]

Premises used: Nat.factorization_lcm
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
pos : LE.le (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
apply pow_dvd_pow

Premises used: pow_dvd_pow
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ LE.le (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
sup_le le_rfl le

Premises used: le_rfl, sup_le
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ LE.le (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
exact sup_le le_rfl le

Premises used: le_rfl, sup_le
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ 1 ∣ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
apply one_dvd

Premises used: one_dvd
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.factorization.support
inr :
  ∀ (hp : Ne (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    Ne (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ p ∈ (a.lcm b).factorization.support

Tactic:
rw [mem_support_iff] at hp ⊢

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : Ne (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
inr : Ne (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Ne (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rw [factorization_lcm ha hb]

Premises used: Nat.factorization_lcm
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : Ne (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Ne (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
(lt_sup_iff.mpr <| .inl <| Nat.pos_of_ne_zero hp).ne'

Premises used: Iff.mpr, lt_sup_iff, LT.lt.ne', Nat.pos_of_ne_zero, Or.inl
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : Ne (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Ne (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
exact (lt_sup_iff.mpr <| .inl <| Nat.pos_of_ne_zero hp).ne'

Premises used: Iff.mpr, lt_sup_iff, LT.lt.ne', Nat.pos_of_ne_zero, Or.inl
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
i : ℕ
h : i ∈ (a.lcm b).factorization.support
inr inr₁ : Eq (α := ℕ) 1 1
⊢ HPow.hPow (β := ℕ) i 0 = 1

Tactic:
rw [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
inl : factorizationLCMRight 0 b ∣ b
inr : ∀ (ha : a ≠ 0), a.factorizationLCMRight b ∣ b
⊢ a.factorizationLCMRight b ∣ b

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
b : ℕ
⊢ factorizationLCMRight 0 b ∣ b

Tactic:
simp [factorizationLCMRight]

Premises used: Nat.factorizationLCMRight
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
inr : a.factorizationLCMRight 0 ∣ 0
inr₁ : ∀ (hb : b ≠ 0), a.factorizationLCMRight b ∣ b
⊢ a.factorizationLCMRight b ∣ b

Tactic:
rcases eq_or_ne b 0 with rfl | hb

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMRight 0 ∣ 0

Tactic:
simp only [dvd_zero]

Premises used: dvd_zero
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr : a.factorizationLCMRight b ∣ b.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
⊢ a.factorizationLCMRight b ∣ b

Tactic:
nth_rewrite 2 [← prod_factorization_pow_eq_self hb]

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr :
  a.factorizationLCMRight b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((b.factorization : (a : ℕ) → ℕ) x : ℕ)
inr₁ : b.factorization.support ⊆ (a.lcm b).factorization.support
inr₂ : ∀ i ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) i 0 = 1
⊢ a.factorizationLCMRight b ∣ b.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
rw [prod_of_support_subset (s := (lcm a b).factorization.support)]

Premises used: Finsupp.prod_of_support_subset
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr :
  ∀ i ∈ (a.lcm b).factorization.support,
    (fun (p n : ℕ) ↦
          if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
          else p ^ n)
        i (((a.lcm b).factorization : (a : ℕ) → ℕ) i) ∣
      HPow.hPow (β := ℕ) i ((b.factorization : (a : ℕ) → ℕ) i : ℕ)
⊢ a.factorizationLCMRight b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((b.factorization : (a : ℕ) → ℕ) x : ℕ)

Tactic:
apply Finset.prod_dvd_prod_of_dvd

Premises used: Finset.prod_dvd_prod_of_dvd
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
pos :
  ∀ (le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
    1 ∣ HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  ∀ (le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
    HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
    else HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
split_ifs with le
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ 1 ∣ HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
apply one_dvd

Premises used: one_dvd
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  HPow.hPow (β := ℕ) p ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [factorization_lcm ha hb]

Premises used: Nat.factorization_lcm
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
neg : LE.le (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
apply pow_dvd_pow

Premises used: pow_dvd_pow
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ LE.le (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
sup_le (not_le.1 le).le le_rfl

Premises used: not_le, le_rfl, LT.lt.le, Iff.mp, sup_le
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ LE.le (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
exact sup_le (not_le.1 le).le le_rfl

Premises used: not_le, le_rfl, LT.lt.le, Iff.mp, sup_le
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ b.factorization.support
inr :
  ∀ (hp : Ne (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    Ne (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ p ∈ (a.lcm b).factorization.support

Tactic:
rw [mem_support_iff] at hp ⊢

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : Ne (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
inr : Ne (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Ne (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rw [factorization_lcm ha hb]

Premises used: Nat.factorization_lcm
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : Ne (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Ne (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
(lt_sup_iff.mpr <| .inr <| Nat.pos_of_ne_zero hp).ne'

Premises used: Iff.mpr, lt_sup_iff, LT.lt.ne', Nat.pos_of_ne_zero, Or.inr
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : Ne (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Ne (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
exact (lt_sup_iff.mpr <| .inr <| Nat.pos_of_ne_zero hp).ne'

Premises used: Iff.mpr, lt_sup_iff, LT.lt.ne', Nat.pos_of_ne_zero, Or.inr
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : IsPrimePow n
obtain :
  ∀ (p k : ℕ) (hp : Prime p) (hk : 0 < k),
    HPow.hPow (β := ℕ) (p ^ k).minFac (((p ^ k).factorization : (a : ℕ) → ℕ) (p ^ k).minFac : ℕ) = p ^ k
⊢ HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n

Tactic:
obtain ⟨p, k, hp, hk, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ Nat.Prime p

Tactic:
rw [← Nat.prime_iff] at hp

Premises used: Nat.prime_iff
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
hp₁ : Nat.Prime p
⊢ 0 < k

Tactic:
rw [← Nat.prime_iff] at hp

Premises used: Nat.prime_iff
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
rw : HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) = p ^ k
rw₁ : HPow.hPow (β := ℕ) p ((Finsupp.single p k : (a : ℕ) → ℕ) p : ℕ) = p ^ k
rw₂ rw₃ : p ^ k = p ^ k
⊢ HPow.hPow (β := ℕ) (p ^ k).minFac (((p ^ k).factorization : (a : ℕ) → ℕ) (p ^ k).minFac : ℕ) = p ^ k

Tactic:
rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, Nat.Prime.factorization_pow, LT.lt.ne', Nat.Prime.pow_minFac
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n
hn : n ≠ 1
inl :
  ∀ (h : HPow.hPow (β := ℕ) (Nat.minFac 0) ((Nat.factorization 0 : (a : ℕ) → ℕ) (Nat.minFac 0) : ℕ) = 0)
    (hn : Ne (α := ℕ) 0 1), IsPrimePow (R := ℕ) 0
inr : ∀ (hn' : n ≠ 0), IsPrimePow n
⊢ IsPrimePow n

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
h : HPow.hPow (β := ℕ) (Nat.minFac 0) ((Nat.factorization 0 : (a : ℕ) → ℕ) (Nat.minFac 0) : ℕ) = 0
hn : Ne (α := ℕ) 0 1
⊢ IsPrimePow (R := ℕ) 0

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n

Tactic:
⟨_, _, (Nat.minFac_prime hn).prime, ?_, h⟩

Premises used: IsPrimePow, Nat.Prime.prime, And.intro, Exists.intro, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n
hn : n ≠ 1
hn' : n ≠ 0
inr : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ)
⊢ IsPrimePow n

Tactic:
refine ⟨_, _, (Nat.minFac_prime hn).prime, ?_, h⟩
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ)

Tactic:
simp [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.support_factorization, hn',
    Nat.minFac_prime hn, Nat.minFac_dvd]

Premises used: Finsupp.mem_support_iff, Nat.support_factorization, Nat.minFac_dvd, pos_iff_ne_zero, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : n ≠ 1
⊢ IsPrimePow n ↔ HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n

Tactic:
⟨fun h => h.minFac_pow_factorization_eq, fun h => isPrimePow_of_minFac_pow_factorization_eq h hn⟩

Premises used: IsPrimePow.minFac_pow_factorization_eq, isPrimePow_of_minFac_pow_factorization_eq, Iff.intro
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
rw :
  (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k
⊢ IsPrimePow n ↔ ∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
rw [isPrimePow_nat_iff]

Premises used: isPrimePow_nat_iff
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
⊢ (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
exists₂_congr fun p k => ?_

Premises used: exists₂_congr
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
refine : ∀ (p k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n ↔ 0 < k ∧ n.factorization = Finsupp.single p k
⊢ (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
refine exists₂_congr fun p k => ?_

Premises used: exists₂_congr
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p k : ℕ
mp : Nat.Prime p ∧ 0 < k ∧ p ^ k = n → 0 < k ∧ n.factorization = Finsupp.single p k
mpr : 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n ↔ 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
rw : (p ^ k).factorization = Finsupp.single p k
rw₁ rw₂ : Eq (α := ℕ →₀ ℕ) (Finsupp.single p k) (Finsupp.single p k)
⊢ n.factorization = Finsupp.single p k

Tactic:
rw [← hn, Nat.Prime.factorization_pow hp]

Premises used: Nat.Prime.factorization_pow
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
exact ⟨hk, by rw [← hn, Nat.Prime.factorization_pow hp]⟩
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p k : ℕ
hk : 0 < k
hn : Nat.factorization 0 = Finsupp.single p k
⊢ False

Tactic:
simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']

Premises used: Finsupp.single_eq_zero, Nat.factorization_zero, eq_comm, LT.lt.ne'
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
⊢ n ≠ 0

Tactic:
have hn0 : n ≠ 0 := by
      rintro rfl
      simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
mpr : Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]

Premises used: Nat.eq_pow_of_factorization_eq_single
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Ne (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp [hn, hk.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k

Tactic:
exact ⟨Nat.prime_of_mem_primeFactors <|
      Finsupp.mem_support_iff.2 (by simp [hn, hk.ne'] : n.factorization p ≠ 0), hk, rfl⟩
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
simp_rw : (∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k) ↔ n.primeFactors.card = 1
simp_rw₁ : (∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k) ↔ n.factorization.support.card = 1
simp_rw₂ :
  (∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k) ↔
    ∃ (a : ℕ) (b : ℕ), b ≠ 0 ∧ n.factorization = Finsupp.single a b
⊢ IsPrimePow n ↔ n.primeFactors.card = 1

Tactic:
simp_rw [isPrimePow_iff_factorization_eq_single, ← Nat.support_factorization,
    Finsupp.card_support_eq_one', pos_iff_ne_zero]

Premises used: isPrimePow_iff_factorization_eq_single, Nat.support_factorization, Finsupp.card_support_eq_one', pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : 2 ≤ n
rw : ¬n.primeFactors.card = 1 ↔ 1 < n.primeFactors.card
⊢ ¬IsPrimePow n ↔ n.primeFactors.Nontrivial

Tactic:
rw [isPrimePow_iff_card_primeFactors_eq_one, ← Finset.one_lt_card_iff_nontrivial]

Premises used: isPrimePow_iff_card_primeFactors_eq_one, Finset.one_lt_card_iff_nontrivial
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : 2 ≤ n
⊢ ¬n.primeFactors.card = 1 ↔ 1 < n.primeFactors.card

Tactic:
grind [primeFactors_eq_empty]

Premises used: Nat.primeFactors_eq_empty
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : IsPrimePow n
inl :
  ∀ (h : IsPrimePow (R := ℕ) 0),
    ∃ (p : ℕ), Nat.Prime p ∧ 0 / HPow.hPow (β := ℕ) p ((Nat.factorization 0 : (a : ℕ) → ℕ) p : ℕ) = 1
inr : ∀ (hn0 : n ≠ 0), ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
h : IsPrimePow (R := ℕ) 0
⊢ ∃ (p : ℕ), Nat.Prime p ∧ 0 / HPow.hPow (β := ℕ) p ((Nat.factorization 0 : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
cases not_isPrimePow_zero h

Premises used: not_isPrimePow_zero
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
inr :
  ∀ (p k : ℕ) (hk0 : 0 < k) (h1 : n.factorization = Finsupp.single p k),
    ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
rcases isPrimePow_iff_factorization_eq_single.mp h with ⟨p, k, hk0, h1⟩

Premises used: isPrimePow_iff_factorization_eq_single, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
inr :
  ∀ (pp : ¬Nat.Prime p), ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
inr₁ :
  ∀ (pp : Nat.Prime p), ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

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

Premises used: Nat.Prime, em'
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
absurd ?_ hk0.ne'

Premises used: LT.lt.ne', absurd
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
inr : k = 0
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
refine absurd ?_ hk0.ne'

Premises used: LT.lt.ne', absurd
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ k = 0

Tactic:
simp [← Nat.factorization_eq_zero_of_not_prime n pp, h1]

Premises used: Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
⟨p, pp, ?_⟩

Premises used: And.intro, Exists.intro