replace h : s^4 = t^4 + u^2 := eq_add_of_sub_eq' h
s t u : ℤ
hs : 0 < s
ht : 0 < t
hu : 0 < u
h : s ^ 4 - t ^ 4 = u ^ 2
⊢ False
s t u : ℤ
hs : 0 < s
ht : 0 < t
hu : 0 < u
h : s ^ 4 = t ^ 4 + u ^ 2
⊢ False