mathlib3

31531531 - feat(measure_theory/interval_integral): add `integral_comp_mul_left` (#6787)