no goals
α : Type u_1
β : Type ?u.21168
γ : Type ?u.21171
δ : Type ?u.21174
ι : Type ?u.21177
R : Type ?u.21180
R' : Type ?u.21183
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t✝ : Set α
hs : MeasurableSet s
t : Set α
⊢ ↑↑μ s + ↑↑μ (t \ s) = ↑↑μ (s ∪ t)
rw [← measure_union' (@disjoint_sdiff_right _ s t) hs, union_diff_self]