no goals
M✝ : Type ?u.27123
N✝ : Type ?u.27126
G : Type ?u.27129
A : Type ?u.27132
B : Type ?u.27135
α : Type ?u.27138
β : Type ?u.27141
γ : Type ?u.27144
δ : Type ?u.27147
M : Type u_1
N : Type u_2
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • 1 * y = x • y
rw [smul_mul_assoc, one_mul]