no goals
M✝ : Type ?u.26534
N✝ : Type ?u.26537
G : Type ?u.26540
A : Type ?u.26543
B : Type ?u.26546
α : Type u_3
β : Type ?u.26552
γ : Type ?u.26555
δ : Type ?u.26558
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid N
inst✝³ : SMul M N
inst✝² : MulAction N α
inst✝¹ : SMul M α
inst✝ : IsScalarTower M N α
x : M
y : α
⊢ (x • 1) • y = x • y
rw [smul_assoc, one_smul]