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