mathlib3

c7f51395 - chore(measure_theory): drop a few `measurable_set` assumptions (#9999)

chore(measure_theory): drop a few `measurable_set` assumptions (#9999) We had an extra `measurable_set` assumption in (one of the copies of) Caratheodory. Also remove `measurable f` assumption in `is_finite_measure (map f μ)` and make it an instance.