∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ENNReal}
  [MeasureTheory.IsProbabilityMeasure μ], ∫⁻ (a : α), f a ∂μ ≠ ⊤ → μ N = 0 → ∃ x ∉ N, ∫⁻ (a : α), f a ∂μ ≤ f x