awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a b : ℕ
⊢ Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1

Tactic:
simp only [irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]

Premises used: Nat.isUnit_iff, irreducible_mul_iff, Nat.irreducible_iff_nat_prime
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a b : ℕ
a1 : a ≠ 1
b1 : b ≠ 1
⊢ ¬Prime (a * b)

Tactic:
simp [prime_mul_iff, *]

Premises used: Nat.prime_mul_iff
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a b n : ℕ
h : a * b = n
h₁ : a ≠ 1
h₂ : b ≠ 1
⊢ ¬Prime n

Tactic:
h ▸ not_prime_mul h₁ h₂

Premises used: Eq.rec, Nat.not_prime_mul
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
a1 : p ≠ 1
⊢ p ∣ p

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p a : ℕ
hp : Prime p
a1 : a ≠ 1
refine : a ∣ p → p = a
⊢ a ∣ p ↔ p = a

Tactic:
refine ⟨?_, by rintro rfl; rfl⟩
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
inl : Prime a → ∀ (hp : Prime (a * 1)), a * 1 = a
inr : Prime j → ∀ (a1 : Ne (α := ℕ) 1 1) (hp : Prime (1 * j)), 1 * j = 1
⊢ a * j = a

Tactic:
rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)

Premises used: Nat.prime_mul_iff, Iff.mp, rfl
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a : ℕ
a1 : a ≠ 1
left : Prime a
hp : Prime (a * 1)
⊢ a * 1 = a

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a : ℕ
a1 : a ≠ 1
left : Prime a
hp : Prime (a * 1)
⊢ a * 1 = a

Tactic:
exact mul_one _

Premises used: mul_one
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
j : ℕ
left : Prime j
a1 : Ne (α := ℕ) 1 1
hp : Prime (1 * j)
⊢ 1 * j = 1

