mathlib

f470cc62 - feat(measure_theory/interval_integral): add simp attribute to `integral_const` (#6334)

feat(measure_theory/interval_integral): add simp attribute to `integral_const` (#6334) By adding a `simp` attribute to `interval_integral.integral_const`, the likes of the following become possible: ``` import measure_theory.interval_integral example : ∫ x:ℝ in 5..19, (12:ℝ) = 168 := by norm_num ```