no goals
K : Type u
inst✝¹ : CommRing K
R : Type u_1
inst✝ : SMul R (FractionRing K[X])
c : R
p : FractionRing K[X]
⊢ { toFractionRing := c • p } = c • { toFractionRing := p }
simp only [SMul.smul, HSMul.hSMul, RatFunc.smul]