∀ {X : Type u_1} {mX : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν],
  (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition = μ.jordanDecompositionOfToSignedMeasureSub ν