no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝³ : Semiring R
p✝ q✝ r : R[X]
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ comp (s • p) q = s • comp p q
rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]