no goals
M : Type u_1
inst✝ : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ ↑(↑(MulEquiv.symm (leftInvEquiv S hS)) x) = (↑x)⁻¹
rw [← mul_right_inj (x : M), mul_right_inv, mul_leftInvEquiv_symm]