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
⊢ ↑(mulLeft R (a * b)) x✝ = ↑(comp (mulLeft R a) (mulLeft R b)) 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
⊢ mulLeft R (a * b) = comp (mulLeft R a) (mulLeft R b)
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
⊢ ↑(mulLeft R (a * b)) x✝ = ↑(comp (mulLeft R a) (mulLeft R b)) x✝
simp only [mulLeft_apply, comp_apply, mul_assoc]