no goals
α : Type u_1
β : Type ?u.22602
γ : Type ?u.22605
δ : Type ?u.22608
ι : Type ?u.22611
R : Type ?u.22614
R' : Type ?u.22617
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s₂ ⊆ s₁
h₂ : MeasurableSet s₂
h_fin : ↑↑μ s₂ ≠ ⊤
⊢ ↑↑μ (s₁ \ s₂) = ↑↑μ s₁ - ↑↑μ s₂
rw [measure_diff' _ h₂ h_fin, union_eq_self_of_subset_right h]