no goals
ι : Type ?u.13713922
𝕜 : Type ?u.13713925
E : Type u_1
F : Type ?u.13713931
A : Type ?u.13713934
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
c : E
⊢ (∫ (x : ℝ) in a..b, c) = (b - a) • c
simp only [integral_const', Real.volume_Ioc, ENNReal.toReal_ofReal', ← neg_sub b,
  max_zero_sub_eq_self]