mathlib3
61db67de - chore(measure_theory/integration): define composition of a `simple_func` and a measurable function (#3667)
