awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : a ∣ p
inl : ∀ (ha : x = p * 1) (this : 1 ∣ p), x = p ∧ y = p
inr : ∀ (hap : a = p), x = p ∧ y = p
⊢ x = p ∧ y = p

Tactic:
obtain rfl | hap := (Nat.dvd_prime hp).mp ‹a ∣ p›

Premises used: Nat.dvd_prime, Iff.mp, rfl
-- 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
ha : x = p * 1
this : 1 ∣ p
⊢ x = p

Tactic:
rw [mul_one] at ha

Premises used: mul_one
-- 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
ha : x = p * 1
this : 1 ∣ p
ha₁ : x = p
⊢ 1 ∣ p

Tactic:
rw [mul_one] at ha

Premises used: mul_one
-- 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
ha : x = p
this : 1 ∣ p
inl :
  ∀ (hp : Prime x) (h : x_1 * y_1 = HPow.hPow (β := ℕ) x 2) (pdvdxy : x ∣ x_1 * y_1)
    (h : x * y = HPow.hPow (β := ℕ) x 2) (this : 1 ∣ x), x = x ∧ y = x
⊢ x = p ∧ y = p

Tactic:
subst ha
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x_1 y_1 : ℕ
hx_1 : x_1 ≠ 1
hy_1 : y_1 ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
hp : Prime x
h_1 : x_1 * y_1 = HPow.hPow (β := ℕ) x 2
pdvdxy : x ∣ x_1 * y_1
h : x * y = HPow.hPow (β := ℕ) x 2
this : 1 ∣ x
⊢ y = x

