ι : Type ?u.20977613
𝕜 : Type ?u.20977616
E : Type ?u.20977619
F : Type ?u.20977622
A : Type ?u.20977625
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᵐ[Measure.restrict μ (Icc a b)] g
H : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ioc a b), f x ≤ g x :=
  Eventually.filter_mono (ae_mono (Measure.restrict_mono Ioc_subset_Icc_self (le_refl μ))) h
⊢ (∫ (u : ℝ) in a..b, f u ∂μ) ≤ ∫ (u : ℝ) in a..b, g u ∂μ
ι : Type ?u.20977613
𝕜 : Type ?u.20977616
E : Type ?u.20977619
F : Type ?u.20977622
A : Type ?u.20977625
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᵐ[Measure.restrict μ (Icc a b)] g
⊢ (∫ (u : ℝ) in a..b, f u ∂μ) ≤ ∫ (u : ℝ) in a..b, g u ∂μ
let H := h.filter_mono <| ae_mono <| Measure.restrict_mono Ioc_subset_Icc_self <| le_refl μ
no goals
ι : Type ?u.20977613
𝕜 : Type ?u.20977616
E : Type ?u.20977619
F : Type ?u.20977622
A : Type ?u.20977625
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᵐ[Measure.restrict μ (Icc a b)] g
H : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ioc a b), f x ≤ g x :=
  Eventually.filter_mono (ae_mono (Measure.restrict_mono Ioc_subset_Icc_self (le_refl μ))) h
⊢ (∫ (u : ℝ) in a..b, f u ∂μ) ≤ ∫ (u : ℝ) in a..b, g u ∂μ
simpa only [integral_of_le hab] using set_integral_mono_ae_restrict hf.1 hg.1 H