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