∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  μ s ≠ 0 → μ s ≠ ⊤ → AEMeasurable f (μ.restrict s) → 0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}