no goals
M : Type u_2
N : Type ?u.22188
G : Type ?u.22191
A : Type ?u.22194
B : Type ?u.22197
α : Type u_1
β : Type ?u.22203
γ : Type ?u.22206
δ : Type ?u.22209
inst✝⁴ : Monoid M
inst✝³ : MulAction M α
inst✝² : Mul α
r s : M
x y : α
inst✝¹ : IsScalarTower M α α
inst✝ : SMulCommClass M α α
⊢ r • x * s • y = (r * s) • (x * y)
rw [smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]