mathlib

43bbaee8 - feat(measure_theory/measure): add lemmas, drop `measurable_set` assumptions (#11499)

feat(measure_theory/measure): add lemmas, drop `measurable_set` assumptions (#11499) * `restrict_eq_self` no longer requires measurability of either set; * `restrict_apply_self` no longer requires measurability of the set; * add `restrict_apply_superset` and `restrict_restrict_of_subset` ; * add `restrict_restrict'` that assumes measurability of the other set, drop one `measurable_set` assumption in `restrict_comm`; * drop measurability assumptions in `restrict_congr_mono`.