internlm/Lean-Github huggingface dataset:
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ IsUnit ↑d
Tactic:
have hne2 : d ≠ 2 := by
  rintro rfl
  rw [Nat.cast_two, ← even_iff_two_dvd] at hdright
  have : ¬ Even (3 : ℤ) := by decide
  simp [this, hparity, two_ne_zero, parity_simps] at hdright
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
⊢ IsUnit ↑d
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
⊢ IsUnit ↑d
Tactic:
have : 2 < d := lt_of_le_of_ne hdprime.two_le hne2.symm
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this : 2 < d
⊢ IsUnit ↑d
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this : 2 < d
⊢ IsUnit ↑d
Tactic:
have : 3 < d := lt_of_le_of_ne this hne3.symm
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
⊢ IsUnit ↑d
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
⊢ IsUnit ↑d
Tactic:
obtain ⟨P, hP⟩ := hdleft
Proof state after:
case intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
⊢ IsUnit ↑d
Theorem: gcd1or3
Proof state before:
case intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
⊢ IsUnit ↑d
Tactic:
obtain ⟨Q, hQ⟩ := hdright
Proof state after:
case intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
⊢ IsUnit ↑d
Theorem: gcd1or3
Proof state before:
case intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
⊢ IsUnit ↑d
Tactic:
obtain ⟨H, hH⟩ : 2 ∣ P := by
  have H := dvd_mul_right 2 p
  rw [hP] at H
  apply (Prime.dvd_or_dvd Int.prime_two H).resolve_left
  rw [Int.dvd_natCast]
  change ¬2 ∣ d
  rw [Nat.prime_dvd_prime_iff_eq Nat.prime_two hdprime]
  exact hne2.symm
Proof state after:
case intro.intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
⊢ IsUnit ↑d
Theorem: gcd1or3
Proof state before:
case intro.intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
⊢ IsUnit ↑d
Tactic:
have hp : p = d * H := by rw [← mul_right_inj' (two_ne_zero' ℤ), hP, hH, mul_left_comm]
Proof state after:
case intro.intro.intro
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ IsUnit ↑d
Theorem: gcd1or3
Proof state before:
case intro.intro.intro
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ IsUnit ↑d
Tactic:
apply hcoprime.isUnit_of_dvd'
Proof state after:
case intro.intro.intro.ha
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ ↑d ∣ p

case intro.intro.intro.hb
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ ↑d ∣ q
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ d ≠ 2
Tactic:
rintro rfl
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : ↑2 ∣ p ^ 2 + 3 * q ^ 2
hne3 : 2 ≠ 3
⊢ False
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : ↑2 ∣ p ^ 2 + 3 * q ^ 2
hne3 : 2 ≠ 3
⊢ False
Tactic:
rw [Nat.cast_two, ← even_iff_two_dvd] at hdright
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
⊢ False
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
⊢ False
Tactic:
have : ¬ Even (3 : ℤ) := by decide
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
this : ¬Even 3
⊢ False
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
this : ¬Even 3
⊢ False
Tactic:
simp [this, hparity, two_ne_zero, parity_simps] at hdright
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
⊢ ¬Even 3
Tactic:
decide
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
⊢ 2 ∣ P
Tactic:
have H := dvd_mul_right 2 p
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ 2 * p
⊢ 2 ∣ P
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ 2 * p
⊢ 2 ∣ P
Tactic:
rw [hP] at H
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ 2 ∣ P
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ 2 ∣ P
Tactic:
apply (Prime.dvd_or_dvd Int.prime_two H).resolve_left
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ ¬2 ∣ ↑d
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ ¬2 ∣ ↑d
Tactic:
rw [Int.dvd_natCast]
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ ¬Int.natAbs 2 ∣ d
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ ¬Int.natAbs 2 ∣ d
Tactic:
change ¬2 ∣ d
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ ¬2 ∣ d
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ ¬2 ∣ d
Tactic:
rw [Nat.prime_dvd_prime_iff_eq Nat.prime_two hdprime]
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ ¬2 = d
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : 2 ∣ ↑d * P
⊢ ¬2 = d
Tactic:
exact hne2.symm
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
⊢ p = ↑d * H
Tactic:
rw [← mul_right_inj' (two_ne_zero' ℤ), hP, hH, mul_left_comm]
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.ha
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ ↑d ∣ p
Tactic:
rw [hp]
Proof state after:
case intro.intro.intro.ha
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ ↑d ∣ ↑d * H
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.ha
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ ↑d ∣ ↑d * H
Tactic:
exact dvd_mul_right _ _
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.hb
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ ↑d ∣ q
Tactic:
have h000 : d ∣ 3 * q.natAbs ^ 2 :=
  by
  rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.natCast_pow, Int.natAbs_sq, Nat.cast_three]
  use Q - d * H ^ 2
  rw [mul_sub, ← hQ, hp]
  ring
Proof state after:
case intro.intro.intro.hb
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000 : d ∣ 3 * q.natAbs ^ 2
⊢ ↑d ∣ q
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.hb
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000 : d ∣ 3 * q.natAbs ^ 2
⊢ ↑d ∣ q
Tactic:
cases' (Nat.Prime.dvd_mul hdprime).mp h000 with h000 h000
Proof state after:
case intro.intro.intro.hb.inl
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * q.natAbs ^ 2
h000 : d ∣ 3
⊢ ↑d ∣ q

case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * q.natAbs ^ 2
h000 : d ∣ q.natAbs ^ 2
⊢ ↑d ∣ q
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ d ∣ 3 * q.natAbs ^ 2
Tactic:
rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.natCast_pow, Int.natAbs_sq, Nat.cast_three]
Proof state after:
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ ↑d ∣ 3 * q ^ 2
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ ↑d ∣ 3 * q ^ 2
Tactic:
use Q - d * H ^ 2
Proof state after:
case h
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ 3 * q ^ 2 = ↑d * (Q - ↑d * H ^ 2)
Theorem: gcd1or3
Proof state before:
case h
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ 3 * q ^ 2 = ↑d * (Q - ↑d * H ^ 2)
Tactic:
rw [mul_sub, ← hQ, hp]
Proof state after:
case h
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ 3 * q ^ 2 = (↑d * H) ^ 2 + 3 * q ^ 2 - ↑d * (↑d * H ^ 2)
Theorem: gcd1or3
Proof state before:
case h
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
⊢ 3 * q ^ 2 = (↑d * H) ^ 2 + 3 * q ^ 2 - ↑d * (↑d * H ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.hb.inl
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * q.natAbs ^ 2
h000 : d ∣ 3
⊢ ↑d ∣ q
Tactic:
rw [Nat.prime_dvd_prime_iff_eq hdprime Nat.prime_three] at h000
Proof state after:
case intro.intro.intro.hb.inl
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * q.natAbs ^ 2
h000 : d = 3
⊢ ↑d ∣ q
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.hb.inl
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * q.natAbs ^ 2
h000 : d = 3
⊢ ↑d ∣ q
Tactic:
exact absurd h000 hne3
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * q.natAbs ^ 2
h000 : d ∣ q.natAbs ^ 2
⊢ ↑d ∣ q
Tactic:
rw [Int.natCast_dvd]
Proof state after:
case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * q.natAbs ^ 2
h000 : d ∣ q.natAbs ^ 2
⊢ d ∣ q.natAbs
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * q.natAbs ^ 2
h000 : d ∣ q.natAbs ^ 2
⊢ d ∣ q.natAbs
Tactic:
exact Nat.Prime.dvd_of_dvd_pow hdprime h000
Proof state after:
no goals