feat(measure_theory/tactic): add measurability tactic (#7756)
Add a measurability tactic defined in the file `measure_theory/tactic.lean`, which is heavily inspired from the continuity tactic. It proves goals of the form `measurable f`, `ae_measurable f ยต` and `measurable_set s`. Some tests are provided in `tests/measurability.lean` and the tactic was used to replace a few lines in `integration.lean` and `mean_inequalities.lean`.
