feat: measure real of the complement of a null measurable set (leanprover-community#31155)

Author: EtienneC30

Mathlib/MeasureTheory/Measure/Real.lean

@@ -368,6 +368,10 @@ theorem measureReal_compl [IsFiniteMeasure μ] (h₁ : MeasurableSet s) :
   rw [compl_eq_univ_diff]
   exact measureReal_diff (subset_univ s) h₁
 
+theorem measureReal_compl₀ [IsFiniteMeasure μ] (h₁ : NullMeasurableSet s μ) :
+    μ.real sᶜ = μ.real univ - μ.real s := by
+  linarith [measureReal_add_measureReal_compl₀ h₁]
+
 theorem measureReal_union_congr_of_subset (hs : s₁ ⊆ s₂)
     (hsμ : μ.real s₂ ≤ μ.real s₁) (ht : t₁ ⊆ t₂) (htμ : μ.real t₂ ≤ μ.real t₁)
     (h₁ : μ s₂ ≠ ∞ := by finiteness) (h₂ : μ t₂ ≠ ∞ := by finiteness) :