mathlib3

758d3228 - feat(measure_theory/interval_integral): make integral_comp lemmas computable by simp (#7010)

feat(measure_theory/interval_integral): make integral_comp lemmas computable by simp (#7010) A follow-up to #6795, enabling the computation of integrals of the form `∫ x in a..b, f (c * x + d)` by `simp`, where `f` is a function whose integral is already in mathlib and `c` and `d` are any real constants such that `c ≠ 0`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>