mathlib3

955e95ad - feat(logic/function/basic): add some more API for `injective2` (#13074)

feat(logic/function/basic): add some more API for `injective2` (#13074) Note that the new `.left` and `.right` lemmas are weaker than the original ones, but the original lemmas were pretty much useless anyway, as `hf.left h` was the same as `(hf h).left`.