no goals
α : Type u_1
β : Type ?u.150394
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure μ - toSignedMeasure ν) i = ENNReal.toReal (↑↑μ i) - ENNReal.toReal (↑↑ν i)
rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
  Measure.toSignedMeasure_apply_measurable hi, sub_eq_add_neg]