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
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
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