-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
inr :
  (-r).toNNReal • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      ((-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₁ :
  (-r).toNNReal • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      (-r).toNNReal • (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₂ :
  -((-r).toNNReal • (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (-r).toNNReal • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₃ :
  -((-r).toNNReal •
        ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
          (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₄ :
  -((↑(-r).toNNReal : ℝ) •
        ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
          (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₅ :
  -(↑(-r).toNNReal : ℝ) •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₆ :
  - -r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₇ inr₈ :
  r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
⊢ ((-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      ((-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)

Tactic:
rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub, NNReal.smul_def,
      ← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr hr)), neg_neg]

Premises used: Iff.mpr, neg_smul, neg_sub, neg_pos, le_of_lt, neg_neg, MeasureTheory.Measure.toSignedMeasure_smul, Real.coe_toNNReal, smul_sub, NNReal.smul_def