Commit 2021-04-21 19:58 700d4773

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.