[GOAL]
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g • ↑m * g⁻¹ • ↑m⁻¹ = 1
[PROOFSTEP]
rw [smul_mul_smul, Units.mul_inv, mul_right_inv, one_smul]
[GOAL]
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g⁻¹ • ↑m⁻¹ * g • ↑m = 1
[PROOFSTEP]
rw [smul_mul_smul, Units.inv_mul, mul_left_inv, one_smul]
