case h
R : Type ?u.1165
G : Type u_1
inst✝ : CancelCommMonoid G
g x✝ : G
⊢ ↑(mulLeftEmbedding g) x✝ = ↑(mulRightEmbedding g) x✝
R : Type ?u.1165
G : Type u_1
inst✝ : CancelCommMonoid G
g : G
⊢ mulLeftEmbedding g = mulRightEmbedding g
ext
no goals
case h
R : Type ?u.1165
G : Type u_1
inst✝ : CancelCommMonoid G
g x✝ : G
⊢ ↑(mulLeftEmbedding g) x✝ = ↑(mulRightEmbedding g) x✝
exact mul_comm _ _