∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  f ≤ᵐ[μ] g → AEMeasurable g μ → ∀ (ε : ENNReal), ∫⁻ (a : α), f a ∂μ + ε * μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