simp [this, hparity, two_ne_zero, parity_simps] at hdright
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
no goals