no goals
M✝ : Type ?u.29021
N✝ : Type ?u.29024
G : Type ?u.29027
A : Type ?u.29030
B : Type ?u.29033
α : Type ?u.29036
β : Type ?u.29039
γ : Type ?u.29042
δ : Type ?u.29045
M : Type u_1
N : Type u_2
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ (x • y) • z = x • y • z
rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]