Tactic:
simp only [sq, mul_right_inj' hp.ne_zero] at h

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

Tactic:
subst h
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y_1 : ℕ
hx_1 : x ≠ 1
hy_1 : y_1 ≠ 1
y : ℕ
hy hx : y ≠ 1
hp : Prime y
h : x * y_1 = HPow.hPow (β := ℕ) y 2
pdvdxy : y ∣ x * y_1
this : 1 ∣ y
⊢ y = y ∧ y = y

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y_1 : ℕ
hx_1 : x ≠ 1
hy_1 : y_1 ≠ 1
y : ℕ
hy hx : y ≠ 1
hp : Prime y
h : x * y_1 = HPow.hPow (β := ℕ) y 2
pdvdxy : y ∣ x * y_1
this : 1 ∣ y
⊢ y = y ∧ y = y

Tactic:
exact ⟨rfl, rfl⟩
-- 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
this : a ∣ p
hap : a = p
⊢ x = p ∧ y = p

Tactic:
(hy ?_).elim

Premises used: False.elim
-- 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
this : a ∣ p
hap : a = p
inr : y = 1
⊢ x = p ∧ y = p

Tactic:
refine (hy ?_).elim

Premises used: False.elim
-- 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
this : a ∣ p
hap : a = p
⊢ Prime a

Tactic:
subst hap
-- 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
this : a ∣ p
hap : a = p
hp₁ : Prime a
⊢ x_1 * y_1 = HPow.hPow (β := ℕ) a 2

Tactic:
subst hap
-- 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
this : a ∣ p
hap : a = p
hp₁ : Prime a
h₁ : x_1 * y_1 = HPow.hPow (β := ℕ) a 2
⊢ a ∣ x_1 * y_1

Tactic:
subst hap
-- 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
this : a ∣ p
hap : a = p
hp₁ : Prime a
h₁ : x_1 * y_1 = HPow.hPow (β := ℕ) a 2
pdvdxy₁ : a ∣ x_1 * y_1
⊢ x * y = HPow.hPow (β := ℕ) a 2

Tactic:
subst hap
-- 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
this : a ∣ p
hap : a = p
hp₁ : Prime a
h₁ : x_1 * y_1 = HPow.hPow (β := ℕ) a 2
pdvdxy₁ : a ∣ x_1 * y_1
h₂ : x * y = HPow.hPow (β := ℕ) a 2
⊢ x = a * a

Tactic:
subst hap
-- 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
this : a ∣ p
hap : a = p
hp₁ : Prime a
h₁ : x_1 * y_1 = HPow.hPow (β := ℕ) a 2
pdvdxy₁ : a ∣ x_1 * y_1
h₂ : x * y = HPow.hPow (β := ℕ) a 2
ha₁ : x = a * a
⊢ a ∣ a

Tactic:
subst hap
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x_1 y_1 : ℕ
hx_1 : x_1 ≠ 1
hy_1 : y_1 ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
a : ℕ
hp : Prime a
h_1 : x_1 * y_1 = HPow.hPow (β := ℕ) a 2
pdvdxy : a ∣ x_1 * y_1
h : x * y = HPow.hPow (β := ℕ) a 2
ha : x = a * a
this : a ∣ a
⊢ a * a ≠ 1

Tactic:
subst ha
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x_1 y_1 : ℕ
hx_1 : x_1 ≠ 1
hy_1 : y_1 ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
a : ℕ
hp : Prime a
h_1 : x_1 * y_1 = HPow.hPow (β := ℕ) a 2
pdvdxy : a ∣ x_1 * y_1
h : x * y = HPow.hPow (β := ℕ) a 2
ha : x = a * a
this : a ∣ a
hx₁ : a * a ≠ 1
⊢ a * a * y = HPow.hPow (β := ℕ) a 2

Tactic:
subst ha
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y_1 : ℕ
hx_1 : x ≠ 1
hy_1 : y_1 ≠ 1
y : ℕ
hy : y ≠ 1
a : ℕ
hp : Prime a
h_1 : x * y_1 = HPow.hPow (β := ℕ) a 2
pdvdxy : a ∣ x * y_1
this : a ∣ a
hx : a * a ≠ 1
h : a * a * y = HPow.hPow (β := ℕ) a 2
⊢ y = 1

Tactic:
rw [sq, Nat.mul_eq_left (Nat.mul_ne_zero hp.ne_zero hp.ne_zero)] at h

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

Tactic:
h
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
x y_1 : ℕ
hx_1 : x ≠ 1
hy_1 : y_1 ≠ 1
y : ℕ
hy : y ≠ 1
a : ℕ
hp : Prime a
h_1 : x * y_1 = HPow.hPow (β := ℕ) a 2
pdvdxy : a ∣ x * y_1
this : a ∣ a
hx : a * a ≠ 1
h : y = 1
⊢ y = 1

Tactic:
exact h
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p m a : ℕ
pp : Prime p
h : ¬p ∣ a
⊢ a.Coprime (p ^ m)

Tactic:
(pp.coprime_iff_not_dvd.2 h).symm.pow_right _

Premises used: Iff.mpr, Nat.Coprime.symm, Nat.Coprime.pow_right, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p q : ℕ
pp : Prime p
pq : Prime q
⊢ p.Coprime q ↔ p ≠ q

Tactic:
pp.coprime_iff_not_dvd.trans <| not_congr <| dvd_prime_two_le pq pp.two_le

Premises used: Nat.dvd_prime_two_le, Iff.trans, Nat.Prime.two_le, Nat.Prime.coprime_iff_not_dvd, not_congr
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p q n m : ℕ
pp : Prime p
pq : Prime q
h : p ≠ q
⊢ (p ^ n).Coprime (q ^ m)

Tactic:
((coprime_primes pp pq).2 h).pow _ _

Premises used: Iff.mpr, Nat.Coprime.pow, Nat.coprime_primes
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
pp : Prime p
i : ℕ
rw : p.Coprime i ∨ ¬p.Coprime i
⊢ p.Coprime i ∨ p ∣ i

Tactic:
rw [pp.dvd_iff_not_coprime]

Premises used: Nat.Prime.dvd_iff_not_coprime
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
pp : Prime p
i : ℕ
⊢ p.Coprime i ∨ ¬p.Coprime i

Tactic:
apply em

Premises used: em
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n p : ℕ
ne_zero : n ≠ 0
hlt : n < p
pp : Prime p
⊢ p.Coprime n

Tactic:
(coprime_or_dvd_of_prime pp n).resolve_right fun h => Nat.lt_le_asymm hlt
    (le_of_dvd (Nat.pos_of_ne_zero ne_zero) h)

Premises used: Nat.pos_of_ne_zero, Nat.lt_le_asymm, Or.resolve_right, Nat.le_of_dvd, Nat.coprime_or_dvd_of_prime
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n p : ℕ
ne_zero : n ≠ 0
hle : n ≤ p
pp : Prime p
⊢ p = n ∨ p.Coprime n

Tactic:
hle.eq_or_lt.imp Eq.symm fun h => coprime_of_lt_prime ne_zero h pp

Premises used: LE.le.eq_or_lt, Nat.coprime_of_lt_prime, Or.imp, Eq.symm
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
m p q : ℕ
pp : Prime p
pq : Prime q
h : p ∣ q ^ m
⊢ p = q

Tactic:
(prime_dvd_prime_iff_eq pp pq).mp (pp.dvd_of_dvd_pow h)

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.prime_dvd_prime_iff_eq, Iff.mp
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
pp : Prime p
m i : ℕ
simp_rw : (∃ (i_1 : ℕ), i_1 ≤ m ∧ Associated i (p ^ i_1)) ↔ ∃ (k : ℕ), k ≤ m ∧ i = p ^ k
⊢ i ∣ p ^ m ↔ ∃ (k : ℕ), k ≤ m ∧ i = p ^ k

Tactic:
simp_rw [_root_.dvd_prime_pow (prime_iff.mp pp) m, associated_eq_eq]

Premises used: associated_eq_eq, Nat.prime_iff, Iff.mp, dvd_prime_pow
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p1 p2 n : ℕ
h_ne : p1 ≠ p2
pp1 : Prime p1
pp2 : Prime p2
h1 : p1 ∣ n
h2 : p2 ∣ n
⊢ p1 * p2 ∣ n

Tactic:
Coprime.mul_dvd_of_dvd_of_dvd ((coprime_primes pp1 pp2).mpr h_ne) h1 h2

Premises used: Iff.mpr, Nat.Coprime.mul_dvd_of_dvd_of_dvd, Nat.coprime_primes
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
a p k : ℕ
pp : Prime p
h₁ : ¬a ∣ p ^ k
h₂ : a ∣ p ^ (k + 1)
obtain : ∀ (l : ℕ) (h : l ≤ k + 1) (h₁ : ¬p ^ l ∣ p ^ k) (h₂ : p ^ l ∣ p ^ (k + 1)), p ^ l = p ^ (k + 1)
⊢ a = p ^ (k + 1)

Tactic:
obtain ⟨l, ⟨h, rfl⟩⟩ := (dvd_prime_pow pp).1 h₂

Premises used: Iff.mp, rfl, Nat.dvd_prime_pow
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
e_a : l = k + 1
⊢ p ^ l = p ^ (k + 1)

Tactic:
congr
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1

Tactic:
le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (Prime.one_lt pp))).1 h₁))

