no goals
ι : Type ?u.18521
α : Type u_1
β : Type ?u.18527
γ : Type ?u.18530
m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
hs : NullMeasurableSet s
t : Set α
⊢ ↑↑μ (s ∪ t) + ↑↑μ (s ∩ t) = ↑↑μ s + ↑↑μ t
rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]