have contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False :=
  by
  intro x y hcoprime hx hy
  rw [even_iff_two_dvd] at hx hy
  have := Int.isUnit_eq_one_or (hcoprime.isUnit_of_dvd' hx hy)
  norm_num at this
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c