Tactic:
(a1 rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
j : ℕ
left : Prime j
a1 : Ne (α := ℕ) 1 1
hp : Prime (1 * j)
⊢ 1 * j = 1

Tactic:
exact (a1 rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
h : p % 2 = 0
⊢ ¬Eq (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
⊢ p = 2 ∨ Odd p

Tactic:
Or.imp_right (fun h => ⟨p / 2, (div_add_mod p 2).symm.trans (congr_arg _ h)⟩) hp.eq_two_or_odd

Premises used: Nat.Prime.eq_two_or_odd, HMul.hMul, Nat.div_add_mod, HDiv.hDiv, congr_arg, HAdd.hAdd, Exists.intro, OfNat.ofNat, Eq.symm, Or.imp_right, Eq.trans
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
by_contra! : ∀ (h : p < 5), False
⊢ 5 ≤ p

Tactic:
by_contra! h
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
h : p < 5
revert : ∀ (hp : Prime p) (h_two : p ≠ 2) (h_three : p ≠ 3), False
⊢ False

Tactic:
revert h_two h_three hp
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
h : p < 5
⊢ ∀ (hp : Prime p) (h_two : p ≠ 2) (h_three : p ≠ 3), False

Tactic:
decide +revert
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
pp : Prime p
⊢ 0 < p.pred

Tactic:
lt_pred_iff.2 pp.one_lt

Premises used: Iff.mpr, Nat.lt_pred_iff, Nat.Prime.one_lt
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
pp : Prime p
⊢ p.pred.succ = p

Tactic:
succ_pred_eq_of_pos pp.pos

Premises used: Nat.succ_pred_eq_of_pos, Nat.Prime.pos
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
n2 : 2 ≤ n
np : ¬Prime n
⊢ ∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n

Tactic:
⟨minFac n, minFac_dvd _, ne_of_gt (minFac_prime (ne_of_gt n2)).one_lt,
    ne_of_lt <| (not_prime_iff_minFac_lt n2).1 np⟩

Premises used: Nat.Prime.one_lt, Nat.minFac, Nat.minFac_dvd, Nat.not_prime_iff_minFac_lt, And.intro, Exists.intro, Iff.mp, Nat.ne_of_lt, Nat.minFac_prime, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
n2 : 2 ≤ n
np : ¬Prime n
⊢ ∃ (m : ℕ), m ∣ n ∧ 2 ≤ m ∧ m < n

Tactic:
⟨minFac n, minFac_dvd _, (minFac_prime (ne_of_gt n2)).two_le,
    (not_prime_iff_minFac_lt n2).1 np⟩

Premises used: Nat.minFac, Nat.minFac_dvd, Nat.not_prime_iff_minFac_lt, And.intro, Exists.intro, Iff.mp, Nat.Prime.two_le, Nat.minFac_prime, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
m n : ℕ
h1 : m ∣ n
h2 : m ≠ 1
h3 : m ≠ n
⊢ ¬Prime n

Tactic:
fun h => Or.elim (h.eq_one_or_self_of_dvd m h1) h2 h3

Premises used: Nat.Prime.eq_one_or_self_of_dvd, Or.elim, Not
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
m n : ℕ
h1 : m ∣ n
h2 : 2 ≤ m
h3 : m < n
⊢ ¬Prime n

Tactic:
not_prime_of_dvd_of_ne h1 (ne_of_gt h2) (ne_of_lt h3)

Premises used: Nat.not_prime_of_dvd_of_ne, Nat.ne_of_lt, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
h : 2 ≤ n
⊢ ¬Prime n ↔ ∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n

Tactic:
⟨exists_dvd_of_not_prime h, fun ⟨_, h1, h2, h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩

Premises used: Nat.Prime, Nat.exists_dvd_of_not_prime, Nat.not_prime_of_dvd_of_ne, Iff.intro, _private.0.Nat.not_prime_iff_exists_dvd_ne.match_1, Not
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
h : 2 ≤ n
⊢ ¬Prime n ↔ ∃ (m : ℕ), m ∣ n ∧ 2 ≤ m ∧ m < n

Tactic:
⟨exists_dvd_of_not_prime2 h, fun ⟨_, h1, h2, h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩

Premises used: Nat.Prime, Nat.not_prime_of_dvd_of_lt, _private.0.Nat.not_prime_iff_exists_dvd_lt.match_1, Iff.intro, Nat.exists_dvd_of_not_prime2, Not
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
h : 2 ≤ n
rw : ¬(2 ≤ n ∧ ¬∃ (m : ℕ), ∃ (n_1 : ℕ), m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
rw₁ : (¬¬∃ (m : ℕ), ∃ (n_1 : ℕ), m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
rw₂ rw₃ : (∃ (m : ℕ), ∃ (n_1 : ℕ), m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
⊢ ¬Prime n ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n

Tactic:
rw [prime_iff_not_exists_mul_eq, and_iff_right h, Classical.not_not]

Premises used: Classical.not_not, and_iff_right, Nat.prime_iff_not_exists_mul_eq
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
inl : ∀ (hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b), 1 ∣ b
inr : ∀ (ha : a ≠ 1), a ∣ b
⊢ a ∣ b

Tactic:
obtain rfl | ha := eq_or_ne a 1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b
⊢ 1 ∣ b

Tactic:
apply one_dvd

Premises used: one_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
inr : ∀ (p : ℕ) (hp : Prime p ∧ p ∣ a), a ∣ b
⊢ a ∣ b

Tactic:
obtain ⟨p, hp⟩ := exists_prime_and_dvd ha

Premises used: Nat.exists_prime_and_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b

Tactic:
_root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)

Premises used: trans, dvd_mul_left, And.right, And.left
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b

Tactic:
exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)

Premises used: trans, dvd_mul_left, And.right, And.left
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
rw : 2 ∣ p ↔ p = 2
rw₁ : 2 = p ↔ p = 2
rw₂ rw₃ : p = 2 ↔ p = 2
⊢ Even p ↔ p = 2

Tactic:
rw [even_iff_two_dvd, prime_dvd_prime_iff_eq prime_two hp, eq_comm]

Premises used: Nat.prime_dvd_prime_iff_eq, eq_comm, Nat.prime_two, even_iff_two_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
rw : p = 2 ↔ p < 3
⊢ Odd p ↔ 3 ≤ p

Tactic:
rw [← not_iff_not, not_odd_iff_even, hp.even_iff, not_le]

Premises used: not_le, not_iff_not, Nat.Prime.even_iff, Nat.not_odd_iff_even
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
⊢ p = 2 ↔ p < 3

Tactic:
grind [hp.two_le]

Premises used: Nat.Prime.two_le
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
h_two : p ≠ 2
⊢ Odd p

Tactic:
hp.eq_two_or_odd'.resolve_left h_two

Premises used: Or.resolve_left, Nat.Prime.eq_two_or_odd'
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
rw : 2 * n + 1 - 1 = n + n
rw₁ : 2 * n = n + n
rw₂ rw₃ : n + n = n + n
⊢ p - 1 = n + n

Tactic:
rw [hn, Nat.add_sub_cancel, two_mul]

Premises used: two_mul, Nat.add_sub_cancel
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
⊢ p % 2 = 1 ↔ p ≠ 2

Tactic:
⟨fun h hf => ?_, hp.eq_two_or_odd.resolve_left⟩

Premises used: Nat.Prime.eq_two_or_odd, Or.resolve_left, Iff.intro
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
refine : ∀ (h : p % 2 = 1) (hf : p = 2), False
⊢ p % 2 = 1 ↔ p ≠ 2

Tactic:
refine ⟨fun h hf => ?_, hp.eq_two_or_odd.resolve_left⟩
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
h : p % 2 = 1
hf : p = 2
⊢ HMod.hMod (α := ℕ) 2 2 = 1

Tactic:
rw [hf] at h
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
h : p % 2 = 1
hf : p = 2
h₁ : HMod.hMod (α := ℕ) 2 2 = 1
⊢ p = 2

Tactic:
rw [hf] at h
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
hp : Prime p
h : HMod.hMod (α := ℕ) 2 2 = 1
hf : p = 2
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → k ∣ n → k ∣ 1
⊢ m.Coprime n

Tactic:
coprime_of_dvd fun k kp km kn => not_le_of_gt kp.one_lt <| le_of_dvd Nat.one_pos <| H k kp km kn

Premises used: Nat.one_pos, Nat.Prime.one_lt, Nat.coprime_of_dvd, not_le_of_gt, Nat.le_of_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p n : ℕ
pp : Prime p
⊢ p ∣ n ↔ ¬p.Coprime n

Tactic:
iff_not_comm.2 pp.coprime_iff_not_dvd

Premises used: Iff.mpr, iff_not_comm, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
m n : ℕ
mp : ¬m.Coprime n → ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n
mpr : (∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n) → ¬m.Coprime n
⊢ ¬m.Coprime n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
apply Iff.intro

Premises used: Iff.intro
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
m n : ℕ
h : ¬m.Coprime n
⊢ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
        (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩

Premises used: Nat.gcd, Nat.gcd_dvd_left, Nat.minFac, Nat.minFac_dvd, And.intro, Exists.intro, Nat.gcd_dvd_right, Nat.minFac_prime, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
m n : ℕ
h : ¬m.Coprime n
⊢ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
exact
      ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
        (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
m n : ℕ
h : ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n
mpr : ∀ (p : ℕ) (hp : Prime p ∧ p ∣ m ∧ p ∣ n), ¬m.Coprime n
⊢ ¬m.Coprime n

Tactic:
obtain ⟨p, hp⟩ := h
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
m n p : ℕ
hp : Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n

Tactic:
apply Nat.not_coprime_of_dvd_of_dvd (Prime.one_lt hp.1) hp.2.1 hp.2.2

Premises used: Nat.Prime.one_lt, Nat.not_coprime_of_dvd_of_dvd, And.right, And.left
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
rw : ¬∃ (p : ℕ), Prime p ∧ p ∣ n ∧ p ∣ m
⊢ n.Coprime m

Tactic:
rw [← not_not (a := n.Coprime m), Prime.not_coprime_iff_dvd]

Premises used: Classical.not_not, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
push : ∀ (p : ℕ) (_ : Prime p) (_ : p ∣ n), ¬p ∣ m
⊢ ¬∃ (p : ℕ), Prime p ∧ p ∣ n ∧ p ∣ m

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
p : ℕ
hp : Prime p
hn : p ∣ n
hm : p ∣ m
⊢ 0 < m

Tactic:
lia
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ ∀ (p : ℕ) (_ : Prime p) (_ : p ∣ n), ¬p ∣ m

Tactic:
exact fun p hp hn hm ↦
    ((le_of_dvd (by lia) hm).trans_lt <| h.trans_le <| minFac_le_of_dvd hp.two_le hn).false

Premises used: Nat.minFac_le_of_dvd, LT.lt.trans_le, LT.lt.false, LE.le.trans_lt, Nat.le_of_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ n.gcd m = 1

Tactic:
coprime_iff_gcd_eq_one.mp <| coprime_of_lt_minFac h₀ h

Premises used: Nat.coprime_of_lt_minFac, Nat.coprime_iff_gcd_eq_one, Iff.mp
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p m n : ℕ
pp : Prime p
Hm : ¬p ∣ m
Hn : ¬p ∣ n
⊢ ¬(p ∣ m ∨ p ∣ n)

Tactic:
simp [Hm, Hn]
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
rw : ¬2 ∣ n ↔ Odd n
rw₁ : ¬2 ∣ n ↔ ¬Even n
rw₂ rw₃ : ¬2 ∣ n ↔ ¬2 ∣ n
⊢ Coprime 2 n ↔ Odd n

Tactic:
rw [prime_two.coprime_iff_not_dvd, ← not_even_iff_odd, even_iff_two_dvd]

Premises used: Nat.not_even_iff_odd, Nat.prime_two, even_iff_two_dvd, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
⊢ n.Coprime 2 ↔ Odd n

Tactic:
coprime_comm.trans coprime_two_left

Premises used: Nat.coprime_two_left, Nat.coprime_comm, Iff.trans
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p m n : ℕ
pp : Prime p
h : p ∣ m ^ n
⊢ p ∣ m

Tactic:
pp.prime.dvd_of_dvd_pow h

Premises used: Nat.Prime.prime, Prime.dvd_of_dvd_pow
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x n : ℕ
hn : n ≠ 1
⊢ ¬Prime (x ^ n)

Tactic:
not_irreducible_pow hn

Premises used: Nat.Prime, not_irreducible_pow
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x n : ℕ
hn : 2 ≤ n
⊢ ¬Prime (x ^ n)

Tactic:
not_prime_pow' ((two_le_iff _).mp hn).2

Premises used: Nat.two_le_iff, Nat.Prime.not_prime_pow', And.right, Iff.mp
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x n : ℕ
h : Prime (x ^ n)
⊢ n = 1

Tactic:
not_imp_not.mp Prime.not_prime_pow' h

Premises used: Nat.Prime.not_prime_pow', Iff.mp, not_imp_not
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
rw : p ^ k = p
rw₁ : HPow.hPow (β := ℕ) p 1 = p
rw₂ rw₃ : p = p
⊢ a ^ k = p

Tactic:
rw [h.1, h.2, pow_one]

Premises used: And.right, And.left, pow_one
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p a k : ℕ
hp : Prime p
refine : ∀ (h : a ^ k = p), a = p ∧ k = 1
⊢ a ^ k = p ↔ a = p ∧ k = 1

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h.1, h.2, pow_one]⟩
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p a k : ℕ
hp : Prime p
h : a ^ k = p
⊢ Prime (a ^ k)

Tactic:
rw [← h] at hp
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p a k : ℕ
hp : Prime p
h : a ^ k = p
hp₁ : Prime (a ^ k)
⊢ a ^ k = p

Tactic:
rw [← h] at hp
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
rw : a = a ^ k ∧ k = 1
rw₁ : a = HPow.hPow (β := ℕ) a 1 ∧ Eq (α := ℕ) 1 1
rw₂ : a = HPow.hPow (β := ℕ) a 1 ∧ True
rw₃ : a = HPow.hPow (β := ℕ) a 1
rw₄ rw₅ : a = a
⊢ a = p ∧ k = 1

Tactic:
rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]

Premises used: and_true, Nat.Prime.eq_one_of_pow, pow_one, eq_self_iff_true
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
⊢ x * y = HPow.hPow (β := ℕ) p 2 ↔ x = p ∧ y = p

Tactic:
⟨fun h => ?_, fun ⟨h₁, h₂⟩ => h₁.symm ▸ h₂.symm ▸ (sq _).symm⟩

Premises used: HMul.hMul, Eq.rec, sq, HPow.hPow, Iff.intro, _private.0.Nat.Prime.mul_eq_prime_sq_iff.match_1, OfNat.ofNat, Eq.symm, Eq
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
refine : ∀ (h : x * y = HPow.hPow (β := ℕ) p 2), x = p ∧ y = p
⊢ x * y = HPow.hPow (β := ℕ) p 2 ↔ x = p ∧ y = p

Tactic:
refine ⟨fun h => ?_, fun ⟨h₁, h₂⟩ => h₁.symm ▸ h₂.symm ▸ (sq _).symm⟩
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
rw : p ∣ HPow.hPow (β := ℕ) p 2
⊢ p ∣ x * y

Tactic:
rw [h]
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
⊢ p ∣ HPow.hPow (β := ℕ) p 2

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
⊢ p ∣ x * y

Tactic:
have pdvdxy : p ∣ x * y := by rw [h]; simp [sq]
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
inl : ∀ (hx : p ∣ x), x = p ∧ y = p
inr : ∀ (hy : p ∣ y), x = p ∧ y = p
⊢ x = p ∧ y = p

Tactic:
obtain hx | hy := hp.dvd_mul.1 pdvdxy

Premises used: Iff.mp, Nat.Prime.dvd_mul
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
inr : y = p ∧ x = p
⊢ x = p ∧ y = p

Tactic:
rw [And.comm]

Premises used: And.comm
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
inl : ∀ (hx : p ∣ x), x = p ∧ y = p
inr : ∀ (hy : p ∣ y), y = p ∧ x = p
⊢ x = p ∧ y = p

Tactic:
obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]]

Premises used: And.comm, Iff.mp, Nat.Prime.dvd_mul
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y * x = HPow.hPow (β := ℕ) p 2

Tactic:
rw [mul_comm] at h pdvdxy

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
h₁ : y * x = HPow.hPow (β := ℕ) p 2
⊢ p ∣ y * x

Tactic:
rw [mul_comm] at h pdvdxy

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
h₁ : y * x = HPow.hPow (β := ℕ) p 2
pdvdxy₁ : p ∣ y * x
⊢ ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p

Tactic:
rw [mul_comm] at h pdvdxy

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
h₁ : y * x = HPow.hPow (β := ℕ) p 2
pdvdxy₁ : p ∣ y * x
this₁ : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
⊢ p ∣ y

Tactic:
rw [mul_comm] at h pdvdxy

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
inl : ∀ (hx : p ∣ x), x = p ∧ y = p
inr :
  ∀ (h : y * x = HPow.hPow (β := ℕ) p 2) (pdvdxy : p ∣ y * x)
    (this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p) (hy : p ∣ y),
    y = p ∧ x = p
⊢ x = p ∧ y = p

Tactic:
obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]] <;>
      [skip; rw [mul_comm] at h pdvdxy]

