no goals
M : Type ?u.11403
N : Type ?u.11406
G : Type ?u.11409
A : Type ?u.11412
B : Type ?u.11415
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ (a • b) • c • d = (a • c) • b • d
rw [smul_assoc, smul_assoc, smul_comm b]