mathlib3

b9ff26b5 - chore(measure_theory/measure/measure_space): reorder, golf (#10015)

chore(measure_theory/measure/measure_space): reorder, golf (#10015) Move `restrict_apply'` up and use it to golf some proofs. Drop an unneeded `measurable_set` assumption in 1 proof.