no goals
α : Type u_1
β : Type ?u.152330
m✝ m : MeasurableSpace α
v : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(ennrealToMeasure v) s = ↑v s
rw [ennrealToMeasure, ofMeasurable_apply _ hs]