by_contra hne3
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : Nat.Prime d
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
⊢ d = 3
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : Nat.Prime d
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : ¬d = 3
⊢ False