mathlib

a71e79e7 - feat(data/fun_like): define `embedding_like` and `equiv_like`

feat(data/fun_like): define `embedding_like` and `equiv_like` 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 `mul_equiv_class` etc.