Commit 2021-06-09 20:42 d9b91f3b

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.