mathlib3

d0e454ac - feat(logic/function/basic): add `function.{in,sur,bi}jective.comp_left` (#10406)

feat(logic/function/basic): add `function.{in,sur,bi}jective.comp_left` (#10406) As far as I can tell we don't have these variations. Note that the `surjective` and `bijective` versions do not appear next to the other composition statements, as they require `surj_inv` to concisely prove.