refactor(MeasureTheory): golf Mathlib/MeasureTheory/VectorMeasure/Decomposition/Lebesgue (leanprover-community#39180)

- refactors `Mathlib/MeasureTheory/VectorMeasure/Decomposition/Lebesgue` by simplifying `singularPart_mutuallySingular` and `singularPart_neg`

Extracted from leanprover-community#38104

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/MeasureTheory/VectorMeasure/Decomposition/Lebesgue.lean

@@ -124,19 +124,8 @@ section
 
 theorem singularPart_mutuallySingular (s : SignedMeasure α) (μ : Measure α) :
     s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ
-      s.toJordanDecomposition.negPart.singularPart μ := by
-  by_cases hl : s.HaveLebesgueDecomposition μ
-  · obtain ⟨i, hi, hpos, hneg⟩ := s.toJordanDecomposition.mutuallySingular
-    rw [s.toJordanDecomposition.posPart.haveLebesgueDecomposition_add μ] at hpos
-    rw [s.toJordanDecomposition.negPart.haveLebesgueDecomposition_add μ] at hneg
-    rw [add_apply, add_eq_zero] at hpos hneg
-    exact ⟨i, hi, hpos.1, hneg.1⟩
-  · rw [not_haveLebesgueDecomposition_iff] at hl
-    rcases hl with hp | hn
-    · rw [Measure.singularPart, dif_neg hp]
-      exact MutuallySingular.zero_left
-    · rw [Measure.singularPart, Measure.singularPart, dif_neg hn]
-      exact MutuallySingular.zero_right
+      s.toJordanDecomposition.negPart.singularPart μ :=
+  (s.toJordanDecomposition.mutuallySingular.singularPart μ).mono le_rfl (singularPart_le _ _)
 
 theorem singularPart_totalVariation (s : SignedMeasure α) (μ : Measure α) :
     (s.singularPart μ).totalVariation =
@@ -317,17 +306,7 @@ theorem singularPart_zero (μ : Measure α) : (0 : SignedMeasure α).singularPar
 
 theorem singularPart_neg (s : SignedMeasure α) (μ : Measure α) :
     (-s).singularPart μ = -s.singularPart μ := by
-  have h₁ :
-    ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
-      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure := by
-    refine toSignedMeasure_congr ?_
-    rw [toJordanDecomposition_neg, JordanDecomposition.neg_posPart]
-  have h₂ :
-    ((-s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
-      (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure := by
-    refine toSignedMeasure_congr ?_
-    rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]
-  rw [singularPart, singularPart, neg_sub, h₁, h₂]
+  simp [singularPart, toJordanDecomposition_neg]
 
 theorem singularPart_smul_nnreal (s : SignedMeasure α) (μ : Measure α) (r : ℝ≥0) :
     (r • s).singularPart μ = r • s.singularPart μ := by