Premises used: not_le, Nat.Prime.one_lt, Nat.pow_dvd_pow_iff_le_right, le_antisymm, Iff.mp, not_congr
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1

Tactic:
exact le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (Prime.one_lt pp))).1 h₁))

Premises used: not_le, Nat.Prime.one_lt, Nat.pow_dvd_pow_iff_le_right, le_antisymm, Iff.mp, not_congr
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
⊢ Ne (α := ℕ) 0 1 ↔ ∃ (p : ℕ), Prime p ∧ p ∣ 0

Tactic:
simpa using Exists.intro 2 Nat.prime_two

Premises used: Nat.prime_two, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
⊢ Ne (α := ℕ) 1 1 ↔ ∃ (p : ℕ), Prime p ∧ p ∣ 1

Tactic:
simp [Nat.not_prime_one]

Premises used: Nat.not_prime_one
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
a : ℕ := n + 2
⊢ a ≠ 1

Tactic:
have ha : a ≠ 1 := Nat.succ_succ_ne_one n
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1
simp : ∃ (p : ℕ), Prime p ∧ p ∣ n + 2
⊢ n + 2 ≠ 1 ↔ ∃ (p : ℕ), Prime p ∧ p ∣ n + 2

Tactic:
simp only [a, true_iff, Ne, not_false_iff, ha]

Premises used: true_iff, Ne, not_false_iff
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1
⊢ ∃ (p : ℕ), Prime p ∧ p ∣ n + 2

Tactic:
⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩

Premises used: Nat.minFac, Nat.minFac_dvd, And.intro, Exists.intro, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1
⊢ ∃ (p : ℕ), Prime p ∧ p ∣ n + 2

Tactic:
exact ⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
n : ℕ
⊢ n = 1 ↔ ∀ (p : ℕ), Prime p → ¬p ∣ n

Tactic:
simpa using not_iff_not.mpr ne_one_iff_exists_prime_dvd

