no goals
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • ↑(of f) x = ↑(of f) (a • x)
rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]