mathlib

a217b9c3 - feat(measure_theory): drop some `measurable_set` assumptions (#11536)

feat(measure_theory): drop some `measurable_set` assumptions (#11536) * make `exists_subordinate_pairwise_disjoint` work for `null_measurable_set`s; * use `ae_disjoint` in `measure_Union₀`, drop `measure_Union_of_null_inter`; * prove `measure_inter_add_diff` for `null_measurable_set`s; * drop some `measurable_set` assumptions in `measure_union`, `measure_diff`, etc; * golf.