no goals
α : Type u_1
β : Type ?u.297148
E : Type ?u.297151
F : Type ?u.297154
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (a : α) ∂μ, a ∈ s → f a ≤ 0
⊢ (fun a => f a) ≤ᵐ[Measure.restrict μ s] 0
rwa [EventuallyLE, ae_restrict_iff' hs]