α : Type u_1
β : Type ?u.623899
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ toSignedMeasure (Measure.singularPart (toJordanDecomposition (r • s)).posPart μ) -
      toSignedMeasure (Measure.singularPart (toJordanDecomposition (r • s)).negPart μ) =
    toSignedMeasure (r • Measure.singularPart (toJordanDecomposition s).posPart μ) -
      toSignedMeasure (r • Measure.singularPart (toJordanDecomposition s).negPart μ)
α : Type u_1
β : Type ?u.623899
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ singularPart (r • s) μ = r • singularPart s μ
rw [singularPart, singularPart, smul_sub, ← toSignedMeasure_smul, ← toSignedMeasure_smul]