refactor(MeasureTheory): golf Mathlib/MeasureTheory/Measure/Sub (leanprover-community#39179)

- refactors `Mathlib/MeasureTheory/Measure/Sub` by shortening `sub_le_iff_le_add_of_le`

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/Measure/Sub.lean

@@ -149,11 +149,7 @@ instance isFiniteMeasure_sub [IsFiniteMeasure μ] : IsFiniteMeasure (μ - ν) :=
 hypothesis `ν ≤ μ`. -/
 lemma sub_le_iff_le_add_of_le [IsFiniteMeasure ν] (h_le : ν ≤ μ) : μ - ν ≤ ξ ↔ μ ≤ ξ + ν := by
   refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩
-  rw [Measure.le_iff] at h ⊢
-  intro s hs
-  specialize h s hs
-  simp only [Measure.coe_add, Pi.add_apply]
-  rwa [Measure.sub_apply hs h_le, tsub_le_iff_right] at h
+  simpa [sub_add_cancel_of_le h_le] using add_le_add_left h ν
 
 end Measure