diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index 2fefbb0f3b..307b47a131 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Util.HasConstCache
 import Lean.Meta.Match.Match
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
@@ -97,7 +98,11 @@ def refinedArgType (matcherApp : MatcherApp) (arg : Expr) : MetaM Bool := do
         return false
 
 private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) (below : Expr) (e : Expr) : M Expr :=
-  let rec loop (below : Expr) (e : Expr) : M Expr := do
+  let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnName) M Bool :=
+    modifyGet (·.contains e)
+  let rec loop (below : Expr) (e : Expr) : StateRefT (HasConstCache recFnName) M Expr := do
+    if !(← containsRecFn e) then
+      return e
     match e with
     | Expr.lam n d b c =>
       withLocalDecl n c.binderInfo (← loop below d) fun x => do
@@ -115,7 +120,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
         return mkMData d (← loop below b)
     | Expr.proj n i e _  => return mkProj n i (← loop below e)
     | Expr.app _ _ _ =>
-      let processApp (e : Expr) : M Expr :=
+      let processApp (e : Expr) : StateRefT (HasConstCache recFnName) M Expr :=
         e.withApp fun f args => do
           if f.isConstOf recFnName then
             let numFixed  := recArgInfo.fixedParams.size
@@ -175,7 +180,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
             pure { matcherApp with alts := altsNew }.toExpr
       | none => processApp e
     | e => ensureNoRecFn recFnName e
-  loop below e
+  loop below e |>.run' {}
 
 def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
   trace[Elab.definition.structural] "mkBRecOn: {value}"
diff --git a/src/Lean/Elab/PreDefinition/Structural/Basic.lean b/src/Lean/Elab/PreDefinition/Structural/Basic.lean
index 14bbb60b73..ff7f265b0e 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Basic.lean
@@ -30,7 +30,7 @@ structure State where
      As a side-effect, this creates matchers. Here we capture all these side-effects, because
      the construction rolls back any changes done to the environment and the side-effects
      need to be replayed. -/
-  addMatchers : Array $ MetaM Unit := #[]
+  addMatchers : Array (MetaM Unit) := #[]
 
 abbrev M := StateRefT State MetaM
 
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 1881c7750b..5ef97696f5 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Util.HasConstCache
 import Lean.Meta.Match.Match
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Cleanup
@@ -30,9 +31,9 @@ private def mkDecreasingProof (decreasingProp : Expr) (decrTactic? : Option Synt
   instantiateMVars mvar
 
 private partial def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) (F : Expr) (e : Expr) : TermElabM Expr :=
-  loop F e
+  loop F e |>.run' {}
 where
-  processRec (F : Expr) (e : Expr) : TermElabM Expr := do
+  processRec (F : Expr) (e : Expr) : StateRefT (HasConstCache recFnName) TermElabM Expr := do
     if e.getAppNumArgs < fixedPrefixSize + 1 then
       loop F (← etaExpand e)
     else
@@ -42,13 +43,18 @@ where
       let r := mkApp r (← mkDecreasingProof decreasingProp decrTactic?)
       return mkAppN r (← args[fixedPrefixSize+1:].toArray.mapM (loop F))
 
-  processApp (F : Expr) (e : Expr) : TermElabM Expr := do
+  processApp (F : Expr) (e : Expr) : StateRefT (HasConstCache recFnName) TermElabM Expr := do
     if e.isAppOf recFnName then
       processRec F e
     else
       e.withApp fun f args => return mkAppN (← loop F f) (← args.mapM (loop F))
 
-  loop (F : Expr) (e : Expr) : TermElabM Expr := do
+  containsRecFn (e : Expr) : StateRefT (HasConstCache recFnName) TermElabM Bool := do
+    modifyGet (·.contains e)
+
+  loop (F : Expr) (e : Expr) : StateRefT (HasConstCache recFnName) TermElabM Expr := do
+    if !(← containsRecFn e) then
+      return e
     match e with
     | Expr.lam n d b c =>
       withLocalDecl n c.binderInfo (← loop F d) fun x => do