rw [← h]
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ c ^ 3 + (-a) ^ 3 = b ^ 3
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ a ^ 3 + b ^ 3 + (-a) ^ 3 = b ^ 3