case h.e'_2.h.e'_5.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ x = ↑(leftInvEquiv S hS) (↑(MulEquiv.symm (leftInvEquiv S hS)) x)
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ ↑x * ↑(↑(MulEquiv.symm (leftInvEquiv S hS)) x) = 1
convert S.leftInvEquiv_mul hS ((S.leftInvEquiv hS).symm x)
no goals
case h.e'_2.h.e'_5.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : { x // x ∈ S }
⊢ x = ↑(leftInvEquiv S hS) (↑(MulEquiv.symm (leftInvEquiv S hS)) x)
simp