∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_add_diff._auto_1 →
      autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_add_diff._auto_3 → μ.real s + μ.real (t \ s) = μ.real (s ∪ t)