chore(MeasureTheory): add [simp] attribute to measure_lt_top and …

…`measure_ne_top` (#16793) This is particularly useful when working only with probability measures, as observed when preparing teaching material. The PR does not change much in Mathlib (if a `simp` could have used the new simp lemmas but didn't, it was non-terminal and then got turned into a `simp only` and we don't see any effect).
leanprover-community · Sep 14, 2024 · 37e06d7 · 37e06d7
1 parent 20ceaf4
commit 37e06d7
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/Mathlib/Analysis/BoxIntegral/Integrability.lean b/Mathlib/Analysis/BoxIntegral/Integrability.lean
@@ -113,7 +113,7 @@ theorem HasIntegral.of_aeEq_zero {l : IntegrationParams} {I : Box ι} {f : (ι
   have : ∀ n, ∃ U, N ⁻¹' {n} ⊆ U ∧ IsOpen U ∧ μ.restrict I U < δ n / n := fun n ↦ by
     refine (N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_
     cases' n with n
-    · simpa [ENNReal.div_zero (ENNReal.coe_pos.2 (δ0 _)).ne'] using measure_lt_top (μ.restrict I) _
+    · simp [ENNReal.div_zero (ENNReal.coe_pos.2 (δ0 _)).ne']
     · refine (measure_mono_null ?_ hf).le.trans_lt ?_
       · exact fun x hxN hxf => n.succ_ne_zero ((Eq.symm hxN).trans <| N0.2 hxf)
       · simp [(δ0 _).ne']

diff --git a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean
@@ -210,7 +210,7 @@ theorem measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure {Ω : Type
     have whole := h 1
     simp only [BoundedContinuousFunction.coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_const,
       one_mul] at whole
-    simpa [← whole] using IsFiniteMeasure.measure_univ_lt_top
+    simp [← whole]
   have obs_μ := HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed μ
   have obs_ν := HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed ν
   simp_rw [h] at obs_μ

diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/Mathlib/MeasureTheory/Measure/Typeclasses.lean
@@ -46,13 +46,14 @@ instance Restrict.isFiniteMeasure (μ : Measure α) [hs : Fact (μ s < ∞)] :
     IsFiniteMeasure (μ.restrict s) :=
   ⟨by simpa using hs.elim⟩
 
+@[simp]
 theorem measure_lt_top (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) : μ s < ∞ :=
   (measure_mono (subset_univ s)).trans_lt IsFiniteMeasure.measure_univ_lt_top
 
 instance isFiniteMeasureRestrict (μ : Measure α) (s : Set α) [h : IsFiniteMeasure μ] :
-    IsFiniteMeasure (μ.restrict s) :=
-  ⟨by simpa using measure_lt_top μ s⟩
+    IsFiniteMeasure (μ.restrict s) := ⟨by simp⟩
 
+@[simp]
 theorem measure_ne_top (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) : μ s ≠ ∞ :=
   ne_of_lt (measure_lt_top μ s)