feat (MeasureTheory): Measure.add_sub_cancel (#15468)

LorenzoLuccioli · LorenzoLuccioli · commit 79df738051ef · 2024-08-04T10:58:32.000Z
Add `Measure.add_sub_cancel`.
diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean
@@ -505,7 +505,7 @@ theorem _root_.ApproximatesLinearOn.norm_fderiv_sub_le {A : E →L[ℝ] E} {δ :
     exact ⟨a, az, by simp only [ha, add_neg_cancel_left]⟩
   have norm_a : ‖a‖ ≤ ‖z‖ + ε :=
     calc
-      ‖a‖ = ‖z + (a - z)‖ := by simp only [add_sub_cancel]
+      ‖a‖ = ‖z + (a - z)‖ := by simp only [_root_.add_sub_cancel]
       _ ≤ ‖z‖ + ‖a - z‖ := norm_add_le _ _
       _ ≤ ‖z‖ + ε := add_le_add_left (mem_closedBall_iff_norm.1 az) _
   -- use the approximation properties to control `(f' x - A) a`, and then `(f' x - A) z` as `z` is
diff --git a/Mathlib/MeasureTheory/Measure/Sub.lean b/Mathlib/MeasureTheory/Measure/Sub.lean
@@ -90,6 +90,12 @@ theorem sub_add_cancel_of_le [IsFiniteMeasure ν] (h₁ : ν ≤ μ) : μ - ν +
   ext1 s h_s_meas
   rw [add_apply, sub_apply h_s_meas h₁, tsub_add_cancel_of_le (h₁ s)]
 
+@[simp]
+lemma add_sub_cancel [IsFiniteMeasure ν] : μ + ν - ν = μ := by
+  ext1 s hs
+  rw [sub_apply hs (Measure.le_add_left (le_refl _)), add_apply,
+    ENNReal.add_sub_cancel_right (measure_ne_top ν s)]
+
 theorem restrict_sub_eq_restrict_sub_restrict (h_meas_s : MeasurableSet s) :
     (μ - ν).restrict s = μ.restrict s - ν.restrict s := by
   repeat rw [sub_def]
