mathlib3

85dc9f34 - refactor(measure_theory/measure): redefine `measure_theory.sigma_finite` (#9207)

refactor(measure_theory/measure): redefine `measure_theory.sigma_finite` (#9207) * don't require in the definition that covering sets are measurable; * use `to_measurable` in `sigma_finite.out` to get measurable sets.