obtain ⟨k, hg, hk⟩ := H
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)
H : ∃ k, g = 3 ^ k ∧ k < 2
⊢ g = 1 ∨ g = 3
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)
k : ℕ
hg : g = 3 ^ k
hk : k < 2
⊢ g = 1 ∨ g = 3