Theorem: MeasureTheory.measureReal_add_measureReal_compl₀ (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : NullMeasurableSet s μ
⊢ μ.real s + μ.real sᶜ = μ.real univ
Tactic:
rw [← measureReal_union₀' hs aedisjoint_compl_right, union_compl_self]
State after:
no goals