diff --git a/Mathlib/Analysis/BoxIntegral/Integrability.lean b/Mathlib/Analysis/BoxIntegral/Integrability.lean
index 9cd4c5108bd04..eaf2f17700f98 100644
--- 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
index ed741f37cbf85..d824d0aecc8ad 100644
--- 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
index 25c6a33aeb53c..7d14584bbab76 100644
--- 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)