[GOAL]
α : Type u_1
M : Type ?u.8804
N : Type ?u.8800
inst✝² : Mul N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : Nᵐᵒᵖ
z : N
⊢ x • y • z = y • x • z
[PROOFSTEP]
induction y using MulOpposite.rec'
[GOAL]
case h
α : Type u_1
M : Type ?u.8804
N : Type ?u.8800
inst✝² : Mul N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
z X✝ : N
⊢ x • op X✝ • z = op X✝ • x • z
[PROOFSTEP]
simp only [smul_mul_assoc, MulOpposite.smul_eq_mul_unop]
