diff --git a/Counterexamples/AharoniKorman.lean b/Counterexamples/AharoniKorman.lean
index 558a146b8f437a..3042c9c1ad8a90 100644
--- a/Counterexamples/AharoniKorman.lean
+++ b/Counterexamples/AharoniKorman.lean
@@ -790,7 +790,6 @@ theorem apply_eq_of_line_eq (f : SpinalMap C) {n : ℕ} (hC : IsChain (· ≤ ·
   have hy : y ∈ level n := ordConnected_level.out hlo.2 hhi.2 ⟨h₂l, h₂h⟩
   induction hx using induction_on_level with | h x₁ y₁ =>
   induction hy using induction_on_level with | h x₂ y₂ =>
-  simp only [] at hxy
   simp only [line_toHollom] at h
   obtain ⟨k, rfl⟩ := exists_add_of_le hxy
   obtain rfl : y₂ = y₁ + k := by lia
diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean b/Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean
index 5625376b02135f..5c7ab025de09b2 100644
--- a/Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean
@@ -127,7 +127,7 @@ theorem circleAverage_log_norm_sub_const₁ (h : ‖a‖ = 1) :
   _ = ∫ x in 0..(2 * π), log (4 * sin (x / 2) ^ 2) / 2 := by
     apply integral_congr
     intro x hx
-    simp only []
+    beta_reduce
     rw [Complex.norm_def, log_sqrt (circleMap 0 1 x - 1).normSq_nonneg]
     congr
     calc Complex.normSq (circleMap 0 1 x - 1)
diff --git a/Mathlib/CategoryTheory/Limits/Fubini.lean b/Mathlib/CategoryTheory/Limits/Fubini.lean
index 6ed237d8a0601b..865a1ea41e63a3 100644
--- a/Mathlib/CategoryTheory/Limits/Fubini.lean
+++ b/Mathlib/CategoryTheory/Limits/Fubini.lean
@@ -571,7 +571,7 @@ theorem colimitFlipCompColimIsoColimitCompColim_ι_ι_hom (j) (k) :
       (colimitFlipCompColimIsoColimitCompColim F).hom =
         (colimit.ι _ k ≫ colimit.ι (F ⋙ colim) j : _ ⟶ colimit (F ⋙ colim)) := by
   dsimp [colimitFlipCompColimIsoColimitCompColim]
-  slice_lhs 1 3 => simp only []
+  slice_lhs 1 3 => beta_reduce
   simp [Equivalence.unit]
 
 set_option backward.isDefEq.respectTransparency false in
@@ -581,7 +581,7 @@ theorem colimitFlipCompColimIsoColimitCompColim_ι_ι_inv (k) (j) :
       (colimitFlipCompColimIsoColimitCompColim F).inv =
         (colimit.ι _ j ≫ colimit.ι (F.flip ⋙ colim) k : _ ⟶ colimit (F.flip ⋙ colim)) := by
   dsimp [colimitFlipCompColimIsoColimitCompColim]
-  slice_lhs 1 3 => simp only []
+  slice_lhs 1 3 => beta_reduce
   simp [Equivalence.counitInv]
 
 end
@@ -712,7 +712,7 @@ theorem colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom {j} {k} :
         (colimit.ι _ k ≫ colimit.ι (curry.obj G ⋙ colim) j :
           _ ⟶ colimit (curry.obj G ⋙ colim)) := by
   dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
-  slice_lhs 1 3 => simp only []
+  slice_lhs 1 3 => beta_reduce
   simp
 
 set_option backward.isDefEq.respectTransparency false in
@@ -724,7 +724,7 @@ theorem colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv {j} {k} :
           colimit.ι (curry.obj _ ⋙ colim) k :
             _ ⟶ colimit (curry.obj (Prod.swap K J ⋙ G) ⋙ colim)) := by
   dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
-  slice_lhs 1 3 => simp only []
+  slice_lhs 1 3 => beta_reduce
   rw [colimitIsoColimitCurryCompColim_ι_ι_inv, HasColimit.isoOfEquivalence_inv_π]
   dsimp [Equivalence.counitInv]
   rw [CategoryTheory.Bifunctor.map_id]
diff --git a/Mathlib/Computability/PartrecCode.lean b/Mathlib/Computability/PartrecCode.lean
index 6a5a8cd7a1819f..e67aa7d71b5309 100644
--- a/Mathlib/Computability/PartrecCode.lean
+++ b/Mathlib/Computability/PartrecCode.lean
@@ -838,7 +838,7 @@ private theorem hG : Primrec G := by
     conv =>
       congr
       · ext p
-        dsimp only []
+        beta_reduce
         erw [Option.bind_eq_bind, ← Option.map_eq_bind]
     refine Primrec.option_map ((hlup.comp <| L.pair <| (k.pair cg).pair n).comp Primrec.fst) ?_
     unfold Primrec₂
diff --git a/Mathlib/Computability/RE.lean b/Mathlib/Computability/RE.lean
index f27d90fdeb867f..f2f3d2b7bb7ced 100644
--- a/Mathlib/Computability/RE.lean
+++ b/Mathlib/Computability/RE.lean
@@ -211,7 +211,7 @@ theorem ite {f₁ f₂ : ℕ → ℕ} (hf₁ : Computable f₁) (hf₂ : Computa
 theorem to_re {p : α → Prop} (hp : ComputablePred p) : REPred p := by
   obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp
   unfold REPred
-  dsimp only []
+  beta_reduce
   refine
     (Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n =>
       Part.ext fun a => ?_
diff --git a/Mathlib/Computability/TuringMachine/Config.lean b/Mathlib/Computability/TuringMachine/Config.lean
index 71099a475e9c7f..0d5e384969c95b 100644
--- a/Mathlib/Computability/TuringMachine/Config.lean
+++ b/Mathlib/Computability/TuringMachine/Config.lean
@@ -587,7 +587,7 @@ theorem stepNormal.is_ret (c k v) : ∃ k' v', stepNormal c k v = Cfg.ret k' v'
   | comp f _g _IHf IHg => apply IHg
   | case f g IHf IHg =>
     rw [stepNormal]
-    simp only []
+    beta_reduce
     cases v.headI <;> [apply IHf; apply IHg]
   | fix f IHf => apply IHf
   | _ => exact ⟨_, _, rfl⟩
@@ -612,7 +612,7 @@ theorem cont_eval_fix {f k v} (fok : Code.Ok f) :
         exact Or.inl (Part.mem_some _)
       · exact Or.inr ⟨_, Part.mem_some _, hv₂⟩
     refine fun c he => evalInduction he fun y h IH => ?_
-    rintro v (⟨v'⟩ | ⟨k', v'⟩) rfl hr <;> rw [Cfg.then] at h IH <;> simp only [] at h IH
+    rintro v (⟨v'⟩ | ⟨k', v'⟩) rfl hr <;> rw [Cfg.then] at h IH
     · have := mem_eval.2 ⟨hr, rfl⟩
       rw [fok, Part.bind_eq_bind, Part.mem_bind_iff] at this
       obtain ⟨v'', h₁, h₂⟩ := this
@@ -621,6 +621,7 @@ theorem cont_eval_fix {f k v} (fok : Code.Ok f) :
       · exact ReflTransGen.single rfl
       cases Part.mem_unique h₂ (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
       refine ⟨v', h₁, ?_⟩
+      beta_reduce at h IH
       rw [stepRet] at h
       revert h
       by_cases he : v'.headI = 0 <;> simp only [if_pos, if_false, he] <;> intro h
@@ -631,7 +632,6 @@ theorem cont_eval_fix {f k v} (fok : Code.Ok f) :
       · obtain ⟨k₀, v₀, e₀⟩ := stepNormal.is_ret f Cont.halt v'.tail
         have e₁ := stepNormal_then f Cont.halt (Cont.fix f k) v'.tail
         rw [e₀, Cont.then, Cfg.then] at e₁
-        simp only [] at e₁
         obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
           IH (stepRet (k₀.then (Cont.fix f k)) v₀) (by rw [stepRet, if_neg he, e₁]; rfl)
             v'.tail _ stepRet_then (by apply ReflTransGen.single; rw [e₀]; rfl)
diff --git a/Mathlib/Computability/TuringMachine/StackTuringMachine.lean b/Mathlib/Computability/TuringMachine/StackTuringMachine.lean
index 77dcba24dc80da..4c7e9c4184ac67 100644
--- a/Mathlib/Computability/TuringMachine/StackTuringMachine.lean
+++ b/Mathlib/Computability/TuringMachine/StackTuringMachine.lean
@@ -713,7 +713,6 @@ theorem trCfg_init (k) (L : List (Γ k)) : TrCfg (TM2.init k L)
     have : ((proj k').f ∘ fun a => update (β := fun k => Option (Γ k)) default k (some a))
       = fun a => (proj k').f (update (β := fun k => Option (Γ k)) default k (some a)) := rfl
     rw [this, List.getElem?_map, proj, PointedMap.mk_val]
-    simp only []
     by_cases h : k' = k
     · subst k'
       simp only [Function.update_self]
diff --git a/Mathlib/LinearAlgebra/Matrix/Basis.lean b/Mathlib/LinearAlgebra/Matrix/Basis.lean
index 6cc2855fc54d87..d747e568327aab 100644
--- a/Mathlib/LinearAlgebra/Matrix/Basis.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Basis.lean
@@ -133,7 +133,6 @@ def toMatrixEquiv [Fintype ι] (e : Basis ι R M) : (ι → M) ≃ₗ[R] Matrix
   map_smul' := by
     intro c v
     ext i j
-    dsimp only []
     rw [e.toMatrix_apply, Pi.smul_apply, map_smul]
     rfl
   invFun m j := ∑ i, m i j • e i
diff --git a/Mathlib/MeasureTheory/Covering/Besicovitch.lean b/Mathlib/MeasureTheory/Covering/Besicovitch.lean
index 0752545b875445..1be5eee58b912f 100644
--- a/Mathlib/MeasureTheory/Covering/Besicovitch.lean
+++ b/Mathlib/MeasureTheory/Covering/Besicovitch.lean
@@ -362,7 +362,6 @@ theorem color_lt {i : Ordinal.{u}} (hi : i < p.lastStep) {N : ℕ}
     have : k ∈ A := by
       simpa only [true_and, mem_univ, Classical.not_not, mem_diff] using
         Nat.notMem_of_lt_sInf hk
-    simp only [] at this
     simpa only [A, exists_prop, mem_iUnion, mem_singleton_iff, mem_closedBall, Subtype.exists,
       Subtype.coe_mk]
   choose! g hg using this
diff --git a/Mathlib/MeasureTheory/Measure/Restrict.lean b/Mathlib/MeasureTheory/Measure/Restrict.lean
index cdc0c8e0b4859b..2640745dd0d20a 100644
--- a/Mathlib/MeasureTheory/Measure/Restrict.lean
+++ b/Mathlib/MeasureTheory/Measure/Restrict.lean
@@ -810,7 +810,6 @@ theorem MeasurableSet.nullMeasurableSet_subtype_coe {t : Set s} (hs : NullMeasur
     simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]
     exact hs.diff ht'
   | iUnion f _ hf =>
-    dsimp only []
     rw [image_iUnion]
     exact .iUnion hf
 
diff --git a/Mathlib/ModelTheory/Encoding.lean b/Mathlib/ModelTheory/Encoding.lean
index 895c473de07db5..f0aab4c2a65efb 100644
--- a/Mathlib/ModelTheory/Encoding.lean
+++ b/Mathlib/ModelTheory/Encoding.lean
@@ -263,13 +263,11 @@ theorem listDecode_encode_list (l : List (Σ n, L.BoundedFormula α n)) :
     rw [length_map, length_finRange]
   | imp _ _ ih1 ih2 =>
     intro l
-    simp only [] at *
     rw [listEncode, List.append_assoc, cons_append, listDecode]
     simp only [ih1, ih2, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
       getElem_cons_zero, getElem_cons_succ, sigmaImp_apply, drop_succ_cons, drop_zero]
   | all _ ih =>
     intro l
-    simp only [] at *
     rw [listEncode, cons_append, listDecode]
     simp only [ih, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
       getElem_cons_zero, sigmaAll_apply, drop_succ_cons, drop_zero]