no goals
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ leftInv S }
⊢ ↑x * ↑(↑(leftInvEquiv S hS) x) = 1
simp only [leftInvEquiv_apply, fromCommLeftInv, mul_fromLeftInv]