no goals
α : Type u_1
β : Type ?u.7710
m : MeasurableSpace α
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w ↔ ∀ (i : Set α), ↑v i = ↑w i
rw [← coe_injective.eq_iff, Function.funext_iff]