no goals
M✝ : Type ?u.27981
N✝ : Type ?u.27984
G : Type ?u.27987
A : Type ?u.27990
B : Type ?u.27993
α : Type ?u.27996
β : Type ?u.27999
γ : Type ?u.28002
δ : Type ?u.28005
M : Type u_1
N : Type u_2
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ y * x • 1 = x • y
rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]