simp only [‹¬ Even (3 : ℤ)›, false_or_iff, iff_not_self, parity_simps] at huvodd
case hb
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this✝² : Odd 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
v : ℤ
this✝¹ : ¬Even 3
hddd : ¬3 ∣ p
s : ℤ
hs : 2 * p = s ^ 3
hpfactor : p = 3 * v * (3 * v - 3 * v) * (3 * v + 3 * v)
hq : q = 3 * v * (3 * v - v) * (3 * v + v)
huvcoprime : IsCoprime (3 * v) v
huvodd : Even (3 * v) ↔ ¬Even v
u_ne_zero : 3 * v ≠ 0
haaa : 2 * p = 2 * (3 * v) * (3 * v - 3 * v) * (3 * v + 3 * v)
this✝ : ¬Even (3 * v - 3 * v)
this : ¬Even (3 * v + 3 * v)
notdvd_2_2 : ¬2 ∣ 3 * v - 3 * v
not_3_dvd_2 : ¬3 ∣ 3 * v - 3 * v
notdvd_3_3 : ¬3 ∣ 3 * v + 3 * v
⊢ False
no goals