have hne2 : d ≠ 2 := by
  rintro rfl
  rw [Nat.cast_two, ← even_iff_two_dvd] at hdright
  simp [hparity, two_ne_zero, parity_simps] at hdright
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
⊢ IsUnit ↑d
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
hne2 : d ≠ 2
⊢ IsUnit ↑d