refine' ⟨p, q, hp, hq, hcoprime, hodd, Or.inr <| Or.inl hcube⟩
case intro.intro.intro.intro.intro.intro.inl.inr.intro.intro.intro.intro.intro.intro.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : b ^ 3 + a ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : Even b
hc : ¬Even c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (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)
no goals