no goals
α : Type u_1
β : Type ?u.6873
γ : Type ?u.6876
δ : Type ?u.6879
ι : Type ?u.6882
R : Type ?u.6885
R' : Type ?u.6888
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t✝ : Set α
hs : MeasurableSet s
t : Set α
⊢ ↑↑μ (s ∪ t) + ↑↑μ (s ∩ t) = ↑↑μ s + ↑↑μ t
rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]