diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 77efa5a68d..b51e8d3865 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -821,7 +821,7 @@ decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
   induction a, i, h using Array.eraseIdx.induct with
   | @case1 a i h h' a' ih =>
     unfold eraseIdx
-    simp [h', a', ih]
+    simp +zetaDelta [h', a', ih]
   | case2 a i h h' =>
     unfold eraseIdx
     simp [h']
diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean
index e01f043353..5fb32bf0b5 100644
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -332,7 +332,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
       simp [enumFrom, f]
   rw [← Array.foldr_toList]
-  simp [go]
+  simp +zetaDelta [go]
 
 /-! ## Other list operations -/
 
diff --git a/src/Lean/Data/RArray.lean b/src/Lean/Data/RArray.lean
index 54b7fd5612..a1b9d66d25 100644
--- a/src/Lean/Data/RArray.lean
+++ b/src/Lean/Data/RArray.lean
@@ -55,7 +55,7 @@ where
   go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by
     induction lb, ub, h1, h2 using RArray.ofFn.go.induct (n := n)
     case case1 => simp [ofFn.go, size]; omega
-    case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega
+    case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega
 
 section Meta
 open Lean
diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean
index 9e2dce4bdf..2948a36f61 100644
--- a/src/Lean/Elab/PatternVar.lean
+++ b/src/Lean/Elab/PatternVar.lean
@@ -159,7 +159,7 @@ private def processVar (idStx : Syntax) : M Syntax := do
 private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool := Id.run do
   if h₁ : s₁.vars.size = s₂.vars.size then
     for h₂ : i in [startingAt:s₁.vars.size] do
-      if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all) then return false
+      if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all +zetaDelta) then return false
     true
   else
     false
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index e7bbedcd80..1bcf5a319b 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -173,68 +173,71 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
     syntax simpErase := "-" ident
     -/
     let go := withMainContext do
-      let mut thmsArray := ctx.simpTheorems
-      let mut thms      := thmsArray[0]!
-      let mut simprocs  := simprocs
-      let mut starArg   := false
-      for arg in stx[1].getSepArgs do
-        try -- like withLogging, but compatible with do-notation
-          if arg.getKind == ``Lean.Parser.Tactic.simpErase then
-            let fvar? ← if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none
-            if let some fvar := fvar? then
-              -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
-              thms := thms.eraseCore (.fvar fvar.fvarId!)
-            else
-              let id := arg[1]
-              if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
-                if (← Simp.isSimproc declName) then
-                  simprocs := simprocs.erase declName
-                else if ctx.config.autoUnfold then
-                  thms := thms.eraseCore (.decl declName)
-                else
-                  thms ← withRef id <| thms.erase (.decl declName)
+      let zetaDeltaSet ← toZetaDeltaSet stx ctx
+      withTrackingZetaDeltaSet zetaDeltaSet do
+        let mut thmsArray := ctx.simpTheorems
+        let mut thms      := thmsArray[0]!
+        let mut simprocs  := simprocs
+        let mut starArg   := false
+        for arg in stx[1].getSepArgs do
+          try -- like withLogging, but compatible with do-notation
+            if arg.getKind == ``Lean.Parser.Tactic.simpErase then
+              let fvar? ← if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none
+              if let some fvar := fvar? then
+                -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
+                thms := thms.eraseCore (.fvar fvar.fvarId!)
               else
-                -- If `id` could not be resolved, we should check whether it is a builtin simproc.
-                -- before returning error.
-                let name := id.getId.eraseMacroScopes
-                if (← Simp.isBuiltinSimproc name) then
-                  simprocs := simprocs.erase name
+                let id := arg[1]
+                if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
+                  if (← Simp.isSimproc declName) then
+                    simprocs := simprocs.erase declName
+                  else if ctx.config.autoUnfold then
+                    thms := thms.eraseCore (.decl declName)
+                  else
+                    thms ← withRef id <| thms.erase (.decl declName)
                 else
-                  withRef id <| throwUnknownConstant name
-          else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
-            let post :=
-              if arg[0].isNone then
-                true
-              else
-                arg[0][0].getKind == ``Parser.Tactic.simpPost
-            let inv  := !arg[1].isNone
-            let term := arg[2]
-            match (← resolveSimpIdTheorem? term) with
-            | .expr e  =>
-              let name ← mkFreshId
-              thms ← addDeclToUnfoldOrTheorem ctx.indexConfig thms (.stx name arg) e post inv kind
-            | .simproc declName =>
-              simprocs ← simprocs.add declName post
-            | .ext (some ext₁) (some ext₂) _ =>
-              thmsArray := thmsArray.push (← ext₁.getTheorems)
-              simprocs  := simprocs.push (← ext₂.getSimprocs)
-            | .ext (some ext₁) none _ =>
-              thmsArray := thmsArray.push (← ext₁.getTheorems)
-            | .ext none (some ext₂) _ =>
-              simprocs  := simprocs.push (← ext₂.getSimprocs)
-            | .none    =>
-              let name ← mkFreshId
-              thms ← addSimpTheorem ctx.indexConfig thms (.stx name arg) term post inv
-          else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
-            starArg := true
-          else
-            throwUnsupportedSyntax
-        catch ex =>
-          if (← read).recover then
-            logException ex
-          else
-            throw ex
-      return { ctx := ctx.setSimpTheorems (thmsArray.set! 0 thms), simprocs, starArg }
+                  -- If `id` could not be resolved, we should check whether it is a builtin simproc.
+                  -- before returning error.
+                  let name := id.getId.eraseMacroScopes
+                  if (← Simp.isBuiltinSimproc name) then
+                    simprocs := simprocs.erase name
+                  else
+                    withRef id <| throwUnknownConstant name
+            else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
+              let post :=
+                if arg[0].isNone then
+                  true
+                else
+                  arg[0][0].getKind == ``Parser.Tactic.simpPost
+              let inv  := !arg[1].isNone
+              let term := arg[2]
+              match (← resolveSimpIdTheorem? term) with
+              | .expr e  =>
+                let name ← mkFreshId
+                thms ← addDeclToUnfoldOrTheorem ctx.indexConfig thms (.stx name arg) e post inv kind
+              | .simproc declName =>
+                simprocs ← simprocs.add declName post
+              | .ext (some ext₁) (some ext₂) _ =>
+                thmsArray := thmsArray.push (← ext₁.getTheorems)
+                simprocs  := simprocs.push (← ext₂.getSimprocs)
+              | .ext (some ext₁) none _ =>
+                thmsArray := thmsArray.push (← ext₁.getTheorems)
+              | .ext none (some ext₂) _ =>
+                simprocs  := simprocs.push (← ext₂.getSimprocs)
+              | .none    =>
+                let name ← mkFreshId
+                thms ← addSimpTheorem ctx.indexConfig thms (.stx name arg) term post inv
+            else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
+              starArg := true
+            else
+              throwUnsupportedSyntax
+          catch ex =>
+            if (← read).recover then
+              logException ex
+            else
+              throw ex
+        let ctx := ctx.setZetaDeltaSet zetaDeltaSet (← getZetaDeltaFVarIds)
+        return { ctx := ctx.setSimpTheorems (thmsArray.set! 0 thms), simprocs, starArg }
     -- If recovery is disabled, then we want simp argument elaboration failures to be exceptions.
     -- This affects `addSimpTheorem`.
     if (← read).recover then
@@ -277,6 +280,20 @@ where
       else
         return .none
 
+  /-- If `zetaDelta := false`, create a `FVarId` set with all local let declarations in the `simp` argument list. -/
+  toZetaDeltaSet (stx : Syntax) (ctx : Simp.Context) : TacticM FVarIdSet := do
+    if ctx.config.zetaDelta then return {}
+    Term.withoutCheckDeprecated do -- We do not want to report deprecated constants in the first pass
+      let mut s : FVarIdSet := {}
+      for arg in stx[1].getSepArgs do
+        if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
+          if arg[0].isNone && arg[1].isNone then
+            let term := arg[2]
+            let .expr (.fvar fvarId) ← resolveSimpIdTheorem? term | pure ()
+            if (← fvarId.getDecl).isLet then
+              s := s.insert fvarId
+      return s
+
 @[inline] def simpOnlyBuiltins : List Name := [``eq_self, ``iff_self]
 
 structure MkSimpContextResult where
@@ -323,7 +340,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     let simprocs := r.simprocs
     let mut simpTheorems := ctx.simpTheorems
     /-