Premises used: not_iff_not, Iff.mpr, Nat.ne_one_iff_exists_prime_dvd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpmn' : p ^ (k + l).succ ∣ m * n := hpmn
rwa rwa₁ rwa₂ rwa₃ : ∀ (hpmn' : p * p ^ (k + l) ∣ m * n), p ^ (k + l) * p ∣ m * n
⊢ p ^ (k + l) * p ∣ m * n

Tactic:
rwa [pow_succ'] at hpmn'

Premises used: Nat.pow_succ'
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + l) * p ∣ m * n

Tactic:
have hpd : p ^ (k + l) * p ∣ m * n := by
      let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
      rwa [pow_succ'] at hpmn'
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
⊢ p ∣ m * n / p ^ (k + l)

Tactic:
have hpd2 : p ∣ m * n / p ^ (k + l) := dvd_div_of_mul_dvd hpd
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
⊢ p ∣ m * n / (p ^ k * p ^ l)

Tactic:
simpa [pow_add] using hpd2

Premises used: pow_add
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
⊢ p ∣ m * n / (p ^ k * p ^ l)

Tactic:
have hpd3 : p ∣ m * n / (p ^ k * p ^ l) := by simpa [pow_add] using hpd2
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
⊢ p ∣ m / p ^ k * (n / p ^ l)

Tactic:
simpa [Nat.div_mul_div_comm hpm hpn] using hpd3

Premises used: Nat.div_mul_div_comm
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
⊢ p ∣ m / p ^ k * (n / p ^ l)

Tactic:
have hpd4 : p ∣ m / p ^ k * (n / p ^ l) := by simpa [Nat.div_mul_div_comm hpm hpn] using hpd3
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
⊢ p ∣ m / p ^ k ∨ p ∣ n / p ^ l

Tactic:
have hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l :=
    (Prime.dvd_mul p_prime).1 hpd4
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
this : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
rwa : p ^ k * p ∣ m ∨ p ^ (l + 1) ∣ n
rwa₁ rwa₂ rwa₃ rwa₄ : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
rwa [_root_.pow_succ, _root_.pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
suffices : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
suffices p ^ k * p ∣ m ∨ p ^ l * p ∣ n by rwa [_root_.pow_succ, _root_.pow_succ]
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
⊢ p ^ k * p ∣ m ∨ p ^ l * p ∣ n

Tactic:
hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h)
    fun h : p ∣ n / p ^ l => Or.inr <| mul_dvd_of_dvd_div hpn h

Premises used: Nat.mul_dvd_of_dvd_div, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Data.Nat.Prime.Basic
Goal:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
⊢ p ^ k * p ∣ m ∨ p ^ l * p ∣ n

Tactic:
exact hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h)
    fun h : p ∣ n / p ^ l => Or.inr <| mul_dvd_of_dvd_div hpn h

Premises used: Nat.mul_dvd_of_dvd_div, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
a : ℕ
⊢ Irreducible a ↔ Prime a

Tactic:
Iff.rfl

Premises used: Nat.Prime, Iff.rfl
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ Prime 0 → False

Tactic:
not_prime_zero

Premises used: Nat.not_prime_zero, Not
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ Prime 1 → False

Tactic:
not_prime_one

Premises used: Nat.not_prime_one, Not
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : Prime n
⊢ n ≠ 0

Tactic:
Irreducible.ne_zero h

Premises used: Irreducible.ne_zero
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
pp : Prime p
⊢ 0 < p

Tactic:
Nat.pos_of_ne_zero pp.ne_zero

Premises used: Nat.pos_of_ne_zero, Nat.Prime.ne_zero
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
⊢ Prime p → 1 < p

Tactic:
Prime.two_le

Premises used: Nat.Prime.two_le, Nat.lt
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp : Prime p
⊢ 1 ≤ p

Tactic:
hp.one_lt.le

Premises used: Nat.Prime.one_lt, LT.lt.le
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n p : ℕ
hp : Fact (Prime p)
⊢ Fact (1 < p)

Tactic:
⟨hp.1.one_lt⟩

Premises used: Nat.Prime.one_lt, Fact.mk, Fact.out
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp : Prime p
⊢ p ≠ 1

Tactic:
hp.one_lt.ne'

Premises used: Nat.Prime.one_lt, LT.lt.ne'
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
pp : Prime p
m : ℕ
hm : m ∣ p
obtain : ∀ (n : ℕ) (hn : p = m * n), m = 1 ∨ m = p
⊢ m = 1 ∨ m = p

Tactic:
obtain ⟨n, hn⟩ := hm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
⊢ IsUnit m ∨ IsUnit n

Tactic:
have := pp.isUnit_or_isUnit hn
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : IsUnit m ∨ IsUnit n
⊢ m = 1 ∨ n = 1

Tactic:
rw [Nat.isUnit_iff, Nat.isUnit_iff] at this

Premises used: Nat.isUnit_iff
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
apply : n = 1 → m = p
⊢ m = 1 ∨ m = p

Tactic:
apply Or.imp_right _ this

Premises used: Or.imp_right
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ Eq (α := ℕ) 1 1
rw : m = m * 1
rw₁ rw₂ : m = m
⊢ m = p

Tactic:
rw [hn, mul_one]

Premises used: mul_one
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p

Tactic:
⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => ?_⟩

Premises used: Nat.Prime.eq_one_or_self_of_dvd, And.intro, Iff.intro, Nat.Prime.two_le
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
refine : ∀ (h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p), Prime p
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p

Tactic:
refine ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => ?_⟩
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ 1 < p

Tactic:
have h1 := Nat.one_lt_two.trans_le h.1
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ Prime p

Tactic:
⟨mt Nat.isUnit_iff.mp h1.ne', ?_⟩

Premises used: Nat.Prime, mt, Irreducible.mk, LT.lt.ne', Nat.isUnit_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
refine : ∀ ⦃a b : ℕ⦄, p = a * b → IsUnit a ∨ IsUnit b
⊢ Prime p

Tactic:
refine ⟨mt Nat.isUnit_iff.mp h1.ne', ?_⟩
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
simp : a = 1 ∨ b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
simp only [Nat.isUnit_iff]

Premises used: Nat.isUnit_iff
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
⊢ a = 1 ∨ b = 1

Tactic:
(h.2 a <| dvd_mul_right ..).imp_right fun hab ↦ ?_

Premises used: And.right, dvd_mul_right, Or.imp_right
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
refine : ∀ (hab : a = a * b), b = 1
⊢ a = 1 ∨ b = 1

Tactic:
refine (h.2 a <| dvd_mul_right ..).imp_right fun hab ↦ ?_

Premises used: And.right, dvd_mul_right, Or.imp_right
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
hab : a = a * b
rw : a * b * b = a * b * 1
rw₁ : a * b = a * 1
rw₂ : a = a * 1
rw₃ rw₄ : a = a
⊢ b = 1

Tactic:
rw [← mul_right_inj' (Nat.ne_zero_of_lt h1), ← hab, ← hab, mul_one]

Premises used: Nat.ne_zero_of_lt, mul_right_inj', mul_one
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1

Tactic:
prime_def.trans <|
    and_congr_right fun p2 =>
      forall_congr' fun _ =>
        ⟨fun h l d => (h d).resolve_right (ne_of_lt l), fun h d =>
          (le_of_dvd (le_of_succ_le p2) d).lt_or_eq_dec.imp_left fun l => h l d⟩

Premises used: Or.imp_left, Nat.le_of_succ_le, Nat.prime_def, and_congr_right, Iff.intro, forall_congr', Iff.trans, LE.le.lt_or_eq_dec, Or.resolve_right, Nat.le_of_dvd, Nat.ne_of_lt
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : m < p → m ∣ p → m = 1
m2 : 2 ≤ m
l : m < p
d : m ∣ p
⊢ LT.lt (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m → m < p → ¬m ∣ p
l : m < p
d : m ∣ p
zero : ∀ (h : LE.le (α := ℕ) 2 0 → 0 < p → ¬0 ∣ p) (l : 0 < p) (d : 0 ∣ p), Eq (α := ℕ) 0 1
succ :
  ∀ (h : 2 ≤ HAdd.hAdd (α := ℕ) 0 1 → HAdd.hAdd (α := ℕ) 0 1 < p → ¬HAdd.hAdd (α := ℕ) 0 1 ∣ p)
    (l : HAdd.hAdd (α := ℕ) 0 1 < p) (d : HAdd.hAdd (α := ℕ) 0 1 ∣ p), HAdd.hAdd (α := ℕ) 0 1 = 1
succ₁ :
  ∀ (m : ℕ) (h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p) (l : m + 1 + 1 < p) (d : m + 1 + 1 ∣ p), m + 1 + 1 = 1
⊢ m = 1

Tactic:
rcases m with (_ | _ | m)
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
h : LE.le (α := ℕ) 2 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ Eq (α := ℕ) 0 1

Tactic:
omega
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ HAdd.hAdd (α := ℕ) 0 1 → HAdd.hAdd (α := ℕ) 0 1 < p → ¬HAdd.hAdd (α := ℕ) 0 1 ∣ p
l : HAdd.hAdd (α := ℕ) 0 1 < p
d : HAdd.hAdd (α := ℕ) 0 1 ∣ p
⊢ HAdd.hAdd (α := ℕ) 0 1 = 1

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1

Tactic:
(h (le_add_left 2 m) l).elim d

Premises used: Nat.le_add_left, Not.elim, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1

Tactic:
exact (h (le_add_left 2 m) l).elim d

Premises used: Nat.le_add_left, Not.elim, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
h mdvd : m ∣ p
k : ℕ
e : p = m * k
h_1 : mdvd = ⋯
inl : ∀ (hm : m ≤ p.sqrt), False
inr : ∀ (hk : k ≤ p.sqrt), False
⊢ False

Tactic:
rcases le_sqrt_of_eq_mul e with hm | hk

Premises used: Nat.le_sqrt_of_eq_mul