no goals
ι : Type ?u.21287
α : Type u_1
β : Type ?u.21293
γ : Type ?u.21296
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
hs : NullMeasurableSet s
⊢ ↑↑μ s + ↑↑μ (sᶜ) = ↑↑μ univ
rw [← measure_union₀' hs aedisjoint_compl_right, union_compl_self]