case h
M✝ : Type ?u.6042
N : Type ?u.6045
G : Type ?u.6048
A : Type ?u.6051
B : Type ?u.6054
α✝ : Type ?u.6057
β : Type ?u.6060
γ : Type ?u.6063
δ : Type ?u.6066
M : Type u_1
α : Type u_2
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : α
X✝ : M
⊢ MulOpposite.unop (MulOpposite.op X✝) • a = MulOpposite.op X✝ • a
M✝ : Type ?u.6042
N : Type ?u.6045
G : Type ?u.6048
A : Type ?u.6051
B : Type ?u.6054
α✝ : Type ?u.6057
β : Type ?u.6060
γ : Type ?u.6063
δ : Type ?u.6066
M : Type u_1
α : Type u_2
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
m : Mᵐᵒᵖ
a : α
⊢ MulOpposite.unop m • a = m • a
induction m using MulOpposite.rec'
no goals
case h
M✝ : Type ?u.6042
N : Type ?u.6045
G : Type ?u.6048
A : Type ?u.6051
B : Type ?u.6054
α✝ : Type ?u.6057
β : Type ?u.6060
γ : Type ?u.6063
δ : Type ?u.6066
M : Type u_1
α : Type u_2
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : α
X✝ : M
⊢ MulOpposite.unop (MulOpposite.op X✝) • a = MulOpposite.op X✝ • a
exact (IsCentralScalar.op_smul_eq_smul _ a).symm