diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean
index c19612b500..0fb37efc23 100644
--- a/src/Init/MetaTypes.lean
+++ b/src/Init/MetaTypes.lean
@@ -161,7 +161,7 @@ structure Config where
   -/
   contextual        : Bool := false
   /--
-  When true (default: `true`) then the simplifier caches the result of simplifying each subexpression, if possible.
+  When true (default: `true`) then the simplifier caches the result of simplifying each sub-expression, if possible.
   -/
   memoize           : Bool := true
   /--
@@ -252,14 +252,14 @@ structure Config where
   -/
   implicitDefEqProofs : Bool := true
   /--
-  When `true` (default : `true`), then `simp` will remove unused `let` and `have` expressions:
+  When `true` (default : `true`), then `simp` removes unused `let` and `have` expressions:
   `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
   This option takes precedence over `zeta` and `zetaHave`.
   -/
   zetaUnused : Bool := true
   /--
-  When `true` (default : `true`), then simps will catch runtime exceptions and
-  convert them into `simp` exceptions.
+  When `true` (default : `true`), then `simp` catches runtime exceptions and
+  converts them into `simp` exceptions.
   -/
   catchRuntime : Bool := true
   /--
@@ -273,6 +273,14 @@ structure Config where
   if they are non-dependent. This only applies when `zeta := false`.
   -/
   letToHave : Bool := true
+  /--
+  When `true` (default : `true`), `simp` tries to realize constant `f.congr_simp`
+  when constructing an auxiliary congruence proof for `f`.
+  This option exists because the termination prover uses `simp` and `withoutModifyingEnv`
+  while constructing the termination proof. Thus, any constant realized by `simp`
+  is deleted.
+  -/
+  congrConsts : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`
diff --git a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean
index 0f6bec5046..22115a73a1 100644
--- a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean
@@ -73,7 +73,9 @@ private def getSimpContext : MetaM Simp.Context := do
   Simp.mkContext
     (simpTheorems  := #[simpTheorems])
     (congrTheorems := {})
-    (config        := { Simp.neutralConfig with dsimp := true })
+    -- Remark: we use `congrConsts` because this module uses `withoutModifyingEnv`
+    -- which would erase any congruence lemmas realized in the `withoutModifyingEnv` block.
+    (config        := { Simp.neutralConfig with dsimp := true, congrConsts := false })
 
 def isWfParam? (e : Expr) : Option Expr :=
   if e.isAppOfArity ``wfParam 2 then
diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index d2f945e073..b68e507fc9 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -364,6 +364,8 @@ def isHCongrReservedNameSuffix (s : String) : Bool :=
 
 def congrSimpSuffix := "congr_simp"
 
+builtin_initialize registerTraceClass `congr.thm
+
 builtin_initialize congrKindsExt : MapDeclarationExtension (Array CongrArgKind) ← mkMapDeclarationExtension
 
 builtin_initialize registerReservedNamePredicate fun env n =>
@@ -386,6 +388,7 @@ builtin_initialize
             name, type := congrThm.type, value := congrThm.proof
             levelParams := info.levelParams
           }
+          trace[congr.thm] "declared `{name}`"
           modifyEnv fun env => congrKindsExt.insert env name congrThm.argKinds
         return true
       catch _ => return false
@@ -401,6 +404,7 @@ builtin_initialize
             name, type := congrThm.type, value := congrThm.proof
             levelParams := cinfo.levelParams
           }
+          trace[congr.thm] "declared `{name}`"
           modifyEnv fun env => congrKindsExt.insert env name congrThm.argKinds
         return true
       catch _ => return false
@@ -430,8 +434,8 @@ Similar to `mkCongrSimp?`, but uses reserved names to ensure we don't keep creat
 same congruence theorem over and over again.
 -/
 def mkCongrSimpForConst? (declName : Name) (levels : List Level) : MetaM (Option CongrTheorem) := do
+  let thmName := Name.str declName congrSimpSuffix
   try
-    let thmName := Name.str declName congrSimpSuffix
     unless (← getEnv).contains thmName do
       let _ ← executeReservedNameAction thmName
     let proof := mkConst thmName levels
@@ -439,7 +443,8 @@ def mkCongrSimpForConst? (declName : Name) (levels : List Level) : MetaM (Option
     let some argKinds := congrKindsExt.find? (← getEnv) thmName
       | unreachable!
     return some { proof, type, argKinds }
-  catch _ =>
+  catch ex =>
+    trace[congr.thm] "failed to generate `{thmName}` {ex.toMessageData}"
     return none
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index fe3568c858..19efe01407 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -643,21 +643,36 @@ Retrieve auto-generated congruence lemma for `f`.
 Remark: If all argument kinds are `fixed` or `eq`, it returns `none` because
 using simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof.
 -/
-def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do
+def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do profileitM Exception "congr simp thm" (← getOptions) do
   if f.isConst then if (← isMatcher f.constName!) then
     -- We always use simple congruence theorems for auxiliary match applications
     return none
-  let info ← getFunInfo f
-  let kinds ← getCongrSimpKinds f info
-  if kinds.all fun k => match k with | CongrArgKind.fixed => true | CongrArgKind.eq => true | _ => false then
-    /- See remark above. -/
-    return none
   match (← get).congrCache[f]? with
   | some thm? => return thm?
   | none =>
-    let thm? ← mkCongrSimpCore? f info kinds
+    let thm? ← go?
     modify fun s => { s with congrCache := s.congrCache.insert f thm? }
     return thm?
+where
+  go? : SimpM (Option CongrTheorem) := do
+    let info ← getFunInfo f
+    let argKinds ← getCongrSimpKinds f info
+    if argKinds.all fun k => match k with | .fixed | .eq => true | _ => false then
+      /- See remark above. -/
+      return none
+    else if !(← getConfig).congrConsts then
+      mkCongrSimpCore? f info argKinds
+    else if let .const declName us := f then
+      let some thm ← mkCongrSimpForConst? declName us | mkCongrSimpCore? f info argKinds
+      if thm.argKinds == argKinds then
+        trace[congr.thm] "used global `{thm.proof.getAppFn}`"
+        return some thm
+      else
+        trace[congr.thm] "argKind mismatch while generating congr_simp theorem for `{declName}`"
+        mkCongrSimpCore? f info argKinds
+    else
+      mkCongrSimpCore? f info argKinds
+
 
 /--
 Try to use automatically generated congruence theorems. See `mkCongrSimp?`.