mathlib

75c81dee - feat(measure_theory/integration): a measurable function is a series of simple functions (#7764)