no goals
R : Type u
S : Type v
A : Type w
B : Type ?u.319925
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
s : R
x y : A
⊢ x * s • y = s • (x * y)
rw [smul_def, smul_def, left_comm]