set g := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) with hg'
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
⊢ Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 1 ∨ Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 3
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)
⊢ g = 1 ∨ g = 3