awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ x = p ∧ y = p
have inr : y = p ∧ x = p
Tactic: rw [And.comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ x = p ∧ y = p
have inl : ∀ (hx : p ∣ x), x = p ∧ y = p
Tactic: obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ x = p ∧ y = p
have inr : ∀ (hy : p ∣ y), y = p ∧ x = p
Tactic: obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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 = p ∧ x = p
have h₁ : y * x = HPow.hPow (β := ℕ) p 2
Tactic: rw [mul_comm] at h pdvdxy
Cleared hypotheses: h, pdvdxy, this, hy
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ y = p ∧ x = p
have pdvdxy₁ : p ∣ y * x
Tactic: rw [mul_comm] at h pdvdxy
Cleared hypotheses: h, pdvdxy, this, hy
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ x = p ∧ y = p
have inl : ∀ (hx : p ∣ x), x = p ∧ y = p
Tactic: obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]] <;>
      [skip; rw [mul_comm] at h pdvdxy]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ x = p ∧ y = p
have 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
Tactic: obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]] <;>
      [skip; rw [mul_comm] at h pdvdxy]
Cleared hypotheses: h, pdvdxy, this
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
⊢ x = p ∧ y = p
have suffices : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → 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
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ p = a * y
have rwa : ∀ (h : p * a * y = HPow.hPow (β := ℕ) p 2) (ha : x = p * a), p = a * y
Tactic: rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ p = a * y
have rwa₁ : ∀ (h : p * a * y = p * p) (ha : x = p * a), p = a * y
Tactic: rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ p = a * y
have rwa₂ : ∀ (h : p * (a * y) = p * p) (ha : x = p * a), p = a * y
Tactic: rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ p = a * y
have rwa₃ : ∀ (h : a * y = p) (ha : x = p * a), p = a * y
Tactic: rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ p = a * y
have rwa₄ : ∀ (h : p = a * y) (ha : x = p * a), p = a * y
Tactic: rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ x = p ∧ y = p
have this : a ∣ p
Tactic: have : a ∣ p := ⟨y, by rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ x = p ∧ y = p
have inl : ∀ (ha : x = p * 1) (this : 1 ∣ p), x = p ∧ y = p
Tactic: obtain rfl | hap := (Nat.dvd_prime hp).mp ‹a ∣ p›
Cleared hypotheses: a, ha, this
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ x = p ∧ y = p
have inr : ∀ (hap : a = p), x = p ∧ y = p
Tactic: obtain rfl | hap := (Nat.dvd_prime hp).mp ‹a ∣ p›
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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 ∧ y = p
have ha₁ : x = p
Tactic: rw [mul_one] at ha
Cleared hypotheses: ha, this
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ x = p ∧ y = p
have 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
Tactic: subst ha
Cleared hypotheses: p, hp, h_1, pdvdxy, h, ha, this
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ x = x ∧ y = x
have h₁ : y = x
Tactic: simp only [sq, mul_right_inj' hp.ne_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ x = x ∧ y = x
have 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
Tactic: subst h
Cleared hypotheses: x, hx, hp, h_1, pdvdxy, this, h
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
have inr : y = 1
Tactic: refine (hy ?_).elim
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ y = 1
have hp₁ : Prime a
Tactic: subst hap
Cleared hypotheses: p, hp, h_1, pdvdxy, h, ha, this, hap
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ y = 1
have h₁ : x_1 * y_1 = HPow.hPow (β := ℕ) a 2
Tactic: subst hap
Cleared hypotheses: p, hp, h_1, pdvdxy, h, ha, this, hap
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ y = 1
have pdvdxy₁ : a ∣ x_1 * y_1
Tactic: subst hap
Cleared hypotheses: p, hp, h_1, pdvdxy, h, ha, this, hap
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ y = 1
have h₂ : x * y = HPow.hPow (β := ℕ) a 2
Tactic: subst hap
Cleared hypotheses: p, hp, h_1, pdvdxy, h, ha, this, hap
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ y = 1
have ha₁ : x = a * a
Tactic: subst hap
Cleared hypotheses: p, hp, h_1, pdvdxy, h, ha, this, hap
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ y = 1
have this₁ : a ∣ a
Tactic: subst hap
Cleared hypotheses: p, hp, h_1, pdvdxy, h, ha, this, hap
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ y = 1
have hx₁ : a * a ≠ 1
Tactic: subst ha
Cleared hypotheses: x, hx, h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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
⊢ y = 1
have h₁ : a * a * y = HPow.hPow (β := ℕ) a 2
Tactic: subst ha
Cleared hypotheses: x, hx, h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
pp : Prime p
i : ℕ
⊢ p.Coprime i ∨ p ∣ i
have rw : p.Coprime i ∨ ¬p.Coprime i
Tactic: rw [pp.dvd_iff_not_coprime]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
pp : Prime p
m i : ℕ
⊢ i ∣ p ^ m ↔ ∃ (k : ℕ), k ≤ m ∧ i = p ^ k
have simp_rw : (∃ (i_1 : ℕ), i_1 ≤ m ∧ Associated i (p ^ i_1)) ↔ ∃ (k : ℕ), k ≤ m ∧ i = p ^ k
Tactic: simp_rw [_root_.dvd_prime_pow (prime_iff.mp pp) m, associated_eq_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
a p k : ℕ
pp : Prime p
h₁ : ¬a ∣ p ^ k
h₂ : a ∣ p ^ (k + 1)
⊢ a = p ^ (k + 1)
have obtain : ∀ (l : ℕ) (h : l ≤ k + 1) (h₁ : ¬p ^ l ∣ p ^ k) (h₂ : p ^ l ∣ p ^ (k + 1)), p ^ l = p ^ (k + 1)
Tactic: obtain ⟨l, ⟨h, rfl⟩⟩ := (dvd_prime_pow pp).1 h₂
Cleared hypotheses: a, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ p ^ l = p ^ (k + 1)
have e_a : l = k + 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
Goal:
n : ℕ
a : ℕ := n + 2
⊢ n + 2 ≠ 1 ↔ ∃ (p : ℕ), Prime p ∧ p ∣ n + 2
have ha : a ≠ 1
Tactic: have ha : a ≠ 1 := Nat.succ_succ_ne_one n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1
⊢ n + 2 ≠ 1 ↔ ∃ (p : ℕ), Prime p ∧ p ∣ n + 2
have simp : ∃ (p : ℕ), Prime p ∧ p ∣ n + 2
Tactic: simp only [a, true_iff, Ne, not_false_iff, ha]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ p ^ (k + l) * p ∣ m * n
have rwa : ∀ (hpmn' : p * p ^ (k + l) ∣ m * n), p ^ (k + l) * p ∣ m * n
Tactic: rwa [pow_succ'] at hpmn'
Cleared hypotheses: hpmn'
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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 + 1) ∣ m ∨ p ^ (l + 1) ∣ n
have hpd : 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'
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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 ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
have hpd2 : p ∣ m * n / p ^ (k + l)
Tactic: have hpd2 : p ∣ m * n / p ^ (k + l) := dvd_div_of_mul_dvd hpd
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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 ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
have hpd3 : p ∣ m * n / (p ^ k * p ^ l)
Tactic: have hpd3 : p ∣ m * n / (p ^ k * p ^ l) := by simpa [pow_add] using hpd2
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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 ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
have hpd4 : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
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 ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
have hpd5 : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
have rwa : p ^ k * p ∣ m ∨ p ^ (l + 1) ∣ n
Tactic: rwa [_root_.pow_succ, _root_.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
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 + 1) ∣ m ∨ p ^ (l + 1) ∣ n
have suffices : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
Tactic: suffices p ^ k * p ∣ m ∨ p ^ l * p ∣ n by rwa [_root_.pow_succ, _root_.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
pp : Prime p
m : ℕ
hm : m ∣ p
⊢ m = 1 ∨ m = p
have obtain : ∀ (n : ℕ) (hn : p = m * n), m = 1 ∨ m = p
Tactic: obtain ⟨n, hn⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
⊢ m = 1 ∨ m = p
have this : IsUnit m ∨ IsUnit n
Tactic: have := pp.isUnit_or_isUnit hn
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : IsUnit m ∨ IsUnit n
⊢ m = 1 ∨ m = p
have this₁ : m = 1 ∨ n = 1
Tactic: rw [Nat.isUnit_iff, Nat.isUnit_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ m = 1 ∨ m = p
have apply : n = 1 → m = p
Tactic: apply Or.imp_right _ this
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ Eq (α := ℕ) 1 1
⊢ m = p
have rw : m = m * 1
Tactic: rw [hn, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ Eq (α := ℕ) 1 1
rw : m = m * 1
⊢ m = p
have rw₁ : m = m
Tactic: rw [hn, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
have refine : ∀ (h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p), Prime p
Tactic: refine ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ Prime p
have h1 : 1 < p
Tactic: have h1 := Nat.one_lt_two.trans_le h.1
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ Prime p
have refine : ∀ ⦃a b : ℕ⦄, p = a * b → IsUnit a ∨ IsUnit b
Tactic: refine ⟨mt Nat.isUnit_iff.mp h1.ne', ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
⊢ IsUnit a ∨ IsUnit b
have simp : a = 1 ∨ b = 1
Tactic: simp only [Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
⊢ a = 1 ∨ b = 1
have refine : ∀ (hab : a = a * b), b = 1
Tactic: refine (h.2 a <| dvd_mul_right ..).imp_right fun hab ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
hab : a = a * b
⊢ b = 1
have rw : a * b * b = a * b * 1
Tactic: rw [← mul_right_inj' (Nat.ne_zero_of_lt h1), ← hab, ← hab, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ b = 1
have rw₁ : a * b = a * 1
Tactic: rw [← mul_right_inj' (Nat.ne_zero_of_lt h1), ← hab, ← hab, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ b = 1
have rw₂ : a = a * 1
Tactic: rw [← mul_right_inj' (Nat.ne_zero_of_lt h1), ← hab, ← hab, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ b = 1
have rw₃ : a = a
Tactic: rw [← mul_right_inj' (Nat.ne_zero_of_lt h1), ← hab, ← hab, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m → m < p → ¬m ∣ p
l : m < p
d : m ∣ p
⊢ m = 1
have zero : ∀ (h : LE.le (α := ℕ) 2 0 → 0 < p → ¬0 ∣ p) (l : 0 < p) (d : 0 ∣ p), Eq (α := ℕ) 0 1
Tactic: rcases m with (_ | _ | m)
Cleared hypotheses: m, h, l, d
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ m = 1
have 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
Tactic: rcases m with (_ | _ | m)
Cleared hypotheses: m, h, l, d
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ m = 1
have 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
Tactic: rcases m with (_ | _ | m)
Cleared hypotheses: m, h, l, d
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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 = ⋯
⊢ False
have inl : ∀ (hm : m ≤ p.sqrt), False
Tactic: rcases le_sqrt_of_eq_mul e with hm | hk
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ False
have inr : ∀ (hk : k ≤ p.sqrt), False
Tactic: rcases le_sqrt_of_eq_mul e with hm | hk