Premises used: And.comm, Iff.mp, mul_comm, Nat.Prime.dvd_mul
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx_1 : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
inl : x ≠ 1
inl₁ : y ≠ 1
inl₂ : x * y = HPow.hPow (β := ℕ) p 2
inl₃ : p ∣ x
⊢ x = p ∧ y = p

Tactic:
apply this
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : y * x = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
inr : y ≠ 1
inr₁ : x ≠ 1
inr₂ : y * x = HPow.hPow (β := ℕ) p 2
inr₃ : p ∣ y
⊢ y = p ∧ x = p

Tactic:
apply this
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx_1 : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x ≠ 1

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx_1 : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ y ≠ 1

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx_1 : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x * y = HPow.hPow (β := ℕ) p 2

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx_1 : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ p ∣ x

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : y * x = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y ≠ 1

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : y * x = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ x ≠ 1

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : y * x = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y * x = HPow.hPow (β := ℕ) p 2

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy_1 : y ≠ 1
h : y * x = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ p ∣ y

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
suffices : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p

Tactic:
suffices ∀ x' y' : ℕ, x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p by
    obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]] <;>
      [skip; rw [mul_comm] at h pdvdxy] <;>
      apply this <;>
      assumption
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x_1 y_1 p : ℕ
hp : Prime p
hx_1 : x_1 ≠ 1
hy_1 : y_1 ≠ 1
h_1 : x_1 * y_1 = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x_1 * y_1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
a : ℕ
ha : x = p * a
rwa : ∀ (h : p * a * y = HPow.hPow (β := ℕ) p 2) (ha : x = p * a), p = a * y
rwa₁ : ∀ (h : p * a * y = p * p) (ha : x = p * a), p = a * y
rwa₂ : ∀ (h : p * (a * y) = p * p) (ha : x = p * a), p = a * y
rwa₃ : ∀ (h : a * y = p) (ha : x = p * a), p = a * y
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (h : p = a * y) (ha : x = p * a), p = a * y
⊢ p = a * y

Tactic:
rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h

Premises used: mul_assoc, sq, eq_comm, Nat.Prime.ne_zero, mul_right_inj'
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x_1 y_1 p : ℕ
hp : Prime p
hx_1 : x_1 ≠ 1
hy_1 : y_1 ≠ 1
h_1 : x_1 * y_1 = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x_1 * y_1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
a : ℕ
ha : x = p * a
⊢ a ∣ p

Tactic:
have : a ∣ p := ⟨y, by rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h⟩