mathlib

615af755 - feat(measure_theory/interval_integral): `integral_deriv_comp_mul_deriv` (#7141)

feat(measure_theory/interval_integral): `integral_deriv_comp_mul_deriv` (#7141) `∫ x in a..b, (g ∘ f) x * f' x`, where `f'` is derivative of `f` and `g` is the derivative of some function (the latter qualification allowing us to compute the integral directly by FTC-2)