no goals
α : Type u_1
β : Type ?u.21889
γ : Type ?u.21892
δ : Type ?u.21895
ι : Type ?u.21898
R : Type ?u.21901
R' : Type ?u.21904
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hm : MeasurableSet t
h_fin : ↑↑μ t ≠ ⊤
⊢ ↑↑μ (s \ t) + ↑↑μ t = ↑↑μ (s ∪ t)
rw [add_comm, measure_add_diff hm, union_comm]