∀ {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ ν : MeasureTheory.Measure X}
  [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : MeasureTheory.IsFiniteMeasure ν],
  MeasureTheory.IsHahnDecomposition μ ν s →
    ((ν - μ).restrict s).toSignedMeasure =
      MeasureTheory.VectorMeasure.restrict ν.toSignedMeasure s -
        MeasureTheory.VectorMeasure.restrict μ.toSignedMeasure s