exfalso
case neg
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
⊢ Even a ↔ ¬Even b
case neg.h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
⊢ False