replace hs : 0 < s := Int.ofNat_pos.mp hs
case intro.intro.intro
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
⊢ False
case intro.intro.intro
s t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
⊢ False