diff --git a/Mathlib/Algebra/CharZero/Quotient.lean b/Mathlib/Algebra/CharZero/Quotient.lean
index d3872fea29c7e..f26890215d6a0 100644
--- a/Mathlib/Algebra/CharZero/Quotient.lean
+++ b/Mathlib/Algebra/CharZero/Quotient.lean
@@ -58,7 +58,7 @@ theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {
   -- Porting note: Introduced Zp notation to shorten lines
   let Zp := AddSubgroup.zmultiples p
   have : (Quotient.mk _ : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl
-  simp only [this]
+  simp +zetaDelta only [this]
   simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
     QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]
   exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz
diff --git a/Mathlib/CategoryTheory/Category/Cat/Limit.lean b/Mathlib/CategoryTheory/Category/Cat/Limit.lean
index e16a6957e1e3f..27275a6d15792 100644
--- a/Mathlib/CategoryTheory/Category/Cat/Limit.lean
+++ b/Mathlib/CategoryTheory/Category/Cat/Limit.lean
@@ -50,7 +50,7 @@ def homDiagram {F : J ⥤ Cat.{v, v}} (X Y : limit (F ⋙ Cat.objects.{v, v})) :
   map_id X := by
     funext f
     letI : Category (objects.obj (F.obj X)) := (inferInstance : Category (F.obj X))
-    simp [Functor.congr_hom (F.map_id X) f]
+    simp +zetaDelta [Functor.congr_hom (F.map_id X) f]
   map_comp {_ _ Z} f g := by
     funext h
     letI : Category (objects.obj (F.obj Z)) := (inferInstance : Category (F.obj Z))
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean
index e6c2252ce3d8d..e11267720fa1a 100644
--- a/Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean
+++ b/Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean
@@ -31,16 +31,18 @@ theorem hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair {C : Type u} [
   let e := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
   HasLimit.mk
     { cone :=
-        PullbackCone.mk (e ≫ π₁) (e ≫ π₂) <| by rw [Category.assoc, equalizer.condition]; simp
+        PullbackCone.mk (e ≫ π₁) (e ≫ π₂) <| by
+          rw [Category.assoc, equalizer.condition]
+          simp +zetaDelta
       isLimit :=
         PullbackCone.IsLimit.mk _ (fun s => equalizer.lift
           (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) <| by
             rw [← Category.assoc, limit.lift_π, ← Category.assoc, limit.lift_π]
             exact PullbackCone.condition _)
-          (by simp [π₁, e]) (by simp [π₂, e]) fun s m h₁ h₂ => by
+          (by simp +zetaDelta [π₁, e]) (by simp +zetaDelta [π₂, e]) fun s m h₁ h₂ => by
           ext
-          · dsimp; simpa using h₁
-          · simpa using h₂ }
+          · dsimp; simpa +zetaDelta using h₁
+          · simpa +zetaDelta using h₂ }
 
 section
 
@@ -73,10 +75,10 @@ theorem hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair {C : Type
               (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) <| by
             rw [Category.assoc, colimit.ι_desc, Category.assoc, colimit.ι_desc]
             exact PushoutCocone.condition _)
-          (by simp [ι₁, c]) (by simp [ι₂, c]) fun s m h₁ h₂ => by
+          (by simp +zetaDelta [ι₁, c]) (by simp +zetaDelta [ι₂, c]) fun s m h₁ h₂ => by
           ext
-          · simpa using h₁
-          · simpa using h₂ }
+          · simpa +zetaDelta using h₁
+          · simpa +zetaDelta using h₂ }
 
 section
 
diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean
index b82770a4d5037..43c689b051d6e 100644
--- a/Mathlib/CategoryTheory/Localization/Construction.lean
+++ b/Mathlib/CategoryTheory/Localization/Construction.lean
@@ -223,7 +223,7 @@ theorem morphismProperty_is_top (P : MorphismProperty W.Localization)
     suffices ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f) by
       rcases X with ⟨⟨X⟩⟩
       rcases Y with ⟨⟨Y⟩⟩
-      simpa only [Functor.map_preimage] using this _ _ (G.preimage f)
+      simpa +zetaDelta only [Functor.map_preimage] using this _ _ (G.preimage f)
     intros X₁ X₂ p
     induction' p with X₂ X₃ p g hp
     · simpa only [Functor.map_id] using hP₁ (𝟙 X₁.obj)
diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean
index 72a7a69ef0039..ae0b9a154b0c0 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functor.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functor.lean
@@ -972,10 +972,10 @@ instance [e.functor.Monoidal] : e.symm.inverse.Monoidal := inferInstanceAs (e.fu
 noncomputable def inverseMonoidal [e.functor.Monoidal] : e.inverse.Monoidal := by
   letI := e.toAdjunction.rightAdjointLaxMonoidal
   have : IsIso (LaxMonoidal.ε e.inverse) := by
-    simp only [Adjunction.rightAdjointLaxMonoidal_ε, Adjunction.homEquiv_unit]
+    simp +zetaDelta only [Adjunction.rightAdjointLaxMonoidal_ε, Adjunction.homEquiv_unit]
     infer_instance
   have : ∀ (X Y : D), IsIso (LaxMonoidal.μ e.inverse X Y) := fun X Y ↦ by
-    simp only [Adjunction.rightAdjointLaxMonoidal_μ, Adjunction.homEquiv_unit]
+    simp +zetaDelta only [Adjunction.rightAdjointLaxMonoidal_μ, Adjunction.homEquiv_unit]
     infer_instance
   apply Monoidal.ofLaxMonoidal
 
diff --git a/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean b/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
index f0f3a969c4866..563ab05ec4916 100644
--- a/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
+++ b/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
@@ -68,9 +68,9 @@ def isColimitOfEffectiveEpiStruct {X Y : C} (f : Y ⟶ X) (Hf : EffectiveEpiStru
       let Y' : D := ⟨Over.mk f, 𝟙 _, by simp⟩
       let Z' : D := ⟨Over.mk (g₁ ≫ f), g₁, rfl⟩
       let g₁' : Z' ⟶ Y' := Over.homMk g₁
-      let g₂' : Z' ⟶ Y' := Over.homMk g₂ (by simp [h])
+      let g₂' : Z' ⟶ Y' := Over.homMk g₂ (by simp +zetaDelta [h])
       change F.map g₁' ≫ _ = F.map g₂' ≫ _
-      simp only [S.w]
+      simp +zetaDelta only [S.w]
     fac := by
       rintro S ⟨T,g,hT⟩
       dsimp
@@ -113,7 +113,7 @@ def effectiveEpiStructOfIsColimit {X Y : C} (f : Y ⟶ X)
       intro W e h
       dsimp
       have := Hf.fac (aux e h) ⟨Over.mk f, 𝟙 _, by simp⟩
-      dsimp at this; rw [this]; clear this
+      dsimp +zetaDelta at this; rw [this]; clear this
       nth_rewrite 2 [← Category.id_comp e]
       apply h
       generalize_proofs hh
@@ -181,7 +181,7 @@ def isColimitOfEffectiveEpiFamilyStruct {B : C} {α : Type*}
       let i₁ : Z' ⟶ A₁ := Over.homMk g₁
       let i₂ : Z' ⟶ A₂ := Over.homMk g₂
       change F.map i₁ ≫ _ = F.map i₂ ≫ _
-      simp only [S.w]
+      simp +zetaDelta only [S.w]
     fac := by
       intro S ⟨T, a, (g : T.left ⟶ X a), hT⟩
       dsimp
@@ -226,7 +226,7 @@ def effectiveEpiFamilyStructOfIsColimit {B : C} {α : Type*}
       intro W e h a
       dsimp
       have := H.fac (aux e h) ⟨Over.mk (π a), a, 𝟙 _, by simp⟩
-      dsimp at this; rw [this]; clear this
+      dsimp +zetaDelta at this; rw [this]; clear this
       conv_rhs => rw [← Category.id_comp (e a)]
       apply h
       generalize_proofs h1 h2
diff --git a/Mathlib/Data/Nat/Pairing.lean b/Mathlib/Data/Nat/Pairing.lean
index bda4acd194b8d..c417b76124131 100644
--- a/Mathlib/Data/Nat/Pairing.lean
+++ b/Mathlib/Data/Nat/Pairing.lean
@@ -45,10 +45,10 @@ theorem pair_unpair (n : ℕ) : pair (unpair n).1 (unpair n).2 = n := by
   dsimp only [unpair]; let s := sqrt n
   have sm : s * s + (n - s * s) = n := Nat.add_sub_cancel' (sqrt_le _)
   split_ifs with h
-  · simp [pair, h, sm]
+  · simp +zetaDelta [pair, h, sm]
   · have hl : n - s * s - s ≤ s := Nat.sub_le_iff_le_add.2
       (Nat.sub_le_iff_le_add'.2 <| by rw [← Nat.add_assoc]; apply sqrt_le_add)
-    simp [pair, hl.not_lt, Nat.add_assoc, Nat.add_sub_cancel' (le_of_not_gt h), sm]
+    simp +zetaDelta [pair, hl.not_lt, Nat.add_assoc, Nat.add_sub_cancel' (le_of_not_gt h), sm]
 
 theorem pair_unpair' {n a b} (H : unpair n = (a, b)) : pair a b = n := by
   simpa [H] using pair_unpair n
@@ -80,7 +80,7 @@ theorem pair_eq_pair {a b c d : ℕ} : pair a b = pair c d ↔ a = c ∧ b = d :
 theorem unpair_lt {n : ℕ} (n1 : 1 ≤ n) : (unpair n).1 < n := by
   let s := sqrt n
   simp only [unpair, Nat.sub_le_iff_le_add]
-  by_cases h : n - s * s < s <;> simp only [h, ↓reduceIte]
+  by_cases h : n - s * s < s <;> simp +zetaDelta [h, ↓reduceIte]
   · exact lt_of_lt_of_le h (sqrt_le_self _)
   · simp only [not_lt] at h
     have s0 : 0 < s := sqrt_pos.2 n1
diff --git a/Mathlib/Order/CompleteBooleanAlgebra.lean b/Mathlib/Order/CompleteBooleanAlgebra.lean
index 352874a908984..8fac147e0686c 100644
--- a/Mathlib/Order/CompleteBooleanAlgebra.lean
+++ b/Mathlib/Order/CompleteBooleanAlgebra.lean
@@ -235,7 +235,7 @@ lemma iInf_iSup_eq' (f : ∀ a, κ a → α) :
   refine le_antisymm ?_ le_iInf_iSup
   calc
     _ = ⨅ a : range (range <| f ·), ⨆ b : a.1, b.1 := by
-      simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]
+      simp_rw +zetaDelta [iInf_subtype, iInf_range, iSup_subtype, iSup_range]
     _ = _ := minAx.iInf_iSup_eq _
     _ ≤ _ := iSup_le fun g => by
       refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2
@@ -269,9 +269,10 @@ abbrev toCompleteDistribLattice : CompleteDistribLattice.MinimalAxioms α where
       _ = ⨅ i : ULift.{u} Bool, ⨆ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
           match i with
           | .up true => a
-          | .up false => j := by simp [le_antisymm_iff, sSup_eq_iSup', iSup_unique, iInf_bool_eq]
+          | .up false => j := by
+            simp +zetaDelta [le_antisymm_iff, sSup_eq_iSup', iSup_unique, iInf_bool_eq]
       _ ≤ _ := by
-        simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
+        simp +zetaDelta only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
         exact fun x ↦ le_biSup _ (x (.up false)).2
   iInf_sup_le_sup_sInf a s := by
     let _ := minAx.toCompleteLattice
@@ -280,9 +281,9 @@ abbrev toCompleteDistribLattice : CompleteDistribLattice.MinimalAxioms α where
           match i with
           | .up true => a
           | .up false => j := by
-        simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
-        exact fun x ↦ biInf_le _ (x (.up false)).2
-      _ = _ := by simp [le_antisymm_iff, sInf_eq_iInf', iInf_unique, iSup_bool_eq]
+            simp +zetaDelta only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
+            exact fun x ↦ biInf_le _ (x (.up false)).2
+      _ = _ := by simp +zetaDelta [le_antisymm_iff, sInf_eq_iInf', iInf_unique, iSup_bool_eq]
 
 /-- The `CompletelyDistribLattice.MinimalAxioms` element corresponding to a frame. -/
 def of [CompletelyDistribLattice α] : MinimalAxioms α := { ‹CompletelyDistribLattice α› with }
diff --git a/Mathlib/Order/Hom/Lattice.lean b/Mathlib/Order/Hom/Lattice.lean
index 3a2945e4b903f..1bf8dba66906e 100644
--- a/Mathlib/Order/Hom/Lattice.lean
+++ b/Mathlib/Order/Hom/Lattice.lean
@@ -806,7 +806,7 @@ def subtypeVal {P : β → Prop}
     SupBotHom {x : β // P x} β :=
   letI := Subtype.orderBot Pbot
   letI := Subtype.semilatticeSup Psup
-  .mk (SupHom.subtypeVal Psup) (by simp [Subtype.coe_bot Pbot])
+  .mk (SupHom.subtypeVal Psup) (by simp +zetaDelta [Subtype.coe_bot Pbot])
 
 @[simp]
 lemma subtypeVal_apply {P : β → Prop}
@@ -957,7 +957,7 @@ def subtypeVal {P : β → Prop}
     InfTopHom {x : β // P x} β :=
   letI := Subtype.orderTop Ptop
   letI := Subtype.semilatticeInf Pinf
-  .mk (InfHom.subtypeVal Pinf) (by simp [Subtype.coe_top Ptop])
+  .mk (InfHom.subtypeVal Pinf) (by simp +zetaDelta [Subtype.coe_top Ptop])
 
 @[simp]
 lemma subtypeVal_apply {P : β → Prop}
@@ -1287,7 +1287,8 @@ def subtypeVal {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤)
     BoundedLatticeHom {x : β // P x} β :=
   letI := Subtype.lattice Psup Pinf
   letI := Subtype.boundedOrder Pbot Ptop
-  .mk (.subtypeVal Psup Pinf) (by simp [Subtype.coe_top Ptop]) (by simp [Subtype.coe_bot Pbot])
+  .mk (.subtypeVal Psup Pinf) (by simp +zetaDelta [Subtype.coe_top Ptop])
+    (by simp +zetaDelta [Subtype.coe_bot Pbot])
 
 @[simp]
 lemma subtypeVal_apply {P : β → Prop}