refactor: move disjoint_sdiff_inter (#12021)

Co-authored-by: Moritz Firsching <firsching@google.com>

Author: mo271

Mathlib/Data/Set/Basic.lean

@@ -1575,6 +1575,11 @@ lemma disjoint_sdiff_left : Disjoint (t \ s) s := disjoint_sdiff_self_left
 lemma disjoint_sdiff_right : Disjoint s (t \ s) := disjoint_sdiff_self_right
 #align set.disjoint_sdiff_right Set.disjoint_sdiff_right
 
+-- TODO: prove this in terms of a lattice lemma
+theorem disjoint_sdiff_inter : Disjoint (s \ t) (s ∩ t) :=
+  disjoint_of_subset_right (inter_subset_right _ _) disjoint_sdiff_left
+#align set.disjoint_sdiff_inter Set.disjoint_sdiff_inter
+
 theorem diff_union_diff_cancel (hts : t ⊆ s) (hut : u ⊆ t) : s \ t ∪ t \ u = s \ u :=
   sdiff_sup_sdiff_cancel hts hut
 #align set.diff_union_diff_cancel Set.diff_union_diff_cancel

Mathlib/MeasureTheory/Integral/PeakFunction.lean

@@ -3,12 +3,7 @@ Copyright (c) 2023 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.MeasureTheory.Integral.SetIntegral
-import Mathlib.MeasureTheory.Function.LocallyIntegrable
-import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 import Mathlib.MeasureTheory.Integral.IntegralEqImproper
-import Mathlib.MeasureTheory.Group.Integral
-import Mathlib.MeasureTheory.Measure.Haar.Unique
 
 #align_import measure_theory.integral.peak_function from "leanprover-community/mathlib"@"13b0d72fd8533ba459ac66e9a885e35ffabb32b2"
 
@@ -44,13 +39,6 @@ open Set Filter MeasureTheory MeasureTheory.Measure TopologicalSpace Metric
 
 open scoped Topology ENNReal
 
-/-- This lemma exists for finsets, but not for sets currently. porting note: move to
-data.set.basic after the port. -/
-theorem Set.disjoint_sdiff_inter {α : Type*} (s t : Set α) : Disjoint (s \ t) (s ∩ t) :=
-  disjoint_of_subset_right (inter_subset_right _ _) disjoint_sdiff_left
-#align set.disjoint_sdiff_inter Set.disjoint_sdiff_inter
-
-
 /-!
 ### General convergent result for integrals against a sequence of peak functions
 -/
@@ -186,7 +174,7 @@ theorem tendsto_set_integral_peak_smul_of_integrableOn_of_tendsto_aux
     ‖∫ x in s, φ i x • g x ∂μ‖ =
       ‖(∫ x in s \ u, φ i x • g x ∂μ) + ∫ x in s ∩ u, φ i x • g x ∂μ‖ := by
       conv_lhs => rw [← diff_union_inter s u]
-      rw [integral_union (disjoint_sdiff_inter _ _) (hs.inter u_open.measurableSet)
+      rw [integral_union disjoint_sdiff_inter (hs.inter u_open.measurableSet)
           (h''i.mono_set (diff_subset _ _)) (h''i.mono_set (inter_subset_left _ _))]
     _ ≤ ‖∫ x in s \ u, φ i x • g x ∂μ‖ + ‖∫ x in s ∩ u, φ i x • g x ∂μ‖ := norm_add_le _ _
     _ ≤ (δ * ∫ x in s, ‖g x‖ ∂μ) + 2 * δ := add_le_add C B