awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
refine ⟨p, pp, ?_⟩
-- 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
⊢ Ne (α := ℕ) 1 0

Tactic:
simp
-- 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 :
  ∀ (q : ℕ),
    Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
      ((Nat.factorization 1 : (a : ℕ) → ℕ) q : ℕ)
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
refine Nat.eq_of_factorization_eq (Nat.ordCompl_pos p hn0).ne' (by simp) fun q => ?_

Premises used: LT.lt.ne', Nat.ordCompl_pos, Nat.eq_of_factorization_eq
-- 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
q : ℕ
inr :
  Eq (α := ℕ) ((Finsupp.erase p (Finsupp.single p k) : (a : ℕ) → ℕ) q : ℕ) ((Nat.factorization 1 : (a : ℕ) → ℕ) q : ℕ)
⊢ Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Nat.factorization 1 : (a : ℕ) → ℕ) q : ℕ)

Tactic:
rw [Nat.factorization_ordCompl n p, h1]

Premises used: Nat.factorization_ordCompl
-- 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
q : ℕ
⊢ Eq (α := ℕ) ((Finsupp.erase p (Finsupp.single p k) : (a : ℕ) → ℕ) q : ℕ) ((Nat.factorization 1 : (a : ℕ) → ℕ) q : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : n ≠ 1
⊢ IsPrimePow n ↔ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
⟨fun h => IsPrimePow.exists_ordCompl_eq_one h, fun h => ?_⟩

Premises used: IsPrimePow.exists_ordCompl_eq_one, Iff.intro
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : n ≠ 1
refine :
  ∀ (h : ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1), IsPrimePow n
⊢ IsPrimePow n ↔ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
refine ⟨fun h => IsPrimePow.exists_ordCompl_eq_one h, fun h => ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : n ≠ 1
h : ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
rcases :
  ∀ (p : ℕ) (pp : Nat.Prime p) (h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1), IsPrimePow n
⊢ IsPrimePow n

Tactic:
rcases h with ⟨p, pp, h⟩
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
rw : ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⊢ IsPrimePow n

Tactic:
rw [isPrimePow_nat_iff]

Premises used: isPrimePow_nat_iff
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
rw :
  ∀ (hn : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1) (pp : Nat.Prime p)
    (h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1),
    ∃ (p_1 : ℕ) (k : ℕ), Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rw [← Nat.eq_of_dvd_of_div_eq_one (Nat.ordProj_dvd n p) h] at hn ⊢

Premises used: Nat.eq_of_dvd_of_div_eq_one, Nat.ordProj_dvd
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hn : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hn : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
refine : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ∃ (p_1 : ℕ) (k : ℕ), Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
refine ⟨p, n.factorization p, pp, ?_, by simp⟩
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hn : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
contrapose! :
  ∀ (hn : LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
contrapose! hn
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
hn : LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
simp [Nat.le_zero.1 hn]

Premises used: Nat.le_zero, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
rw : (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
⊢ IsPrimePow n ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n

Tactic:
rw [isPrimePow_nat_iff]

Premises used: isPrimePow_nat_iff
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
mp : (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
mpr : (∃! p : ℕ, Nat.Prime p ∧ p ∣ n) → ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⊢ (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃! p_1 : ℕ, Nat.Prime p_1 ∧ p_1 ∣ p ^ k

Tactic:
⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, ?_⟩

Premises used: dvd_pow_self, LT.lt.ne', ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
mp : ∀ (y : ℕ), (fun (p_1 : ℕ) ↦ Nat.Prime p_1 ∧ p_1 ∣ p ^ k) y → y = p
⊢ ∃! p_1 : ℕ, Nat.Prime p_1 ∧ p_1 ∣ p ^ k

Tactic:
refine ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ k
⊢ q = p

Tactic:
(Nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq')

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.prime_dvd_prime_iff_eq, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ k
⊢ q = p

Tactic:
exact (Nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq')

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.prime_dvd_prime_iff_eq, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
mpr :
  ∀ (hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ 0) y → y = p) (hn : p ∣ 0),
    ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = 0
mpr₁ : ∀ (hn₀ : n ≠ 0), ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⊢ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ 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.PrimePow
Goal:
p : ℕ
hp : Nat.Prime p
hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ 0) y → y = p
hn : p ∣ 0
⊢ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = 0

Tactic:
cases (hq 2 ⟨Nat.prime_two, dvd_zero 2⟩).trans (hq 3 ⟨Nat.prime_three, dvd_zero 3⟩).symm

Premises used: dvd_zero, Nat.prime_two, Nat.prime_three, And.intro, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, ?_⟩

Premises used: Nat.Prime.factorization_pos_of_dvd, And.intro, Exists.intro, DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
mpr : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
⊢ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
refine ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p

Tactic:
simp only [and_imp] at hq

Premises used: and_imp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
mpr : n ∣ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n

Tactic:
apply Nat.dvd_antisymm (Nat.ordProj_dvd _ _)

Premises used: Nat.ordProj_dvd, Nat.dvd_antisymm
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
mpr : n.primeFactorsList.Subperm (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).primeFactorsList
⊢ n ∣ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
apply Nat.dvd_of_primeFactorsList_subperm hn₀

Premises used: Nat.dvd_of_primeFactorsList_subperm
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
mpr :
  ∀ x ∈ n.primeFactorsList,
    List.count x n.primeFactorsList ≤ List.count x (List.replicate ((n.factorization : (a : ℕ) → ℕ) p) p)
⊢ n.primeFactorsList.Subperm (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).primeFactorsList

Tactic:
rw [hp.primeFactorsList_pow, List.subperm_ext_iff]

Premises used: Nat.Prime.primeFactorsList_pow, List.subperm_ext_iff
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : q ∈ n.primeFactorsList
⊢ Nat.Prime q ∧ q ∣ n

Tactic:
rw [Nat.mem_primeFactorsList hn₀] at hq'

Premises used: Nat.mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : Nat.Prime q ∧ q ∣ n
mpr :
  ∀ (hq' : Nat.Prime p ∧ p ∣ n),
    List.count p n.primeFactorsList ≤ List.count p (List.replicate ((n.factorization : (a : ℕ) → ℕ) p) p)
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate ((n.factorization : (a : ℕ) → ℕ) p) p)

Tactic:
cases hq _ hq'.1 hq'.2

Premises used: And.right, And.left
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
hq' : Nat.Prime p ∧ p ∣ n
⊢ List.count p n.primeFactorsList ≤ List.count p (List.replicate ((n.factorization : (a : ℕ) → ℕ) p) p)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n k : ℕ
hk : k ≠ 0
simp : (∃! p : ℕ, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
⊢ IsPrimePow (n ^ k) ↔ IsPrimePow n

Tactic:
simp only [isPrimePow_iff_unique_prime_dvd]

Premises used: isPrimePow_iff_unique_prime_dvd
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n k : ℕ
hk : k ≠ 0
h : ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n
⊢ (∃! p : ℕ, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n

Tactic:
apply existsUnique_congr

Premises used: existsUnique_congr
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n

Tactic:
simp +contextual [Nat.prime_iff, Prime.dvd_pow_iff_dvd, hk]

Premises used: Nat.prime_iff, Prime.dvd_pow_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
inl : ∀ (hab : Coprime 0 b), n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
inr : ∀ (ha : a ≠ 0), n ∣ a * b ↔ n ∣ a ∨ n ∣ b
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n b : ℕ
hn : IsPrimePow n
hab : Coprime 0 b
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
inr : ∀ (hab : a.Coprime 0), n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
inr₁ : ∀ (hb : b ≠ 0), n ∣ a * b ↔ n ∣ a ∨ n ∣ b
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : a.Coprime 0
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b

Tactic:
⟨?_, fun h =>
      Or.elim h (fun i => i.trans ((@dvd_mul_right a b a hab).mpr (dvd_refl a)))
          fun i => i.trans ((@dvd_mul_left a b b hab.symm).mpr (dvd_refl b))⟩

Premises used: Iff.mpr, Nat.Coprime.symm, Nat.Coprime.dvd_mul_right, Iff.intro, Nat.Coprime.dvd_mul_left, Or.elim, dvd_refl, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
inr : n ∣ a * b → n ∣ a ∨ n ∣ b
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b

Tactic:
refine
    ⟨?_, fun h =>
      Or.elim h (fun i => i.trans ((@dvd_mul_right a b a hab).mpr (dvd_refl a)))
          fun i => i.trans ((@dvd_mul_left a b b hab.symm).mpr (dvd_refl b))⟩
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
inr : ∀ (p k : ℕ) (hp : Prime p), 0 < k → ∀ (hn : IsPrimePow (p ^ k)), p ^ k ∣ a * b → p ^ k ∣ a ∨ p ^ k ∣ b
⊢ n ∣ a * b → n ∣ a ∨ n ∣ b

Tactic:
obtain ⟨p, k, hp, _, rfl⟩ := (isPrimePow_nat_iff _).1 hn

Premises used: isPrimePow_nat_iff, Iff.mp, rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
inr :
  k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
    k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
⊢ p ^ k ∣ a * b → p ^ k ∣ a ∨ p ^ k ∣ b

Tactic:
simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb), Nat.factorization_mul ha hb,
    hp.pow_dvd_iff_le_factorization ha, hp.pow_dvd_iff_le_factorization hb, Pi.add_apply,
    Finsupp.coe_add]

Premises used: Nat.factorization_mul, Pi.add_apply, Finsupp.coe_add, Nat.Prime.pow_dvd_iff_le_factorization, mul_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
rw : p ∉ a.factorization.support ∩ b.factorization.support
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ∨
    Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rw [← Finsupp.notMem_support_iff, ← Finsupp.notMem_support_iff, ← not_and_or, ←
      Finset.mem_inter]

Premises used: Finsupp.notMem_support_iff, not_and_or, Finset.mem_inter
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
t : p ∈ a.factorization.support ∩ b.factorization.support
⊢ False

Tactic:
simpa using hab.disjoint_primeFactors.le_bot t

Premises used: Disjoint.le_bot, Nat.Coprime.disjoint_primeFactors
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ∨
    Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
have : a.factorization p = 0 ∨ b.factorization p = 0 := by
    rw [← Finsupp.notMem_support_iff, ← Finsupp.notMem_support_iff, ← not_and_or, ←
      Finset.mem_inter]
    intro t
    simpa using hab.disjoint_primeFactors.le_bot t
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
this :
  Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ∨
    Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
inr :
  ∀ (h : Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
      k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
inr₁ :
  ∀ (h : Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
      k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
⊢ k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
    k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p

Tactic:
rcases this with h | h
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
h : Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
    k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p

Tactic:
simp [h, imp_or]

Premises used: imp_or
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
h : Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
    k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p

Tactic:
simp [h, imp_or]

Premises used: imp_or
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
inl : ∀ (hab : Coprime 0 b), {d ∈ (0 * b).divisors | IsPrimePow d} = {d ∈ divisors 0 ∪ b.divisors | IsPrimePow d}
inr : ∀ (ha : a ≠ 0), {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
b : ℕ
hab : Coprime 0 b
⊢ b = 1

Tactic:
simp only [Nat.coprime_zero_left] at hab

Premises used: Nat.coprime_zero_left
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
b : ℕ
hab : b = 1
⊢ {d ∈ (0 * b).divisors | IsPrimePow d} = {d ∈ divisors 0 ∪ b.divisors | IsPrimePow d}

Tactic:
simp [hab, Finset.filter_singleton, not_isPrimePow_one]

Premises used: not_isPrimePow_one, Finset.filter_singleton
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
inr : ∀ (hab : a.Coprime 0), {d ∈ (a * 0).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ divisors 0 | IsPrimePow d}
inr₁ : ∀ (hb : b ≠ 0), {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a : ℕ
ha : a ≠ 0
hab : a.Coprime 0
⊢ a = 1

Tactic:
simp only [Nat.coprime_zero_right] at hab

Premises used: Nat.coprime_zero_right
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a : ℕ
ha : a ≠ 0
hab : a = 1
⊢ {d ∈ (a * 0).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ divisors 0 | IsPrimePow d}

Tactic:
simp [hab, Finset.filter_singleton, not_isPrimePow_one]

Premises used: not_isPrimePow_one, Finset.filter_singleton
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
inr : ∀ (n : ℕ), n ∈ {d ∈ (a * b).divisors | IsPrimePow d} ↔ n ∈ {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}

Tactic:
ext n
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
inr : IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)
⊢ n ∈ {d ∈ (a * b).divisors | IsPrimePow d} ↔ n ∈ {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}

Tactic:
simp only [ha, hb, Finset.mem_union, Finset.mem_filter, Nat.mul_eq_zero, and_true, Ne,
    and_congr_left_iff, not_false_iff, Nat.mem_divisors, or_self_iff]

Premises used: and_true, Nat.mem_divisors, or_self_iff, Ne, and_congr_left_iff, Finset.mem_filter, Finset.mem_union, not_false_iff, Nat.mul_eq_zero
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)

Tactic:
apply hab.isPrimePow_dvd_mul

Premises used: Nat.Coprime.isPrimePow_dvd_mul
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
x : Primes × ℕ
p : Primes
k : ℕ
⊢ (fun (n : { n : ℕ // IsPrimePow n }) ↦
        (Subtype.mk (p := fun (p : ℕ) ↦ Prime p) (↑n : ℕ).minFac ⋯,
          HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ)))
      ((fun (pk : Primes × ℕ) ↦
          (Subtype.mk (p := fun (n : ℕ) ↦ IsPrimePow n) ((↑pk.1 : ℕ) ^ (pk.2 + 1)) ⋯ : { n : ℕ // IsPrimePow n }))
        (p, k)) =
    (p, k)

Tactic:
simp only [p.prop.pow_minFac k.add_one_ne_zero, Subtype.coe_eta, factorization_pow, p.prop,
      Prime.factorization, Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.single_add,
      Finsupp.coe_add, Pi.add_apply, Finsupp.single_eq_same, add_tsub_cancel_right]

Premises used: Finsupp.single_eq_same, Nat.add_one_ne_zero, Nat.Prime.factorization, Pi.add_apply, Finsupp.coe_add, Finsupp.single_add, Subtype.coe_eta, Subtype.prop, Nat.Prime.pow_minFac, add_tsub_cancel_right, Nat.factorization_pow, smul_eq_mul, mul_one, Finsupp.smul_single
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : { n : ℕ // IsPrimePow n }
a :
  (↑((fun (pk : Primes × ℕ) ↦
            (Subtype.mk (p := fun (n : ℕ) ↦ IsPrimePow n) ((↑pk.1 : ℕ) ^ (pk.2 + 1)) ⋯ : { n : ℕ // IsPrimePow n }))
          ((fun (n : { n : ℕ // IsPrimePow n }) ↦
              (Subtype.mk (p := fun (p : ℕ) ↦ Prime p) (↑n : ℕ).minFac ⋯,
                HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ)))
            n)) :
      ℕ) =
    (↑n : ℕ)
⊢ (fun (pk : Primes × ℕ) ↦
        (Subtype.mk (p := fun (n : ℕ) ↦ IsPrimePow n) ((↑pk.1 : ℕ) ^ (pk.2 + 1)) ⋯ : { n : ℕ // IsPrimePow n }))
      ((fun (n : { n : ℕ // IsPrimePow n }) ↦
          (Subtype.mk (p := fun (p : ℕ) ↦ Prime p) (↑n : ℕ).minFac ⋯,
            HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ)))
        n) =
    n

Tactic:
ext1