obtain ⟨s, ⟨b⟩⟩ := hS
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
hS : ∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ IsNilpotent ((trace R S) x)
case pos.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsNilpotent x
s : Finset S
b : Basis { x // x ∈ s } R S
⊢ IsNilpotent ((trace R S) x)