-    When using `zeta := false`, we do not expand let-declarations when using `[*]`.
+    When using `zetaDelta := false`, we do not expand let-declarations when using `[*]`.
     Users must explicitly include it in the list.
     -/
     let hs ← getPropHyps
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index f199e067b6..1bc9c0b904 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -326,6 +326,10 @@ structure Context where
   `refine' (fun x => _)
   -/
   holesAsSyntheticOpaque : Bool := false
+  /--
+  If `checkDeprecated := true`, then `Linter.checkDeprecated` when creating constants.
+  -/
+  checkDeprecated : Bool := true
 
 abbrev TermElabM := ReaderT Context $ StateRefT State MetaM
 abbrev TermElab  := Syntax → Option Expr → TermElabM Expr
@@ -2026,6 +2030,10 @@ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do
   trace[Elab.letrec] "mvarId root: {mkMVar mvarId}"
   return (← get).letRecsToLift.any (·.mvarId == mvarId)
 
+private def checkDeprecatedCore (constName : Name) : TermElabM Unit := do
+  if (← read).checkDeprecated then
+    Linter.checkDeprecated constName
+
 /--
   Create an `Expr.const` using the given name and explicit levels.
   Remark: fresh universe metavariables are created if the constant has more universe
@@ -2033,9 +2041,8 @@ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do
 
   If `checkDeprecated := true`, then `Linter.checkDeprecated` is invoked.
 -/
-def mkConst (constName : Name) (explicitLevels : List Level := []) (checkDeprecated := true) : TermElabM Expr := do
-  if checkDeprecated then
-    Linter.checkDeprecated constName
+def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do
+  checkDeprecatedCore constName
   let cinfo ← getConstInfo constName
   if explicitLevels.length > cinfo.levelParams.length then
     throwError "too many explicit universe levels for '{constName}'"
@@ -2046,7 +2053,10 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) (checkDepreca
 
 def checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit := do
   if let .const declName _ := e.getAppFn then
-    withRef ref do Linter.checkDeprecated declName
+    withRef ref do checkDeprecatedCore declName
+
+@[inline] def withoutCheckDeprecated [MonadWithReaderOf Context m] : m α → m α :=
+  withTheReader Context (fun ctx => { ctx with checkDeprecated := false })
 
 private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do
@@ -2058,7 +2068,7 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     At `elabAppFnId`, we perform the check when converting the list returned by `resolveName'` into a list of
     `TermElabResult`s.
     -/
-    let const ← mkConst declName explicitLevels (checkDeprecated := false)
+    let const ← withoutCheckDeprecated <| mkConst declName explicitLevels
     return (const, projs) :: result
 
 def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 581fe806a2..37e0749abb 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -141,18 +141,6 @@ structure Config where
     Controls which definitions and theorems can be unfolded by `isDefEq` and `whnf`.
    -/
   transparency       : TransparencyMode := TransparencyMode.default
-  /--
-  When `trackZetaDelta = true`, we track all free variables that have been zetaDelta-expanded.
-  That is, suppose the local context contains
-  the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaDeltaFVarIds`.
-  We use `trackZetaDelta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`.
-  When we find these declarations we set their `nonDep` flag with `true`.
-  To find these let-declarations in a given term `s`, we
-  1- Reset `State.zetaDeltaFVarIds`
-  2- Set `trackZetaDelta := true`
-  3- Type-check `s`.
-  -/
-  trackZetaDelta     : Bool := false
   /-- Eta for structures configuration mode. -/
   etaStruct          : EtaStructMode := .all
   /--
@@ -187,7 +175,7 @@ structure Config where
   Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
   -/
   zetaDelta : Bool := true
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 /-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results -/
 private def Config.toKey (c : Config) : UInt64 :=
@@ -419,7 +407,7 @@ structure Diagnostics where
 structure State where
   mctx             : MetavarContext := {}
   cache            : Cache := {}
-  /-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta-expanded by `MetaM` is stored in `zetaDeltaFVarIds`. -/
+  /-- When `Context.trackZetaDelta == true`, then any let-decl free variable that is zetaDelta-expanded by `MetaM` is stored in `zetaDeltaFVarIds`. -/
   zetaDeltaFVarIds : FVarIdSet := {}
   /-- Array of postponed universe level constraints -/
   postponed        : PersistentArray PostponedEntry := {}
@@ -445,6 +433,28 @@ register_builtin_option maxSynthPendingDepth : Nat := {
 structure Context where
   private config    : Config               := {}
   private configKey : UInt64               := config.toKey
+  /--
+  When `trackZetaDelta = true`, we track all free variables that have been zetaDelta-expanded.
+  That is, suppose the local context contains
+  the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaDeltaFVarIds`.
+  We use `trackZetaDelta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`.
+  When we find these declarations we set their `nonDep` flag with `true`.
+  To find these let-declarations in a given term `s`, we
+  1- Reset `State.zetaDeltaFVarIds`
+  2- Set `trackZetaDelta := true`
+  3- Type-check `s`.
+
+  Note that, we do not include this field in the `Config` structure because this field is not
+  taken into account while caching results. See also field `zetaDeltaSet`.
+  -/
+  trackZetaDelta     : Bool := false
+  /--
+  If `config.zetaDelta := false`, we may select specific local declarations to be unfolded using
+  the field `zetaDeltaSet`. Note that, we do not include this field in the `Config` structure
+  because this field is not taken into account while caching results.
+  Moreover, we reset all caches whenever setting it.
+  -/
+  zetaDeltaSet : FVarIdSet := {}
   /-- Local context -/
   lctx              : LocalContext         := {}
   /-- Local instances in `lctx`. -/
@@ -1089,8 +1099,36 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 /--
 Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
 -/
-@[inline] def withTrackingZetaDelta (x : n α) : n α :=
-  withConfig (fun cfg => { cfg with trackZetaDelta := true }) x
+@[inline] def withTrackingZetaDelta : n α → n α :=
+  mapMetaM <| withReader (fun ctx => { ctx with trackZetaDelta := true })
+
+def withZetaDeltaSetImp (s : FVarIdSet) (x : MetaM α) : MetaM α := do
+  if s.isEmpty then
+    x
+  else
+    let cacheSaved := (← get).cache
+    modify fun s => { s with cache := {} }
+    try
+      withReader (fun ctx => { ctx with zetaDeltaSet := s }) x
+    finally
+      modify fun s => { s with cache := cacheSaved }
+
+/--
+`withZetaDeltaSet s x` executes `x` with `zetaDeltaSet := s`.
+The cache is reset while executing `x` if `s` is not empty.
+-/
+def withZetaDeltaSet (s : FVarIdSet) : n α → n α :=
+  mapMetaM <| withZetaDeltaSetImp s
+
+/--
+Similar to `withZetaDeltaSet`, but also enables `withTrackingZetaDelta` if
+`s` is not empty.
+-/
+def withTrackingZetaDeltaSet (s : FVarIdSet) (x : n α) : n α := do
+  if s.isEmpty then
+    x
+  else
+    withZetaDeltaSet s <| withTrackingZetaDelta x
 
 @[inline] def withoutProofIrrelevance (x : n α) : n α :=
   withConfig (fun cfg => { cfg with proofIrrelevance := false }) x
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index b9e8bd9016..71ef14f4d0 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -304,14 +304,14 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
     if info.isInstImplicit then
       discard <| trySynthPending a₁
       discard <| trySynthPending a₂
-    unless (← withAtLeastTransparency TransparencyMode.default <| Meta.isExprDefEqAux a₁ a₂) do
+    unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do
       return false
   for i in postponedHO do
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
     let info := finfo.paramInfo[i]!
     if info.isInstImplicit then
-      unless (← withAtLeastTransparency TransparencyMode.default <| Meta.isExprDefEqAux a₁ a₂) do
+      unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do
        return false
     else
       unless (← Meta.isExprDefEqAux a₁ a₂) do
@@ -380,12 +380,13 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
     else
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
-      let vType ← inferType v
-      if (← withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then
-        mvar.mvarId!.assign v
-        pure true
-      else
-        pure false
+      withInferTypeConfig do
+        let vType ← inferType v
+        if (← Meta.isExprDefEqAux mvarType vType) then
+          mvar.mvarId!.assign v
+          pure true
+        else
+          pure false
 
 /--
 Auxiliary method for solving constraints of the form `?m xs := v`.
@@ -1582,7 +1583,7 @@ private def etaEq (t s : Expr) : Bool :=
   Then, we can enable the flag only when applying `simp` and `rw` theorems.
 -/
 private def withProofIrrelTransparency (k : MetaM α) : MetaM α :=
-  withAtLeastTransparency .default k
+  withInferTypeConfig k
 
 private def isDefEqProofIrrel (t s : Expr) : MetaM LBool := do
   if (← getConfig).proofIrrelevance then
diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 710d385450..82a447c0d3 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -177,15 +177,20 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
         modifyInferTypeCache fun c => c.insert key type
       return type
 
-private def defaultConfig : ConfigWithKey :=
-  { : Config }.toConfigWithKey
-
-private def allConfig : ConfigWithKey :=
-  { transparency := .all : Config }.toConfigWithKey
+/--
+Ensure `MetaM` configuration is strong enough for inferring/checking types.
+For example, `beta := true` is essential when type checking.
 
-@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := do
-  let cfg := if (← getTransparency) == .all then allConfig else defaultConfig
-  withConfigWithKey cfg x
+Remark: we previously use the default configuration here, but this is problematic
+because it overrides unrelated configurations.
+-/
+@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α :=
+  withAtLeastTransparency .default do
+    let cfg ← getConfig
+    if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj == .yesWithDelta then
+      x
+    else
+      withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaDelta := true, proj := .yesWithDelta }) x
 
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 66a992b9bd..e9d8868787 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -57,7 +57,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
         match e? with
         | none   => pure none
         | some e =>
-          match (← reduceProj? e.getAppFn) with
+          match (← withSimpMetaConfig <| reduceProj? e.getAppFn) with
           | some f => return some (mkAppN f e.getAppArgs)
           | none   => return none
       if projInfo.fromClass then
@@ -152,7 +152,7 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
       withDefault <| unfoldDefinition? e
     else if (← isMatchDef fName) then
       let some value ← withDefault <| unfoldDefinition? e | return none
-      let .reduced value ← reduceMatcher? value | return none
+      let .reduced value ← withSimpMetaConfig <| reduceMatcher? value | return none
       return some value
     else
       return none
