∀ {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {μ : MeasureTheory.Measure α}
  [self : s.HaveLebesgueDecomposition μ], s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