feat(logic/function/basic): refine extend_apply (#16944)
Add `function.extend_apply_of_unique`
which allows to rewrite `function.extend f g e (f a) = g a`
not only when `f` is injective, what `function.extend_apply` does,
but when `f a = f b → g a = g b`.
Generalize a few similar lemmas in the same way.
TODO ? : rewrite `function.extend_apply` to use this function.
Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
