no goals
α : Type u_1
β : Type ?u.283976
E : Type ?u.283979
F : Type ?u.283982
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s t : Set α
hf : IntegrableOn f s
hg : IntegrableOn g s
hs : MeasurableSet s
h : ∀ (x : α), x ∈ s → f x ≤ g x
⊢ (fun a => f a) ≤ᵐ[Measure.restrict μ s] fun a => g a
simp [hs, EventuallyLE, eventually_inf_principal, ae_of_all _ h]