refactor(Measure): replace trimmed with trim_le (#12794)

This follows the design pattern "request a seemingly weaker assumption in the definition,
prove a seemingly stronger condition in a theorem".

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -822,7 +822,7 @@ theorem measure_toMeasurable_inter {s t : Set α} (hs : MeasurableSet s) (ht : 
 instance instZero [MeasurableSpace α] : Zero (Measure α) :=
   ⟨{  toOuterMeasure := 0
       m_iUnion := fun _f _hf _hd => tsum_zero.symm
-      trimmed := OuterMeasure.trim_zero }⟩
+      trim_le := OuterMeasure.trim_zero.le }⟩
 #align measure_theory.measure.has_zero MeasureTheory.Measure.instZero
 
 @[simp]
@@ -858,7 +858,7 @@ instance instAdd [MeasurableSpace α] : Add (Measure α) :=
       m_iUnion := fun s hs hd =>
         show μ₁ (⋃ i, s i) + μ₂ (⋃ i, s i) = ∑' i, (μ₁ (s i) + μ₂ (s i)) by
           rw [ENNReal.tsum_add, measure_iUnion hd hs, measure_iUnion hd hs]
-      trimmed := by rw [OuterMeasure.trim_add, μ₁.trimmed, μ₂.trimmed] }⟩
+      trim_le := by rw [OuterMeasure.trim_add, μ₁.trimmed, μ₂.trimmed] }⟩
 #align measure_theory.measure.has_add MeasureTheory.Measure.instAdd
 
 @[simp]
@@ -888,7 +888,7 @@ instance instSMul [MeasurableSpace α] : SMul R (Measure α) :=
       m_iUnion := fun s hs hd => by
         simp only [OuterMeasure.smul_apply, coe_toOuterMeasure, ENNReal.tsum_const_smul,
           measure_iUnion hd hs]
-      trimmed := by rw [OuterMeasure.trim_smul, μ.trimmed] }⟩
+      trim_le := by rw [OuterMeasure.trim_smul, μ.trimmed] }⟩
 #align measure_theory.measure.has_smul MeasureTheory.Measure.instSMul
 
 @[simp]
@@ -1118,7 +1118,7 @@ instance instCompleteLattice [MeasurableSpace α] : CompleteLattice (Measure α)
             exact le_top
           else
             simp_all [Set.not_nonempty_iff_eq_empty]
-        trimmed := le_antisymm le_top (OuterMeasure.le_trim _) },
+        trim_le := le_top },
     le_top := fun μ => toOuterMeasure_le.mp le_top
     bot := 0
     bot_le := fun _a _s => bot_le }

Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

@@ -80,7 +80,7 @@ extension of the restricted measure. -/
 structure Measure (α : Type*) [MeasurableSpace α] extends OuterMeasure α where
   m_iUnion ⦃f : ℕ → Set α⦄ : (∀ i, MeasurableSet (f i)) → Pairwise (Disjoint on f) →
     toOuterMeasure (⋃ i, f i) = ∑' i, toOuterMeasure (f i)
-  trimmed : toOuterMeasure.trim = toOuterMeasure
+  trim_le : toOuterMeasure.trim ≤ toOuterMeasure
 #align measure_theory.measure MeasureTheory.Measure
 
 theorem Measure.toOuterMeasure_injective [MeasurableSpace α] :
@@ -100,6 +100,9 @@ variable [MeasurableSpace α] {μ μ₁ μ₂ : Measure α} {s s₁ s₂ t : Set
 
 namespace Measure
 
+theorem trimmed (μ : Measure α) : μ.toOuterMeasure.trim = μ.toOuterMeasure :=
+  le_antisymm μ.trim_le μ.1.le_trim
+
 /-! ### General facts about measures -/
 
 /-- Obtain a measure by giving a countably additive function that sends `∅` to `0`. -/
@@ -108,16 +111,13 @@ def ofMeasurable (m : ∀ s : Set α, MeasurableSet s → ℝ≥0∞) (m0 : m 
       ∀ ⦃f : ℕ → Set α⦄ (h : ∀ i, MeasurableSet (f i)),
         Pairwise (Disjoint on f) → m (⋃ i, f i) (MeasurableSet.iUnion h) = ∑' i, m (f i) (h i)) :
     Measure α :=
-  { inducedOuterMeasure m _ m0 with
+  { toOuterMeasure := inducedOuterMeasure m _ m0
     m_iUnion := fun f hf hd =>
       show inducedOuterMeasure m _ m0 (iUnion f) = ∑' i, inducedOuterMeasure m _ m0 (f i) by
         rw [inducedOuterMeasure_eq m0 mU, mU hf hd]
         congr; funext n; rw [inducedOuterMeasure_eq m0 mU]
-    trimmed :=
-      show (inducedOuterMeasure m _ m0).trim = inducedOuterMeasure m _ m0 by
-        unfold OuterMeasure.trim
-        congr; funext s hs
-        exact inducedOuterMeasure_eq m0 mU hs }
+    trim_le := le_inducedOuterMeasure.2 fun s hs ↦ by
+      rw [OuterMeasure.trim_eq _ hs, inducedOuterMeasure_eq m0 mU hs] }
 #align measure_theory.measure.of_measurable MeasureTheory.Measure.ofMeasurable
 
 theorem ofMeasurable_apply {m : ∀ s : Set α, MeasurableSet s → ℝ≥0∞}

Mathlib/MeasureTheory/Measure/NullMeasurable.lean

@@ -486,8 +486,7 @@ def completion {_ : MeasurableSpace α} (μ : Measure α) :
     @MeasureTheory.Measure (NullMeasurableSpace α μ) _ where
   toOuterMeasure := μ.toOuterMeasure
   m_iUnion s hs hd := measure_iUnion₀ (hd.mono fun i j h => h.aedisjoint) hs
-  trimmed := by
-    refine le_antisymm ?_ (@OuterMeasure.le_trim (NullMeasurableSpace α μ) _ _)
+  trim_le := by
     nth_rewrite 2 [← μ.trimmed]
     exact OuterMeasure.trim_anti_measurableSpace _ fun _ ↦ MeasurableSet.nullMeasurableSet
 #align measure_theory.measure.completion MeasureTheory.Measure.completion

Mathlib/MeasureTheory/Measure/Stieltjes.lean

@@ -346,7 +346,7 @@ protected irreducible_def measure : Measure ℝ :=
   { toOuterMeasure := f.outer
     m_iUnion := fun _s hs =>
       f.outer.iUnion_eq_of_caratheodory fun i => f.borel_le_measurable _ (hs i)
-    trimmed := f.outer_trim }
+    trim_le := f.outer_trim.le }
 #align stieltjes_function.measure StieltjesFunction.measure
 
 @[simp]