∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] {μ : MeasureTheory.Measure α}
  [μ.WeaklyRegular] (f : MeasureTheory.SimpleFunc α NNReal),
  ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤ →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε