simp [natDegree_comp]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (P.comp (X + C r)).natDegree ≤ P.natDegree
no goals