Lean4
/-- A monoid homomorphism `f : M →* N` with a left-inverse `g : N → M` defines a multiplicative
equivalence between `M` and `f.mrange`.
This is a bidirectional version of `MonoidHom.mrange_restrict`. -/
@[to_additive (attr := simps +simpRhs) /--
An additive monoid homomorphism `f : M →+ N` with a left-inverse `g : N → M` defines an
additive equivalence between `M` and `f.mrange`. This is a bidirectional version of
`AddMonoidHom.mrange_restrict`. -/
]
def ofLeftInverse' (f : M →* N) {g : N → M} (h : Function.LeftInverse g f) : M ≃* MonoidHom.mrange f :=
{ f.mrangeRestrict with
toFun := f.mrangeRestrict
invFun := g ∘ (MonoidHom.mrange f).subtype
left_inv := h
right_inv := fun x =>
Subtype.ext <|
let ⟨x', hx'⟩ := MonoidHom.mem_mrange.mp x.2
show f (g x) = x by rw [← hx', h x'] }
