no goals
α : Type u_2
β : Type ?u.25485
m : MeasurableSpace α
M✝ : Type ?u.25491
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : TopologicalSpace M✝
inst✝³ : T2Space M✝
v✝ : VectorMeasure α M✝
f : ℕ → Set α
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ ↑v (B \ A) = ↑v B - ↑v A
rw [← of_add_of_diff hA hB h, add_sub_cancel']