no goals
α : Type u_1
β : Type ?u.23713
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ ↑v A + ↑v (B \ A) = ↑v B
rw [← of_union (@Set.disjoint_sdiff_right _ A B) hA (hB.diff hA), Set.union_diff_cancel h]