rw [← pow_mul_pow_sub _ H] at hg
case H
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)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ k
H : 2 ≤ List.length (Nat.factors g)
⊢ False
case H
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)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
⊢ False