[GOAL]
R : Type u_1
G : Type u_2
inst✝ : CancelCommMonoid G
g : G
⊢ mulLeftEmbedding g = mulRightEmbedding g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
G : Type u_2
inst✝ : CancelCommMonoid G
g x✝ : G
⊢ ↑(mulLeftEmbedding g) x✝ = ↑(mulRightEmbedding g) x✝
[PROOFSTEP]
exact mul_comm _ _
