case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b x✝ : A
⊢ ↑(mulRight R (a * b)) x✝ = ↑(comp (mulRight R b) (mulRight R a)) x✝
R : Type u_2
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b : A
⊢ mulRight R (a * b) = comp (mulRight R b) (mulRight R a)
ext
no goals
case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b x✝ : A
⊢ ↑(mulRight R (a * b)) x✝ = ↑(comp (mulRight R b) (mulRight R a)) x✝
simp only [mulRight_apply, comp_apply, mul_assoc]