@@ -166,6 +166,7 @@ private def reduceStep (e : Expr) : SimpM Expr := do
   let f := e.getAppFn
   if f.isMVar then
     return (← instantiateMVars e)
+  withSimpMetaConfig do
   if cfg.beta then
     if f.isHeadBetaTargetFn false then
       return f.betaRev e.getAppRevArgs
@@ -256,7 +257,7 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
     withFreshCache do f
 
 def simpProj (e : Expr) : SimpM Result := do
-  match (← reduceProj? e) with
+  match (← withSimpMetaConfig <| reduceProj? e) with
   | some e => return { expr := e }
   | none =>
     let s := e.projExpr!
@@ -484,7 +485,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do
     let rhs := hType.appArg!
     rhs.withApp fun m zs => do
       let val ← mkLambdaFVars zs r.expr
-      unless (← isDefEq m val) do
+      unless (← withSimpMetaConfig <| isDefEq m val) do
         throwCongrHypothesisFailed
       let mut proof ← r.getProof
       if hType.isAppOf ``Iff then
@@ -528,7 +529,7 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
     let args := e.getAppArgs
     e := mkAppN e.getAppFn args[:numArgs]
     extraArgs := args[numArgs:].toArray
-  if (← isDefEq lhs e) then
+  if (← withSimpMetaConfig <| isDefEq lhs e) then
     let mut modified := false
     for i in c.hypothesesPos do
       let x := xs[i]!
@@ -766,16 +767,28 @@ where
     trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
     simpLoop e
 
--- TODO: delete
-@[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α :=
-  withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
+@[inline] private def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α := do
+  withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <|
+  withTrackingZetaDeltaSet ctx.zetaDeltaSet <|
+  withReducible x
+
+private def updateUsedSimpsWithZetaDeltaCore (s : UsedSimps) (usedZetaDelta : FVarIdSet) : UsedSimps :=
+  usedZetaDelta.fold (init := s) fun s fvarId =>
+    s.insert <| .fvar fvarId
+
+private def updateUsedSimpsWithZetaDelta (ctx : Context) (stats : Stats) : MetaM Stats := do
+  let used := stats.usedTheorems
+  let used := updateUsedSimpsWithZetaDeltaCore used ctx.initUsedZetaDelta
+  let used := updateUsedSimpsWithZetaDeltaCore used (← getZetaDeltaFVarIds)
+  return { stats with usedTheorems := used }
 
 def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
   let ctx ← ctx.setLctxInitIndices
   withSimpContext ctx do
     let (r, s) ← go e methods.toMethodsRef ctx |>.run { stats with }
     trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
-    return (r, { s with })
+    let s ← updateUsedSimpsWithZetaDelta ctx { s with }
+    return (r, s)
 where
   go (e : Expr) : SimpM Result :=
     tryCatchRuntimeEx
@@ -790,7 +803,8 @@ where
 def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Expr × Stats) := do
   withSimpContext ctx do
     let (r, s) ← go e methods.toMethodsRef ctx |>.run { stats with }
-    pure (r, { s with })
+    let s ← updateUsedSimpsWithZetaDelta ctx { s with }
+    pure (r, s)
 where
   go (e : Expr) : SimpM Expr :=
     tryCatchRuntimeEx
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index b68829fa9b..906cb24054 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -117,7 +117,7 @@ private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   recordTriedSimpTheorem thm.origin
   let rec go (e : Expr) : SimpM (Option Result) := do
-    if (← isDefEq lhs e) then
+    if (← withSimpMetaConfig <| isDefEq lhs e) then
       unless (← synthesizeArgs thm.origin bis xs) do
         return none
       let proof? ← if (← useImplicitDefEqProof thm) then
@@ -342,7 +342,7 @@ def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do
 def simpMatch : Simproc := fun e => do
   unless (← getConfig).iota do
     return .continue
-  if let some e ← reduceRecMatcher? e then
+  if let some e ← withSimpMetaConfig <| reduceRecMatcher? e then
     return .visit { expr := e }
   let .const declName _ := e.getAppFn
     | return .continue
@@ -549,7 +549,7 @@ private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
     -- well-behaved discharger. See comment at `Methods.wellBehavedDischarge`
     else if !contextual && localDecl.index >= lctxInitIndices then
       return none
-    else if (← isDefEq e localDecl.type) then
+    else if (← withSimpMetaConfig <| isDefEq e localDecl.type) then
       return some localDecl.toExpr
     else
       return none
@@ -591,7 +591,7 @@ def dischargeRfl (e : Expr) : SimpM (Option Expr) := do
   forallTelescope e fun xs e => do
     let some (t, a, b) := e.eq? | return .none
     unless a.getAppFn.isMVar || b.getAppFn.isMVar do return .none
-    if (← withReducible <| isDefEq a b) then
+    if (← withSimpMetaConfig <| isDefEq a b) then
       trace[Meta.Tactic.simp.discharge] "Discharging with rfl: {e}"
       let u ← getLevel t
       let proof := mkApp2 (.const ``rfl [u]) t a
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 786ea79c82..f730a0915b 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -54,6 +54,12 @@ abbrev CongrCache := ExprMap (Option CongrTheorem)
 structure Context where
   private mk ::
   config            : Config := {}
+  /-- Local declarations to propagate to `Meta.Context` -/
+  zetaDeltaSet      : FVarIdSet := {}
+  /--
+  When processing `Simp` arguments, `zetaDelta` may be performed if `zetaDeltaSet` is not empty.
+  We save the local free variable ids in `initUsedZetaDelta`. `initUsedZetaDelta` is a subset of `zetaDeltaSet`. -/
+  initUsedZetaDelta : FVarIdSet := {}
   metaConfig        : ConfigWithKey := default
   indexConfig       : ConfigWithKey := default
   /-- `maxDischargeDepth` from `config` as an `UInt32`. -/
@@ -122,8 +128,18 @@ private def updateArith (c : Config) : CoreM Config := do
 /--
 Converts `Simp.Config` into `Meta.ConfigWithKey` used for indexing.
 -/
