rw [← mul_right_inj' (two_ne_zero' ℤ), hP, hH, mul_left_comm]
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
no goals