apply IsCoprime.isUnit_of_dvd' hcoprime hdvdp
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)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ IsUnit 3
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)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ 3 ∣ q