-private def mkIndexConfig (c : Config) : ConfigWithKey :=
-  { c with
+private def mkIndexConfig (c : Config) : MetaM ConfigWithKey := do
+  let curr ← Meta.getConfig
+  return { curr with
+    beta         := c.beta
+    iota         := c.iota
+    zeta         := c.zeta
+    zetaDelta    := c.zetaDelta
+    etaStruct    := c.etaStruct
+    /-
+    When indexing terms we disable projection to ensure a term such as `f ((a, b).1)`
+    is an instance of the pattern `f (?x.1)`
+    -/
     proj         := .no
     transparency := .reducible
   : Meta.Config }.toConfigWithKey
@@ -131,9 +147,14 @@ private def mkIndexConfig (c : Config) : ConfigWithKey :=
 /--
 Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`.
 -/
--- TODO: use `metaConfig` at `isDefEq`. It is not being used yet because it will break Mathlib.
-private def mkMetaConfig (c : Config) : ConfigWithKey :=
-  { c with
+private def mkMetaConfig (c : Config) : MetaM ConfigWithKey := do
+  let curr ← Meta.getConfig
+  return { curr with
+    beta         := c.beta
+    zeta         := c.zeta
+    iota         := c.iota
+    zetaDelta    := c.zetaDelta
+    etaStruct    := c.etaStruct
     proj         := if c.proj then .yesWithDelta else .no
     transparency := .reducible
   : Meta.Config }.toConfigWithKey
@@ -142,12 +163,16 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (
   let config ← updateArith config
   return {
     config, simpTheorems, congrTheorems
-    metaConfig := mkMetaConfig config
-    indexConfig := mkIndexConfig config
+    metaConfig := (← mkMetaConfig config)
+    indexConfig := (← mkIndexConfig config)
   }
 
-def Context.setConfig (context : Context) (config : Config) : Context :=
-  { context with config }
+def Context.setConfig (context : Context) (config : Config) : MetaM Context := do
+  return { context with
+    config
+    metaConfig := (← mkMetaConfig config)
+    indexConfig := (← mkIndexConfig config)
+  }
 
 def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
   { c with simpTheorems }
@@ -164,6 +189,9 @@ def Context.setFailIfUnchanged (c : Context) (flag : Bool) : Context :=
 def Context.setMemoize (c : Context) (flag : Bool) : Context :=
   { c with config.memoize := flag }
 
+def Context.setZetaDeltaSet (c : Context) (zetaDeltaSet : FVarIdSet) (initUsedZetaDelta : FVarIdSet) : Context :=
+  { c with zetaDeltaSet, initUsedZetaDelta }
+
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
@@ -237,6 +265,12 @@ For example, if the user has set `simp (config := { zeta := false })`,
 @[inline] def withSimpIndexConfig (x : SimpM α) : SimpM α := do
   withConfigWithKey (← readThe Simp.Context).indexConfig x
 
+/--
+Executes `x` using a `MetaM` configuration for inferred from `Simp.Config`.
+-/
+@[inline] def withSimpMetaConfig (x : SimpM α) : SimpM α := do
+  withConfigWithKey (← readThe Simp.Context).metaConfig x
+
 @[extern "lean_simp"]
 opaque simp (e : Expr) : SimpM Result
 
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 067ab7d7bb..bad1ed8cc3 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -349,8 +349,10 @@ end
       -- Let-declarations marked as implementation detail should always be unfolded
       -- We initially added this feature for `simp`, and added it here for consistency.
       let cfg ← getConfig
-      unless cfg.zetaDelta || decl.isImplementationDetail do return e
-      if cfg.trackZetaDelta then
+      if !decl.isImplementationDetail && !cfg.zetaDelta then
+        if !(← read).zetaDeltaSet.contains fvarId then
+          return e
+      if (← read).trackZetaDelta then
         modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId }
       whnfEasyCases v k
   | .mvar mvarId   =>
@@ -572,7 +574,17 @@ where
             return (← go <| mkAppN (b.instantiate1 v) args)
         let f := f.getAppFn
         let f' ← go f
-        if cfg.beta && f'.isLambda then
+        /-
+        If `f'` is a lambda, then we perform beta-reduction here IF
+        1- `cfg.beta` is enabled, OR
+        2- `f` was not a lambda expression. That is, `f` was reduced, and the beta-reduction step is part
+           of this step. This is similar to allowing beta-reduction while unfolding expressions even if `cfg.beta := false`.
+
+        We added case 2 because a failure at `norm_cast`. See test `6123_mod_cast.lean`.
+        Another possible fix to this test is to set `beta := true` at the `Simp.Config` value at
+        `NormCast.lean`.
+        -/
+        if f'.isLambda && (cfg.beta || !f.isLambda) then
           let revArgs := e.getAppRevArgs
           go <| f'.betaRev revArgs
         else if let some eNew ← whnfDelayedAssigned? f' e then
diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index cf12873255..4a12ef54dc 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -471,7 +471,7 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
       have := input.lhs.ref.hgate
       have := input.rhs.ref.hgate
       omega
-  ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩
+  ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
 
 /--
 Add a new input node to the AIG in `aig`. Note that this version is only meant for proving,
@@ -487,7 +487,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α :=
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction
-  ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩
+  ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
 
 /--
 Add a new constant node to `aig`. Note that this version is only meant for proving,
@@ -503,7 +503,7 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α :=
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction
-  ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩
+  ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
 
 end AIG
 
diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean
index 95ecaa3ae8..b43ced351d 100644
--- a/src/Std/Sat/AIG/CNF.lean
+++ b/src/Std/Sat/AIG/CNF.lean
@@ -505,7 +505,7 @@ def State.addConst (state : State aig) (idx : Nat) (h : idx < aig.decls.size)
   let newCnf := Decl.constToCNF (.inr ⟨idx, h⟩) b
   have hinv := toCNF.State.Inv_constToCNF htip
   let ⟨cache, hcache⟩ := cache.addConst idx h htip
-  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩
+  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩
 
 /--
 Add the CNF for a `Decl.atom` to the state.
@@ -517,7 +517,7 @@ def State.addAtom (state : State aig) (idx : Nat) (h : idx < aig.decls.size)
   let newCnf := Decl.atomToCNF (.inr ⟨idx, h⟩) (.inl a)
   have hinv := toCNF.State.Inv_atomToCNF htip
   let ⟨cache, hcache⟩ := cache.addAtom idx h htip
-  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩
+  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩
 
 /--
 Add the CNF for a `Decl.gate` to the state.
@@ -537,7 +537,7 @@ def State.addGate (state : State aig) {hlb} {hrb} (idx : Nat) (h : idx < aig.dec
       rinv
   have hinv := toCNF.State.Inv_gateToCNF htip
   let ⟨cache, hcache⟩ := cache.addGate idx h htip hl hr
-  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩
+  ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩
 
 /--
 Evaluate the CNF contained within the state.
diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean
index f06433ffaa..ae33a83460 100644
--- a/src/Std/Sat/AIG/Relabel.lean
+++ b/src/Std/Sat/AIG/Relabel.lean
@@ -65,7 +65,7 @@ def relabel (r : α → β) (aig : AIG α) : AIG β :=
     cache,
     invariant := by
       intro idx lhs rhs linv rinv hbound hgate
-      simp [decls] at hgate
+      simp +zetaDelta [decls] at hgate
       have := Decl.relabel_gate hgate
       apply aig.invariant
       assumption
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
index be25f5ad8b..ac09debb1f 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
@@ -224,7 +224,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p
             have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
               ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
                (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
-            simp only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints,
+            simp +zetaDelta only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints,
               clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
               restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
               clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index 5603cfec86..ee001fdb78 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -111,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           ⟨units.size, units_size_lt_updatedUnits_size⟩
         have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
         refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
-        simp only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
+        simp +zetaDelta only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
         constructor
         · rfl
         · constructor
@@ -131,7 +131,6 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                   exact k_property
                 · intro h
                   simp only [← h, not_true, mostRecentUnitIdx] at hk
-                  exact hk rfl
               rw [Array.getElem_push_lt _ _ _ k_in_bounds]
               rw [i_eq_l] at h2
               exact h2 ⟨k.1, k_in_bounds⟩
@@ -193,7 +192,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           constructor
           · rw [Array.getElem_push_lt units l j.1 j.2, h1]
           · constructor
-            · simp [i_eq_l, ← hl]
+            · simp +zetaDelta [i_eq_l, ← hl]
               rfl
             · constructor
               · simp only [i_eq_l]
@@ -228,7 +227,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩
           simp [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq]
           constructor
-          · simp [i_eq_l, ← hl]
+          · simp +zetaDelta [i_eq_l, ← hl]
             rfl
           · constructor
             · rw [Array.getElem_push_lt units l j.1 j.2, h1]
@@ -1328,7 +1327,7 @@ theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (ru
         have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
           rw [size_assignments_insertRupUnits f (negate c)]
           exact f_readyForRupAdd.2.1
-        simp only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
+        simp +zetaDelta only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
           restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at rupAddSuccess
         have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by
           rw [rupAddSuccess]
diff --git a/src/Std/Time/Date/ValidDate.lean b/src/Std/Time/Date/ValidDate.lean
index bd38c6520d..ce74efb4ee 100644
--- a/src/Std/Time/Date/ValidDate.lean
+++ b/src/Std/Time/Date/ValidDate.lean
@@ -48,7 +48,7 @@ def ofOrdinal (ordinal : Day.Ordinal.OfYear leap) : ValidDate leap :=
         let bounded := Bounded.LE.mk ordinal.val (And.intro h h₁) |>.sub acc
         let bounded : Bounded.LE 1 monthDays.val := bounded.cast (by omega) (by omega)
         let days₁ : Day.Ordinal := ⟨bounded.val, And.intro bounded.property.left (Int.le_trans bounded.property.right monthDays.property.right)⟩
-        ⟨⟨idx, days₁⟩, Int.le_trans bounded.property.right (by simp)⟩
+        ⟨⟨idx, days₁⟩, Int.le_trans bounded.property.right (by simp +zetaDelta)⟩
       else by
         let h₂ := Int.not_le.mp h₁
 
diff --git a/tests/lean/run/2670.lean b/tests/lean/run/2670.lean
index 7120e52b5e..d533c89bfc 100644
--- a/tests/lean/run/2670.lean
+++ b/tests/lean/run/2670.lean
@@ -19,5 +19,18 @@ theorem enumFrom_eq_enumFromTR' : @enumFrom = @enumFromTR' := by
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_toList]
-  simp [go] -- Should close the goal
+  rw [←Array.foldr_toList]
+  simp [f] at go -- We must unfold `f` at `go`, or use `+zetaDelta`. See next theorem
+  simp [go]
+
+open List in
+theorem enumFrom_eq_enumFromTR'' : @enumFrom = @enumFromTR' := by
+  funext α n l; simp only [enumFromTR']
+  let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
+  let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
+    | [], n => rfl
+    | a::as, n => by
+      rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as]
+      simp [enumFrom, f]
+  rw [←Array.foldr_toList]
+  simp +zetaDelta [go]
diff --git a/tests/lean/run/5455.lean b/tests/lean/run/5455.lean
new file mode 100644
index 0000000000..f963187962
--- /dev/null
+++ b/tests/lean/run/5455.lean
@@ -0,0 +1,23 @@
+variable {α : Type}
+
+theorem test1 {n : Nat} {f : Fin n → α} : False := by
+  let c (i : Fin n) : Nat := i
+  let d : Fin n → Nat × Nat := fun i => (c i, c i + 1)
+  have : ∀ i, (d i).2 ≠ c i * 2 := by
+    fail_if_success simp only -- should not unfold `d` or `i`
+    guard_target =ₛ ∀ (i : Fin n), (d i).snd ≠ c i * 2
+    simp +zetaDelta only -- `d` and `i` are now unfolded
+    guard_target =ₛ ∀ (i : Fin n), i.val + 1 ≠ i.val * 2
+    sorry
+  sorry
+
+opaque f : Nat → Nat
+axiom f_ax (x : Nat): f (f x) = x
+
+theorem test2 (a : Nat) : False := by
+  let d : Nat → Nat × Nat := fun i => (f a, i)
+  have : f (d 1).1 = a := by
+    fail_if_success simp only [f_ax] -- f_ax should be applicable
+    simp +zetaDelta only [f_ax] -- f_ax is applicable if zetaDelta := true
+    done
+  sorry
diff --git a/tests/lean/run/6123_cat_adjunction.lean b/tests/lean/run/6123_cat_adjunction.lean
new file mode 100644
index 0000000000..af810102de
--- /dev/null
+++ b/tests/lean/run/6123_cat_adjunction.lean
@@ -0,0 +1,498 @@
+section Mathlib.CategoryTheory.ConcreteCategory.Bundled
+
+universe u v
+
+namespace CategoryTheory
+
+variable {c : Type u → Type v}
+
+structure Bundled (c : Type u → Type v) : Type max (u + 1) v where
+  α : Type u
+  str : c α := by infer_instance
+
+set_option checkBinderAnnotations false in
+def Bundled.of {c : Type u → Type v} (α : Type u) [str : c α] : Bundled c :=
+  ⟨α, str⟩
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.ConcreteCategory.Bundled
+
+section Mathlib.Logic.Equiv.Defs
+
+open Function
+
+universe u v
+
+variable {α : Sort u} {β : Sort v}
+
+structure Equiv (α : Sort _) (β : Sort _) where
+  protected toFun : α → β
+  protected invFun : β → α
+
+infixl:25 " ≃ " => Equiv
+
+protected def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩
+
+end Mathlib.Logic.Equiv.Defs
+
+section Mathlib.Combinatorics.Quiver.Basic
+
+universe v v₁ v₂ u u₁ u₂
+
+class Quiver (V : Type u) where
+  Hom : V → V → Sort v
+
+infixr:10 " ⟶ " => Quiver.Hom
+
+structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where
+  obj : V → W
+  map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y)
+
+end Mathlib.Combinatorics.Quiver.Basic
+
+section Mathlib.CategoryTheory.Category.Basic
+
+universe v u
+
+namespace CategoryTheory
+
+class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
+  id : ∀ X : obj, Hom X X
+  comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
+
+scoped notation "𝟙" => CategoryStruct.id
+scoped infixr:80 " ≫ " => CategoryStruct.comp
+
+class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Category.Basic
+
+section Mathlib.CategoryTheory.Functor.Basic
+
+namespace CategoryTheory
+
+universe v v₁ v₂ v₃ u u₁ u₂ u₃
+
+structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+    extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where
+
+infixr:26 " ⥤ " => Functor
+
+namespace Functor
+
+section
+
+variable (C : Type u₁) [Category.{v₁} C]
+
+protected def id : C ⥤ C where
+  obj X := X
+  map f := f
+
+notation "𝟭" => Functor.id
+
+variable {C}
+
+theorem id_obj (X : C) : (𝟭 C).obj X = X := rfl
+
+theorem id_map {X Y : C} (f : X ⟶ Y) : (𝟭 C).map f = f := rfl
+
+end
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+  {E : Type u₃} [Category.{v₃} E]
+
+def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where
+  obj X := G.obj (F.obj X)
+  map f := G.map (F.map f)
+
+@[simp] theorem comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) : (F.comp G).obj X = G.obj (F.obj X) := rfl
+
+infixr:80 " ⋙ " => Functor.comp
+
+theorem comp_map (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) :
+    (F ⋙ G).map f = G.map (F.map f) := rfl
+
+end Functor
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Functor.Basic
+
+section Mathlib.CategoryTheory.NatTrans
+
+namespace CategoryTheory
+
+universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+
+structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where
+  app : ∀ X : C, F.obj X ⟶ G.obj X
+  naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f
+
+namespace NatTrans
+
+/-- `NatTrans.id F` is the identity natural transformation on a functor `F`. -/
+protected def id (F : C ⥤ D) : NatTrans F F where
+  app X := 𝟙 (F.obj X)
+  naturality := sorry
+
+variable {F G H : C ⥤ D}
+
+def vcomp (α : NatTrans F G) (β : NatTrans G H) : NatTrans F H where
+  app X := α.app X ≫ β.app X
+  naturality := sorry
+
+end NatTrans
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.NatTrans
+
+section Mathlib.CategoryTheory.Functor.Category
+
+namespace CategoryTheory
+
+universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
+
+variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+
+variable {C D}
+
+instance Functor.category : Category.{max u₁ v₂} (C ⥤ D) where
+  Hom F G := NatTrans F G
+  id F := NatTrans.id F
+  comp α β := NatTrans.vcomp α β
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Functor.Category
+
+section Mathlib.CategoryTheory.EqToHom
+
+universe v₁ u₁
+
+namespace CategoryTheory
+
+variable {C : Type u₁} [Category.{v₁} C]
+
+def eqToHom {X Y : C} (p : X = Y) : X ⟶ Y := by rw [p]; exact 𝟙 _
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.EqToHom
+
+section Mathlib.CategoryTheory.Functor.Const
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+open CategoryTheory
+
+namespace CategoryTheory.Functor
+
+variable (J : Type u₁) [Category.{v₁} J]
+variable {C : Type u₂} [Category.{v₂} C]
+
+def const : C ⥤ J ⥤ C where
+  obj X :=
+    { obj := fun _ => X
+      map := fun _ => 𝟙 X }
+  map f := { app := fun _ => f, naturality := sorry }
+
+end CategoryTheory.Functor
+
+
+end Mathlib.CategoryTheory.Functor.Const
+
+section Mathlib.CategoryTheory.DiscreteCategory
+
+namespace CategoryTheory
+
+universe v₁ v₂ v₃ u₁ u₁' u₂ u₃
+
+structure Discrete (α : Type u₁) where
+  as : α
+
+instance discreteCategory (α : Type u₁) : Category (Discrete α) where
+  Hom X Y := ULift (PLift (X.as = Y.as))
+  id _ := ULift.up (PLift.up rfl)
+  comp {X Y Z} g f := by
+    cases X
+    cases Y
+    cases Z
+    rcases f with ⟨⟨⟨⟩⟩⟩
+    exact g
+
+namespace Discrete
+
+variable {α : Type u₁}
+
+theorem eq_of_hom {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as :=
+  i.down.down
+
+protected abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
+  eqToHom sorry
+
+variable {C : Type u₂} [Category.{v₂} C]
+
+def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C where
+  obj := F ∘ Discrete.as
+  map {X Y} f := by
+    dsimp
+    rcases f with ⟨⟨h⟩⟩
+    exact eqToHom (congrArg _ h)
+
+end Discrete
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.DiscreteCategory
+
+section Mathlib.CategoryTheory.Types
+
+namespace CategoryTheory
+
+universe v v' w u u'
+
+instance types : Category (Type u) where
+  Hom a b := a → b
+  id _ := id
+  comp f g := g ∘ f
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Types
+
+section Mathlib.CategoryTheory.Bicategory.Basic
+
+namespace CategoryTheory
+
+universe w v u
+
+open Category
+
+class Bicategory (B : Type u) extends CategoryStruct.{v} B where
+  homCategory : ∀ a b : B, Category.{w} (a ⟶ b) := by infer_instance
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Bicategory.Basic
+
+section Mathlib.CategoryTheory.Bicategory.Strict
+
+namespace CategoryTheory
+
+universe w v u
+
+variable (B : Type u) [Bicategory.{w, v} B]
+
+instance (priority := 100) StrictBicategory.category : Category B where
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Bicategory.Strict
+
+section Mathlib.CategoryTheory.Category.Cat
+
+universe v u
+
+namespace CategoryTheory
+
+open Bicategory
+
+def Cat :=
+  Bundled Category.{v, u}
+
+namespace Cat
+
+instance : CoeSort Cat (Type u) :=
+  ⟨Bundled.α⟩
+
+instance str (C : Cat.{v, u}) : Category.{v, u} C :=
+  Bundled.str C
+
+def of (C : Type u) [Category.{v} C] : Cat.{v, u} :=
+  Bundled.of C
+
+instance bicategory : Bicategory.{max v u, max v u} Cat.{v, u} where
+  Hom C D := C ⥤ D
+  id C := 𝟭 C
+  comp F G := F ⋙ G
+  homCategory := fun _ _ => Functor.category
+
+@[simp] theorem of_α (C) [Category C] : (of C).α = C := rfl
+
+def objects : Cat.{v, u} ⥤ Type u where
+  obj C := C
+  map F := F.obj
+
+instance (X : Cat.{v, u}) : Category (objects.obj X) := (inferInstance : Category X)
+
+end Cat
+
+def typeToCat : Type u ⥤ Cat where
+  obj X := Cat.of (Discrete X)
+  map := fun {X} {Y} f => by
+    dsimp
+    exact Discrete.functor (Discrete.mk ∘ f)
+
+@[simp] theorem typeToCat_obj (X : Type u) : typeToCat.obj X = Cat.of (Discrete X) := rfl
+@[simp] theorem typeToCat_map {X Y : Type u} (f : X ⟶ Y) :
+  typeToCat.map f = Discrete.functor (Discrete.mk ∘ f) := rfl
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.Category.Cat
+
+section Mathlib.CategoryTheory.Adjunction.Basic
+
+namespace CategoryTheory
+
+open Category
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+
+structure Adjunction (F : C ⥤ D) (G : D ⥤ C) where
+  unit : 𝟭 C ⟶ F.comp G
+  counit : G.comp F ⟶ 𝟭 D
+
+infixl:15 " ⊣ " => Adjunction
+
+namespace Adjunction
+
+structure CoreHomEquivUnitCounit (F : C ⥤ D) (G : D ⥤ C) where
+  homEquiv : ∀ X Y, (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
+  unit : 𝟭 C ⟶ F ⋙ G
+  counit : G ⋙ F ⟶ 𝟭 D
+  homEquiv_counit : ∀ {X Y g}, (homEquiv X Y).symm.toFun g = F.map g ≫ counit.app Y
+
+variable {F : C ⥤ D} {G : D ⥤ C}
+
+def mk' (adj : CoreHomEquivUnitCounit F G) : F ⊣ G where
+  unit := adj.unit
+  counit := adj.counit
+
+end Adjunction
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.Adjunction.Basic
+
+section Mathlib.CategoryTheory.IsConnected
+
+universe w₁ w₂ v₁ v₂ u₁ u₂
+
+noncomputable section
+
+open CategoryTheory.Category
+
+namespace CategoryTheory
+
+class IsPreconnected (J : Type u₁) [Category.{v₁} J] : Prop where
+  iso_constant :
+    ∀ {α : Type u₁} (F : J ⥤ Discrete α) (j : J), False
+
+class IsConnected (J : Type u₁) [Category.{v₁} J] extends IsPreconnected J : Prop where
+  [is_nonempty : Nonempty J]
+
+variable {J : Type u₁} [Category.{v₁} J]
+
+def Zag (j₁ j₂ : J) : Prop := sorry
+
+def Zigzag : J → J → Prop := sorry
+
+def Zigzag.setoid (J : Type u₂) [Category.{v₁} J] : Setoid J where
+  r := Zigzag
+  iseqv := sorry
+
+end CategoryTheory
+
+end
+
+end Mathlib.CategoryTheory.IsConnected
+
+section Mathlib.CategoryTheory.ConnectedComponents
+
+universe v₁ v₂ v₃ u₁ u₂
+
+noncomputable section
+
+namespace CategoryTheory
+
+variable {J : Type u₁} [Category.{v₁} J]
+
+def ConnectedComponents (J : Type u₁) [Category.{v₁} J] : Type u₁ :=
+  Quotient (Zigzag.setoid J)
+
+def Functor.mapConnectedComponents {K : Type u₂} [Category.{v₂} K] (F : J ⥤ K)
+    (x : ConnectedComponents J) : ConnectedComponents K :=
+  x |> Quotient.lift (Quotient.mk (Zigzag.setoid _) ∘ F.obj) sorry
+
+def ConnectedComponents.functorToDiscrete   (X : Type _)
+    (f : ConnectedComponents J → X) : J ⥤ Discrete X where
+  obj Y :=  Discrete.mk (f (Quotient.mk (Zigzag.setoid _) Y))
+  map g := Discrete.eqToHom sorry
+
+def ConnectedComponents.liftFunctor (J) [Category J] {X : Type _} (F :J ⥤ Discrete X) :
+    (ConnectedComponents J → X) :=
+  Quotient.lift (fun c => (F.obj c).as) sorry
+
+end CategoryTheory
+
+end
+
+end Mathlib.CategoryTheory.ConnectedComponents
+
+universe v u
+namespace CategoryTheory.Cat
+
+variable (X : Type u) (C : Cat)
+
+private def typeToCatObjectsAdjHomEquiv : (typeToCat.obj X ⟶ C) ≃ (X ⟶ Cat.objects.obj C) where
+  toFun f x := f.obj ⟨x⟩
+  invFun := Discrete.functor
+
+private def typeToCatObjectsAdjCounitApp : (Cat.objects ⋙ typeToCat).obj C ⥤ C where
+  obj := Discrete.as
+  map := eqToHom ∘ Discrete.eq_of_hom
+
+/-- `typeToCat : Type ⥤ Cat` is left adjoint to `Cat.objects : Cat ⥤ Type` -/
+def typeToCatObjectsAdj : typeToCat ⊣ Cat.objects :=
+  Adjunction.mk' {
+    homEquiv := typeToCatObjectsAdjHomEquiv
+    unit := sorry
+    counit := {
+      app := typeToCatObjectsAdjCounitApp
+      naturality := sorry }
+    homEquiv_counit := by
+      intro X Y g
+      simp_all only [typeToCat_obj, Functor.id_obj, typeToCat_map, of_α, id_eq]
+      rfl }
+
+def connectedComponents : Cat.{v, u} ⥤ Type u where
+  obj C := ConnectedComponents C
+  map F := Functor.mapConnectedComponents F
+
+def connectedComponentsTypeToCatAdj : connectedComponents ⊣ typeToCat :=
+  Adjunction.mk' {
+    homEquiv := sorry
+    unit :=
+      { app:= fun C  ↦ ConnectedComponents.functorToDiscrete _ (𝟙 (connectedComponents.obj C))
+        naturality := by
+          intro X Y f
+          simp_all only [Functor.id_obj, Functor.comp_obj, typeToCat_obj, Functor.id_map,
+            Functor.comp_map, typeToCat_map, of_α, id_eq]
+          rfl }
+    counit := sorry
+    homEquiv_counit := sorry }
+
+end CategoryTheory.Cat
diff --git a/tests/lean/run/6123_mod_cast.lean b/tests/lean/run/6123_mod_cast.lean
new file mode 100644
index 0000000000..4bfa0cc372
--- /dev/null
+++ b/tests/lean/run/6123_mod_cast.lean
@@ -0,0 +1,189 @@
+
+section Mathlib.Order.Defs
+
+variable {α : Type _}
+
+section Preorder
+
+class Preorder (α : Type _) extends LE α, LT α where
+  le_refl : ∀ a : α, a ≤ a
+  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
+  lt := fun a b => a ≤ b ∧ ¬b ≤ a
+  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
+
+end Preorder
+
+section PartialOrder
+
+class PartialOrder (α : Type _) extends Preorder α where
+  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
+
+end PartialOrder
+
+section LinearOrder
+
+class LinearOrder (α : Type _) extends PartialOrder α, Min α, Max α, Ord α where
+  le_total (a b : α) : a ≤ b ∨ b ≤ a
+  decidableLE : DecidableRel (· ≤ · : α → α → Prop)
+  decidableEq : DecidableEq α
+  decidableLT : DecidableRel (· < · : α → α → Prop)
+  min := fun a b => if a ≤ b then a else b
+  max := fun a b => if a ≤ b then b else a
+  min_def : ∀ a b, min a b = if a ≤ b then a else b := by intros; rfl
+  max_def : ∀ a b, max a b = if a ≤ b then b else a := by intros; rfl
+  compare a b := compareOfLessAndEq a b
+  compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b
+
+end LinearOrder
+
+end Mathlib.Order.Defs
+
+section Mathlib.Order.Notation
+
+class Bot (α : Type _) where
+  bot : α
+
+notation "⊥" => Bot.bot
+
+attribute [match_pattern] Bot.bot
+
+end Mathlib.Order.Notation
+
+section Mathlib.Order.Basic
+
+variable {α : Type _}
+
+/-- An order is dense if there is an element between any pair of distinct comparable elements. -/
+class DenselyOrdered (α : Type _) [LT α] : Prop where
+  /-- An order is dense if there is an element between any pair of distinct elements. -/
+  dense : ∀ a₁ a₂ : α, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
+
+theorem exists_between [LT α] [DenselyOrdered α] : ∀ {a₁ a₂ : α}, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂ :=
+  DenselyOrdered.dense _ _
+
+theorem le_of_forall_le_of_dense [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α}
+    (h : ∀ a, a₂ < a → a₁ ≤ a) : a₁ ≤ a₂ := sorry
+
+end Mathlib.Order.Basic
+
+section Mathlib.Order.BoundedOrder
+
+universe u
+
+variable {α : Type u}
+
+/-- An order is an `OrderBot` if it has a least element.
+We state this using a data mixin, holding the value of `⊥` and the least element constraint. -/
+class OrderBot (α : Type u) [LE α] extends Bot α where
+  /-- `⊥` is the least element -/
+  bot_le : ∀ a : α, ⊥ ≤ a
+
+section OrderBot
+
+variable [LE α] [OrderBot α] {a : α}
+
+@[simp]
+theorem bot_le : ⊥ ≤ a :=
+  OrderBot.bot_le a
+
+end OrderBot
+
+end Mathlib.Order.BoundedOrder
+
+section Mathlib.Order.TypeTags
+
+variable {α : Type _}
+
+def WithBot (α : Type _) := Option α
+
+namespace WithBot
+
+@[coe, match_pattern] def some : α → WithBot α :=
+  Option.some
+
+instance coe : Coe α (WithBot α) :=
+  ⟨some⟩
+
+instance bot : Bot (WithBot α) :=
+  ⟨none⟩
+
+@[elab_as_elim, induction_eliminator, cases_eliminator]
+def recBotCoe {C : WithBot α → Sort _} (bot : C ⊥) (coe : ∀ a : α, C a) : ∀ n : WithBot α, C n
+  | ⊥ => bot
+  | (a : α) => coe a
+
+end WithBot
+
+end Mathlib.Order.TypeTags
+
+variable {α β γ δ : Type _}
+
+namespace WithBot
+
+variable {a b : α}
+
+@[simp, norm_cast]
+theorem coe_inj : (a : WithBot α) = b ↔ a = b :=
+  Option.some_inj
+
+@[simp]
+theorem bot_ne_coe : ⊥ ≠ (a : WithBot α) :=
+  nofun
+
+section LE
+
+variable [LE α]
+
+instance (priority := 10) le : LE (WithBot α) :=
+  ⟨fun o₁ o₂ => ∀ a : α, o₁ = ↑a → ∃ b : α, o₂ = ↑b ∧ a ≤ b⟩
+
+@[simp, norm_cast]
+theorem coe_le_coe : (a : WithBot α) ≤ b ↔ a ≤ b := by
+  simp [LE.le]
+
+instance orderBot : OrderBot (WithBot α) where
+  bot_le _ := fun _ h => Option.noConfusion h
+
+theorem le_coe_iff : ∀ {x : WithBot α}, x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b
+  | (b : α) => by simp
+  | ⊥ => by simp
+
+end LE
+
+section LT
+
+variable [LT α]
+
+instance (priority := 10) lt : LT (WithBot α) :=
+  ⟨fun o₁ o₂ : WithBot α => ∃ b : α, o₂ = ↑b ∧ ∀ a : α, o₁ = ↑a → a < b⟩
+
+@[simp, norm_cast]
+theorem coe_lt_coe : (a : WithBot α) < b ↔ a < b := by
+  simp [LT.lt]
+
+end LT
+
+instance preorder [Preorder α] : Preorder (WithBot α) where
+  le := (· ≤ ·)
+  lt := (· < ·)
+  lt_iff_le_not_le := sorry
+  le_refl _ a ha := sorry
+  le_trans _ _ _ h₁ h₂ a ha := sorry
+
+end WithBot
+
+namespace WithBot
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+theorem le_of_forall_lt_iff_le [LinearOrder α] [DenselyOrdered α]
+    {x y : WithBot α} : (∀ z : α, x < z → y ≤ z) ↔ y ≤ x := by
+  refine ⟨fun h ↦ ?_, fun h z x_z ↦ sorry⟩
+  induction x with
+  | bot => sorry
+  | coe x =>
+    rw [le_coe_iff]
+    rintro y rfl
+    exact le_of_forall_le_of_dense (by exact_mod_cast h)
+
+end WithBot
diff --git a/tests/lean/run/betaSimp.lean b/tests/lean/run/betaSimp.lean
new file mode 100644
index 0000000000..bdacf4b204
--- /dev/null
+++ b/tests/lean/run/betaSimp.lean
@@ -0,0 +1,5 @@
+opaque f : Nat → Nat
+@[simp] axiom f_ax : f (no_index 0) = 1
+example : f ((fun x => x) 0) = 1 := by
+  fail_if_success simp -beta -- should fail
+  simp
diff --git a/tests/lean/run/heapSort.lean b/tests/lean/run/heapSort.lean
index d54b543c49..fc76b691a1 100644
--- a/tests/lean/run/heapSort.lean
+++ b/tests/lean/run/heapSort.lean
@@ -166,7 +166,8 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
     | none => out
     | some x =>
       have : a.popMax.size < a.size := by
-        simp; exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
+        simp +zetaDelta
+        exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
       loop a.popMax (out.push x)
     termination_by a.size
     decreasing_by assumption
@@ -175,15 +176,18 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
 attribute [simp] Array.heapSort.loop
 
 /--
-info: Array.heapSort.loop.eq_1.{u_1} {α : Type u_1} (gt : α → α → Bool) (a : BinaryHeap α gt) (out : Array α) :
-  Array.heapSort.loop gt a out =
+info: Array.heapSort.loop.eq_1 fun a b =>
+  decide
+    (a <
+      b) : ∀ (a : BinaryHeap Nat fun y x => decide (x < y)) (out : Array Nat),
+  Array.heapSort.loop (fun a b => decide (a < b)) a out =
     match e : a.max with
     | none => out
     | some x =>
       let_fun this := ⋯;
-      Array.heapSort.loop gt a.popMax (out.push x)
+      Array.heapSort.loop (fun a b => decide (a < b)) a.popMax (out.push x)
 -/
 #guard_msgs in
-#check Array.heapSort.loop.eq_1
+#check Array.heapSort.loop.eq_1 (fun (a b : Nat) => a < b)
 
 attribute [simp] BinaryHeap.heapifyDown
diff --git a/tests/lean/run/simpConfigPropagationIssue1.lean b/tests/lean/run/simpConfigPropagationIssue1.lean
new file mode 100644
index 0000000000..be3e5e84d6
--- /dev/null
+++ b/tests/lean/run/simpConfigPropagationIssue1.lean
@@ -0,0 +1,13 @@
+namespace Option
+
+variable {α : Type _}
+
+instance liftOrGet_isCommutative (f : α → α → α) [Std.Commutative f] :
+    Std.Commutative (liftOrGet f) :=
+  ⟨fun a b ↦ by cases a <;> cases b <;> simp [liftOrGet, Std.Commutative.comm]⟩
+
+instance liftOrGet_isAssociative (f : α → α → α) [Std.Associative f] :
+    Std.Associative (liftOrGet f) :=
+  ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [liftOrGet, Std.Associative.assoc]⟩
+
+end Option
diff --git a/tests/lean/run/simpConfigPropagationIssue3.lean b/tests/lean/run/simpConfigPropagationIssue3.lean
new file mode 100644
index 0000000000..cc238c06d1
--- /dev/null
+++ b/tests/lean/run/simpConfigPropagationIssue3.lean
@@ -0,0 +1,36 @@
+namespace Ordering
+
+@[simp] theorem swap_swap {o : Ordering} : o.swap.swap = o := by cases o <;> rfl
+
+@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ :=
+  ⟨fun h => by simpa using congrArg swap h, congrArg _⟩
+
+end Ordering
+
+/-- `OrientedCmp cmp` asserts that `cmp` is determined by the relation `cmp x y = .lt`. -/
+class OrientedCmp (cmp : α → α → Ordering) : Prop where
+  /-- The comparator operation is symmetric, in the sense that if `cmp x y` equals `.lt` then
+  `cmp y x = .gt` and vice versa. -/
+  symm (x y) : (cmp x y).swap = cmp y x
+
+namespace OrientedCmp
+
+theorem cmp_eq_gt [OrientedCmp cmp] : cmp x y = .gt ↔ cmp y x = .lt := by
+  rw [← Ordering.swap_inj, symm]; exact .rfl
+
+end OrientedCmp
+
+/-- `TransCmp cmp` asserts that `cmp` induces a transitive relation. -/
+class TransCmp (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+  /-- The comparator operation is transitive. -/
+  le_trans : cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt
+
+namespace TransCmp
+variable [TransCmp cmp]
+open OrientedCmp
+
+theorem ge_trans (h₁ : cmp x y ≠ .lt) (h₂ : cmp y z ≠ .lt) : cmp x z ≠ .lt := by
+  have := @TransCmp.le_trans _ cmp _ z y x
+  simp [cmp_eq_gt] at *
+  -- `simp` did not fire at `this`
+  exact this h₂ h₁
diff --git a/tests/lean/run/splitIfIssue.lean b/tests/lean/run/splitIfIssue.lean
new file mode 100644
index 0000000000..893629649e
--- /dev/null
+++ b/tests/lean/run/splitIfIssue.lean
@@ -0,0 +1,249 @@
+import Lean.Elab.Tactic.Location
+import Lean.Meta.Tactic.SplitIf
+import Lean.Elab.Tactic.Simp
+
+section Mathlib.Tactic.Core
+
+open Lean Elab Tactic
+
+namespace Lean.Elab.Tactic
+#check Parser.Tactic.allGoals
+def allGoals (tac : TacticM Unit) : TacticM Unit := do
+  let mvarIds ← getGoals
+  let mut mvarIdsNew := #[]
+  for mvarId in mvarIds do
+    unless (← mvarId.isAssigned) do
+      setGoals [mvarId]
+      try
+        tac
+        mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals)
+      catch ex =>
+        if (← read).recover then
+          logException ex
+          mvarIdsNew := mvarIdsNew.push mvarId
+        else
+          throw ex
+  setGoals mvarIdsNew.toList
+
+/-- Simulates the `<;>` tactic combinator. First runs `tac1` and then runs
+    `tac2` on all newly-generated subgoals.
+-/
+def andThenOnSubgoals (tac1 : TacticM Unit) (tac2 : TacticM Unit) : TacticM Unit :=
+  focus do tac1; allGoals tac2
+
+end Lean.Elab.Tactic
+
+end Mathlib.Tactic.Core
+
+section Mathlib.Tactic.SplitIfs
+
+namespace Mathlib.Tactic
+
+open Lean Elab.Tactic Parser.Tactic Lean.Meta
+
+/-- A position where a split may apply.
+-/
+private inductive SplitPosition
+| target
+| hyp (fvarId: FVarId)
+
+/-- Collects a list of positions pointed to by `loc` and their types.
+-/
+private def getSplitCandidates (loc : Location) : TacticM (List (SplitPosition × Expr)) :=
+match loc with
+| Location.wildcard => do
+   let candidates ← (← getLCtx).getFVarIds.mapM
+     (fun fvarId ↦ do
+       let typ ← instantiateMVars (← inferType (mkFVar fvarId))
+       return (SplitPosition.hyp fvarId, typ))
+   pure ((SplitPosition.target, ← getMainTarget) :: candidates.toList)
+| Location.targets hyps tgt => do
+   let candidates ← (← hyps.mapM getFVarId).mapM
+     (fun fvarId ↦ do
+       let typ ← instantiateMVars (← inferType (mkFVar fvarId))
+       return (SplitPosition.hyp fvarId, typ))
+   if tgt
+   then return (SplitPosition.target, ← getMainTarget) :: candidates.toList
+   else return candidates.toList
+
+/-- Return the condition and decidable instance of an `if` expression to case split. -/
+private partial def findIfToSplit? (e : Expr) : Option (Expr × Expr) :=
+  match e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars with
+  | some iteApp =>
+    let cond := iteApp.getArg! 1 5
+    let dec := iteApp.getArg! 2 5
+    -- Try to find a nested `if` in `cond`
+    findIfToSplit? cond |>.getD (cond, dec)
+  | none => none
+
+/-- Finds an if condition to split. If successful, returns the position and the condition.
+-/
+private def findIfCondAt (loc : Location) : TacticM (Option (SplitPosition × Expr)) := do
+  for (pos, e) in (← getSplitCandidates loc) do
+    if let some (cond, _) := findIfToSplit? e
+    then return some (pos, cond)
+  return none
+
+/-- `Simp.Discharge` strategy to use in `reduceIfsAt`. Delegates to
+`SplitIf.discharge?`, and additionally supports discharging `True`, to
+better match the behavior of mathlib3's `split_ifs`.
+-/
+private def discharge? (e : Expr) : SimpM (Option Expr) := do
+  let e ← instantiateMVars e
+  if let some e1 ← (← SplitIf.mkDischarge? false) e
+    then return some e1
+  if e.isConstOf `True
+    then return some (mkConst `True.intro)
+  return none
+
+/-- Simplifies if-then-else expressions after cases have been split out.
+-/
+private def reduceIfsAt (loc : Location) : TacticM Unit := do
+  let ctx ← SplitIf.getSimpContext
+  let ctx ← ctx.setConfig { ctx.config with failIfUnchanged := false }
+  let _ ← simpLocation ctx (← ({} : Simp.SimprocsArray).add `reduceCtorEq false) discharge? loc
+  pure ()
+
+/-- Splits a single if-then-else expression and then reduces the resulting goals.
+Has a similar effect as `SplitIf.splitIfTarget?` or `SplitIf.splitIfLocalDecl?` from
+core Lean 4. We opt not to use those library functions so that we can better mimic
+the behavior of mathlib3's `split_ifs`.
+-/
+private def splitIf1 (cond : Expr) (hName : Name) (loc : Location) : TacticM Unit := do
+  let splitCases :=
+    evalTactic (← `(tactic| by_cases $(mkIdent hName) : $(← Elab.Term.exprToSyntax cond)))
+  andThenOnSubgoals splitCases (reduceIfsAt loc)
+
+/-- Pops off the front of the list of names, or generates a fresh name if the
+list is empty.
+-/
+private def getNextName (hNames: IO.Ref (List (TSyntax `Lean.binderIdent))) : MetaM Name := do
+  match ← hNames.get with
+  | [] => mkFreshUserName `h
+  | n::ns => do hNames.set ns
+                if let `(binderIdent| $x:ident) := n
+                then pure x.getId
+                else pure `_
+
+/-- Returns `true` if the condition or its negation already appears as a hypothesis.
+-/
+private def valueKnown (cond : Expr) : TacticM Bool := do
+  let not_cond := mkApp (mkConst `Not) cond
+  for h in ← getLocalHyps do
+    let ty ← instantiateMVars (← inferType h)
+    if cond == ty then return true
+    if not_cond == ty then return true
+  return false
+
+/-- Main loop of split_ifs. Pulls names for new hypotheses from `hNames`.
+Stops if it encounters a condition in the passed-in `List Expr`.
+-/
+private partial def splitIfsCore
+    (loc : Location)
+    (hNames : IO.Ref (List (TSyntax `Lean.binderIdent))) :
+    List Expr → TacticM Unit := fun done ↦ withMainContext do
+  let some (_,cond) ← findIfCondAt loc
+      | Meta.throwTacticEx `split_ifs (← getMainGoal) "no if-then-else conditions to split"
+
+  -- If `cond` is `¬p` then use `p` instead.
+  let cond := if cond.isAppOf `Not then cond.getAppArgs[0]! else cond
+
+  if done.contains cond then return ()
+  let no_split ← valueKnown cond
+  if no_split then
+    andThenOnSubgoals (reduceIfsAt loc) (splitIfsCore loc hNames (cond::done) <|> pure ())
+  else do
+    let hName ← getNextName hNames
+    andThenOnSubgoals (splitIf1 cond hName loc) ((splitIfsCore loc hNames (cond::done)) <|>
+      pure ())
+
+/-- Splits all if-then-else-expressions into multiple goals.
+Given a goal of the form `g (if p then x else y)`, `split_ifs` will produce
+two goals: `p ⊢ g x` and `¬p ⊢ g y`.
+If there are multiple ite-expressions, then `split_ifs` will split them all,
+starting with a top-most one whose condition does not contain another
+ite-expression.
+`split_ifs at *` splits all ite-expressions in all hypotheses as well as the goal.
+`split_ifs with h₁ h₂ h₃` overrides the default names for the hypotheses.
+-/
+syntax (name := splitIfs) "split_ifs" (location)? (" with" (ppSpace colGt binderIdent)+)? : tactic
+
+elab_rules : tactic
+| `(tactic| split_ifs $[$loc:location]? $[with $withArg*]?) =>
+  let loc := match loc with
+  | none => Location.targets #[] true
+  | some loc => expandLocation loc
+  let names := match withArg with
+  | none => []
+  | some args => args.toList
+  withMainContext do
+    let names ← IO.mkRef names
+    splitIfsCore loc names []
+    for name in ← names.get do
+      logWarningAt name m!"unused name: {name}"
+
+end Mathlib.Tactic
+
+end Mathlib.Tactic.SplitIfs
+
+section Mathlib.Order.Defs
+
+class Preorder (α : Type _) extends LE α, LT α where
+
+class PartialOrder (α : Type _) extends Preorder α where
+
+class LinearOrder (α : Type _) extends PartialOrder α, Min α, Max α, Ord α where
+  /-- In a linearly ordered type, we assume the order relations are all decidable. -/
+  decidableLE : DecidableRel (· ≤ · : α → α → Prop)
+  /-- In a linearly ordered type, we assume the order relations are all decidable. -/
+  decidableEq : DecidableEq α
+  /-- In a linearly ordered type, we assume the order relations are all decidable. -/
+  decidableLT : DecidableRel (· < · : α → α → Prop)
+  min := fun a b => if a ≤ b then a else b
+  max := fun a b => if a ≤ b then b else a
+
+variable [LinearOrder α] {a b c : α}
+
+instance (priority := 900) (a b : α) : Decidable (a < b) := LinearOrder.decidableLT a b
+instance (priority := 900) (a b : α) : Decidable (a ≤ b) := LinearOrder.decidableLE a b
+instance (priority := 900) (a b : α) : Decidable (a = b) := LinearOrder.decidableEq a b
+
+end Mathlib.Order.Defs
+
+section Mathlib.Order.Lattice
+
+universe u v w
+
+variable {α : Type u}
+
+class SemilatticeSup (α : Type u) extends PartialOrder α where
+  sup : α → α → α
+
+class Lattice (α : Type u) extends SemilatticeSup α
+
+end Mathlib.Order.Lattice
+
+open Lean Meta Elab Tactic in
+/-- `guard_goal_nums n` succeeds if there are exactly `n` goals and fails otherwise. -/
+elab (name := guardGoalNums) "guard_goal_nums " n:num : tactic => do
+  let numGoals := (← getGoals).length
+  guard (numGoals = n.getNat) <|>
+    throwError "expected {n.getNat} goals but found {numGoals}"
+
+example (a m tl : α) (f : α → β) [LinearOrder β] :
+    (if f (if f a < f m then m else a) < f tl then some tl else some (if f a < f m then m else a)) =
+      if f a < f (if f m < f tl then tl else m) then some (if f m < f tl then tl else m) else some a := by
+  split_ifs
+  guard_goal_nums 7
+  all_goals sorry
+
+instance LinearOrder.toLattice {α : Type u} [o : LinearOrder α] : Lattice α :=
+  let __spread := o
+  { __spread with sup := max }
+
+example (a m tl : α) (f : α → β) [LinearOrder β] :
+    (if f (if f a < f m then m else a) < f tl then some tl else some (if f a < f m then m else a)) =
+      if f a < f (if f m < f tl then tl else m) then some (if f m < f tl then tl else m) else some a := by
+  split_ifs
+  guard_goal_nums 7
+  all_goals sorry
diff --git a/tests/lean/run/zetaDeltaSet.lean b/tests/lean/run/zetaDeltaSet.lean
new file mode 100644
index 0000000000..ef3d96b714
--- /dev/null
+++ b/tests/lean/run/zetaDeltaSet.lean
@@ -0,0 +1,13 @@
+opaque f : Nat → Nat
+
+example (a : Nat) : True := by
+  let x := a
+  have h1 : f x = 2 := sorry
+  suffices f a = 2 by sorry
+  simp only [h1, x]
+
+example : True := by
+  let x := 37
+  have : x = 2 := sorry
+  suffices 37 = 2 by sorry
+  simp only [this, x]
diff --git a/tests/lean/run/zetaDeltaTryThisIssue.lean b/tests/lean/run/zetaDeltaTryThisIssue.lean
new file mode 100644
index 0000000000..30276eadfb
--- /dev/null
+++ b/tests/lean/run/zetaDeltaTryThisIssue.lean
@@ -0,0 +1,27 @@
+opaque f : Nat → Nat
+
+/--
+info: Try this: simp only [h1, x]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (a : Nat) : True := by
+  let x := a
+  have h1 : f x = 2 := sorry
+  suffices f a = 2 by sorry
+  let w := a + a
+  simp? only [h1, w, x]
+
+/--
+info: Try this: simp only [this, x]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : True := by
+  let x := 37
+  let y := 34
+  have : x = 2 := sorry
+  suffices 37 = 2 by sorry
+  simp? only [this, x, y]