mathlib

4ca9b48f - refactor(data/set/function): Generalize `maps_to`, `inj_on`, `eq_on`, `left_inv_on`, `right_inv_on`, and `inv_on` to anything with has_mem

refactor(data/set/function): Generalize `maps_to`, `inj_on`, `eq_on`, `left_inv_on`, `right_inv_on`, and `inv_on` to anything with has_mem This makes these statements usable on finset too, but does so at the expense of breaking projection notation.