mathlib

494f7199 - feat(data/fun_like): define `embedding_like` and `equiv_like` (#10759)

feat(data/fun_like): define `embedding_like` and `equiv_like` (#10759) These extend `fun_like` with a proof of injectivity resp. an inverse. The number of new generic lemmas is quite low at the moment, so their use is more in defining derived classes such as `mul_equiv_class`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>