mathlib3

75b4ee86 - feat(data/equiv/local_equiv): construct from `bij_on` or `inj_on` (#2232)

feat(data/equiv/local_equiv): construct from `bij_on` or `inj_on` (#2232) * feat(data/equiv/local_equiv): construct from `bij_on` or `inj_on` Also fix usage of `nonempty` vs `inhabited` in `set/function`. Linter didn't catch these bugs because the types use the `.to_nonempty` projection of the `[inhabited]` arguments. * Add `simps`/`simp` attrs Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>