∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    s ⊆ t →
      ∀ (ε : ℝ),
        μ.real t < μ.real s + ε →
          autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_diff_lt_of_lt_add._auto_1 → μ.real (t \ s) < ε