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