simp
case inl
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (discConv w 0).degree ≤ degree 0
no goals