no goals
ι : Type ?u.12172012
𝕜 : Type ?u.12172015
E : Type u_1
F : Type ?u.12172021
A : Type ?u.12172024
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g✝ : ℝ → E
μ : MeasureTheory.Measure ℝ
g : ℝ → ℝ
h : ∀ᵐ (t : ℝ) ∂Measure.restrict μ (Ι a b), ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
⊢ ‖∫ (t : ℝ) in a..b, f t ∂μ‖ ≤ abs (∫ (t : ℝ) in a..b, g t ∂μ)
simp_rw [norm_intervalIntegral_eq, abs_intervalIntegral_eq,
  abs_eq_self.mpr (integral_nonneg_of_ae <| h.mono fun _t ht => (norm_nonneg _).trans ht),
  norm_integral_le_of_norm_le hbound.def h]