mathlib3

700d4773 - feat(analysis/special_functions/integrals): integral_comp for `f : ℝ → ℝ` (#7216)

feat(analysis/special_functions/integrals): integral_comp for `f : ℝ → ℝ` (#7216) In #7103 I added lemmas to deal with integrals of the form `c • ∫ x in a..b, f (c * x + d)`. However, it came to my attention that, with those lemmas, `simp` can only handle such integrals if they use `•`, not `*`. To solve this problem and enable computation of these integrals by `simp`, I add versions of the aforementioned `integral_comp` lemmas specialized with `f : ℝ → ℝ` and label them with `simp`.