mathlib3

a359bd98 - chore(measure_theory): measurability statements for coercions, coherent naming (#7854)