lift t to ℕ using Int.le_of_lt ht
case intro
t u : ℤ
ht : 0 < t
hu : 0 < u
s : ℕ
hs : 0 < ↑s
h : ↑s ^ 4 = t ^ 4 + u ^ 2
⊢ False
case intro.intro
u : ℤ
hu : 0 < u
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
h : ↑s ^ 4 = ↑t ^ 4 + u ^ 2
⊢ False