no goals
ι : Type ?u.20745139
𝕜 : Type ?u.20745142
E : Type ?u.20745145
F : Type ?u.20745148
A : Type ?u.20745151
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
⊢ abs (∫ (x : ℝ) in a..b, f x ∂μ) ≤ ∫ (x : ℝ) in a..b, abs (f x) ∂μ
simpa only [← Real.norm_eq_abs] using norm_integral_le_integral_norm hab