From 8655f7706feb180d419aa362e412be01b345c8c1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 7 Oct 2025 14:53:09 +0200
Subject: [PATCH] refactor: structural recursion: prove `.eq_def` directly
 (#10606)

This PR changes how Lean proves the equational theorems for structural
recursion. The core idea is to let-bind the `f` argument to `brecOn` and
rewriting `.brecOn` with an unfolding theorem. This means no extra case
split for the `.rec` in `.brecOn` is needed, and `simp` doesn't change
the `f` argument which can break the definitional equality with the
defined function. With this, we can prove the unfolding theorem first,
and derive the equational theorems from that, like for all other ways of
defining recursive functions.

Backs out the changes from #10415, the old strategy works well with the
new goals.

Fixes #5667
Fixes #10431
Fixes #10195
Fixes #2962
---
 src/Init/Data/Dyadic/Basic.lean               |   1 +
 src/Lean/Elab/PreDefinition/Eqns.lean         |  11 +-
 .../PreDefinition/PartialFixpoint/Eqns.lean   |   2 +-
 .../Elab/PreDefinition/Structural/Eqns.lean   | 168 +++++++++---------
 src/Lean/Meta/Constructions/BRecOn.lean       | 116 ++++++++----
 src/Lean/Meta/Tactic/Refl.lean                |  12 +-
 stage0/src/stdlib_flags.h                     |   2 +
 tests/lean/run/2961.lean                      |  99 -----------
 tests/lean/run/5667.lean                      | 121 +++++++------
 tests/lean/run/eqValue.lean                   |   1 +
 tests/lean/run/issue10195.lean                |  19 --
 tests/lean/run/issue10424.lean                |  52 ------
 tests/lean/run/issue10431.lean                |  78 ++++++++
 tests/lean/run/issue2237.lean                 |  35 ++++
 tests/lean/run/issue2962.lean                 | 105 +++++++++++
 tests/lean/run/issue6592.lean                 | 136 ++++++++++++++
 tests/lean/run/issue9846.lean                 |  21 +++
 tests/lean/run/partial_fixpoint.lean          |   2 +-
 tests/lean/run/structuralEqn6.lean            |  87 +++++++++
 tests/lean/run/structuralEqns2.lean           |   2 +-
 tests/lean/run/structuralEqns4.lean           |  44 +++++
 tests/lean/run/structuralEqns5.lean           |  76 ++++++++
 22 files changed, 834 insertions(+), 356 deletions(-)
 delete mode 100644 tests/lean/run/2961.lean
 create mode 100644 tests/lean/run/issue10431.lean
 create mode 100644 tests/lean/run/issue2237.lean
 create mode 100644 tests/lean/run/issue2962.lean
 create mode 100644 tests/lean/run/issue6592.lean
 create mode 100644 tests/lean/run/issue9846.lean
 create mode 100644 tests/lean/run/structuralEqn6.lean
 create mode 100644 tests/lean/run/structuralEqns4.lean
 create mode 100644 tests/lean/run/structuralEqns5.lean

diff --git a/src/Init/Data/Dyadic/Basic.lean b/src/Init/Data/Dyadic/Basic.lean
index 3cd06e327d..2c11a943e8 100644
--- a/src/Init/Data/Dyadic/Basic.lean
+++ b/src/Init/Data/Dyadic/Basic.lean
@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Rat.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
 import Init.Data.Int.DivMod.Lemmas
+import Init.Hints
 
 /-!
 # The dyadic rationals
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 85a4464500..409f00f16f 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -101,10 +101,11 @@ partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Opti
                                        target declNames badCases then
       try
         Meta.Split.splitMatch mvarId e
-      catch _ =>
+      catch ex =>
+        trace[Elab.definition.eqns] "cannot split {e}\n{ex.toMessageData}"
         go (badCases.insert e)
     else
-      trace[Meta.Tactic.split] "did not find term to split\n{MessageData.ofGoal mvarId}"
+      trace[Elab.definition.eqns] "did not find term to split\n{MessageData.ofGoal mvarId}"
       return none
   go {}
 
@@ -288,7 +289,7 @@ public def deltaLHS (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   let some lhs ← delta? lhs | throwTacticEx `deltaLHS mvarId "failed to delta reduce lhs"
   mvarId.replaceTargetDefEq (← mkEq lhs rhs)
 
-def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := mvarId.withContext do
+public def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := mvarId.withContext do
   let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | return none
   let some rhs ← delta? rhs.consumeMData (· == declName) | return none
@@ -347,7 +348,7 @@ private def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvar
     deltaLHS mvarId
 
 private partial def mkEqnProof (declName : Name) (type : Expr) (tryRefl : Bool) : MetaM Expr := do
-  trace[Elab.definition.eqns] "proving: {type}"
+  withTraceNode `Elab.definition.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do
   withNewMCtxDepth do
     let main ← mkFreshExprSyntheticOpaqueMVar type
     let (_, mvarId) ← main.mvarId!.intros
@@ -371,7 +372,7 @@ private partial def mkEqnProof (declName : Name) (type : Expr) (tryRefl : Bool)
   recursion and structural recursion can and should use this too.
   -/
   go (mvarId : MVarId) : MetaM Unit := do
-    trace[Elab.definition.eqns] "step\n{MessageData.ofGoal mvarId}"
+    withTraceNode `Elab.definition.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do
     if (← tryURefl mvarId) then
       return ()
     else if (← tryContradiction mvarId) then
diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
index 054903b9a3..dc0d3e19e6 100644
--- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
@@ -117,7 +117,7 @@ def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then
-    mkEqns declName info.declNames
+    mkEqns declName info.declNames (tryRefl := false)
   else
     return none
 
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index e9120628f8..d46cec496f 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -16,6 +16,7 @@ import Lean.Meta.Tactic.Apply
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Meta.Match.MatchEqs
+import Lean.Meta.Tactic.Rewrite
 
 namespace Lean.Elab
 open Meta
@@ -29,33 +30,95 @@ public structure EqnInfo extends EqnInfoCore where
   fixedParamPerms : FixedParamPerms
   deriving Inhabited
 
-private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
+/--
+Searches in the lhs of goal for a `.brecOn` application, possibly with extra arguments
+and under `PProd` projections. Returns the `.brecOn` application and the context
+`(fun x => (x).1.2.3 extraArgs = rhs)`.
+-/
+partial def findBRecOnLHS (goal : Expr) : MetaM (Expr × Expr) := do
+  let some (_, lhs, rhs) := goal.eq? | throwError "goal not an equality{indentExpr goal}"
+  go lhs fun brecOnApp x c =>
+    return (brecOnApp, ← mkLambdaFVars #[x] (← mkEq c rhs))
+where
+  go {α} (e : Expr) (k : Expr → Expr → Expr → MetaM α) : MetaM α := e.withApp fun f xs => do
+    if let .proj t n e := f then
+      return ← go e fun brecOnApp x c => k brecOnApp x (mkAppN (mkProj t n c) xs)
+    if let .const name _ := f then
+      if isBRecOnRecursor (← getEnv) name then
+        let arity ← forallTelescope (← inferType f) fun xs _ => return xs.size
+        if arity ≤ xs.size then
+          let brecOnApp := mkAppN f xs[:arity]
+          let extraArgs := xs[arity:]
+          return ← withLocalDeclD `x (← inferType brecOnApp) fun x =>
+            k brecOnApp x (mkAppN x extraArgs)
+    throwError "could not find `.brecOn` application in{indentExpr e}"
+
+/--
+Creates the proof of the unfolding theorem for `declName` with type `type`. It
+
+1. unfolds the function on the left to expose the `.brecOn` application
+2. rewrites that using the `.brecOn.eq` theorem, unrolling it once
+3. let-binds the last argument, which should be the `.brecOn.go` call of type `.below …`.
+   This way subsequent steps (which may involve `simp`) do not touch it and do
+   not break the definitional equality with the recursive calls on the RHS.
+4. repeatedly splits `match` statements (because on the left we have `match` statements with extra
+   `.below` arguments, and on the right we have the original `match` statements) until the goal
+   is solved using `rfl` or `contradiction`.
+-/
+partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
   withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do
+    prependError m!"failed to generate equational theorem for `{.ofConstName declName}`" do
     withNewMCtxDepth do
       let main ← mkFreshExprSyntheticOpaqueMVar type
       let (_, mvarId) ← main.mvarId!.intros
       unless (← tryURefl mvarId) do -- catch easy cases
-        go1 mvarId
+        goUnfold (← deltaLHS mvarId)
       instantiateMVars main
 where
-  /--
-  Step 1: Split the function body into its cases, but keeping the LHS intact, because the
-  `.below`-added `match` statements and the `.rec` can quickly confuse `split`.
-  -/
-  go1 (mvarId : MVarId) : MetaM Unit := do
-    withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} go1:\n{MessageData.ofGoal mvarId}") do
+  goUnfold (mvarId : MVarId) : MetaM Unit := do
+    withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} goUnfold:\n{MessageData.ofGoal mvarId}") do
+    let mvarId' ← mvarId.withContext do
+      -- This should now be headed by `.brecOn`
+      let goal ← mvarId.getType
+      let (brecOnApp, context) ← findBRecOnLHS goal
+      let brecOnName := brecOnApp.getAppFn.constName!
+      let us := brecOnApp.getAppFn.constLevels!
+      let brecOnThmName := brecOnName.str "eq"
+      let brecOnAppArgs := brecOnApp.getAppArgs
+      unless (← hasConst brecOnThmName) do
+        throwError "no theorem `{brecOnThmName}`\n{MessageData.ofGoal mvarId}"
+      -- We don't just `← inferType eqThmApp` as that beta-reduces more than we want
+      let eqThmType ← inferType (mkConst brecOnThmName us)
+      let eqThmType ← instantiateForall eqThmType brecOnAppArgs
+      let some (_, _, rwRhs) := eqThmType.eq? | throwError "theorem `{brecOnThmName}` is not an equality\n{MessageData.ofGoal mvarId}"
+      let recArg := rwRhs.getAppArgs.back!
+      trace[Elab.definition.structural.eqns] "abstracting{inlineExpr recArg} from{indentExpr rwRhs}"
+      let mvarId2 ← mvarId.define `r (← inferType recArg) recArg
+      let (r, mvarId3) ← mvarId2.intro1P
+      let mvarId4 ← mvarId3.withContext do
+        let goal' := mkApp rwRhs.appFn! (mkFVar r)
+        let thm ← mkCongrArg context (mkAppN (mkConst brecOnThmName us) brecOnAppArgs)
+        mvarId3.replaceTargetEq (mkApp context goal') thm
+      pure mvarId4
+    go mvarId'
+
+  go (mvarId : MVarId) : MetaM Unit := do
+    withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do
       if (← tryURefl mvarId) then
         trace[Elab.definition.structural.eqns] "tryURefl succeeded"
         return ()
       else if (← tryContradiction mvarId) then
         trace[Elab.definition.structural.eqns] "tryContadiction succeeded"
         return ()
+      else if let some mvarId ← whnfReducibleLHS? mvarId then
+        trace[Elab.definition.structural.eqns] "whnfReducibleLHS succeeded"
+        go mvarId
       else if let some mvarId ← simpMatch? mvarId then
         trace[Elab.definition.structural.eqns] "simpMatch? succeeded"
-        go1 mvarId
+        go mvarId
       else if let some mvarId ← simpIf? mvarId (useNewSemantics := true) then
         trace[Elab.definition.structural.eqns] "simpIf? succeeded"
-        go1 mvarId
+        go mvarId
       else
         let ctx ← Simp.mkContext
         match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
@@ -63,80 +126,19 @@ where
           trace[Elab.definition.structural.eqns] "simpTargetStar closed the goal"
         | TacticResultCNM.modified mvarId =>
           trace[Elab.definition.structural.eqns] "simpTargetStar modified the goal"
-          go1 mvarId
+          go mvarId
         | TacticResultCNM.noChange =>
-          if let some mvarIds ← casesOnStuckLHS? mvarId then
+          if let some mvarId ← deltaRHS? mvarId declName then
+            trace[Elab.definition.structural.eqns] "deltaRHS? succeeded"
+            go mvarId
+          else if let some mvarIds ← casesOnStuckLHS? mvarId then
             trace[Elab.definition.structural.eqns] "casesOnStuckLHS? succeeded"
-            mvarIds.forM go1
+            mvarIds.forM go
           else if let some mvarIds ← splitTarget? mvarId (useNewSemantics := true) then
             trace[Elab.definition.structural.eqns] "splitTarget? succeeded"
-            mvarIds.forM go1
+            mvarIds.forM go
           else
-            go2 (← deltaLHS mvarId)
-  /-- Step 2: Unfold the lhs to expose the recursor. -/
-  go2 (mvarId : MVarId) : MetaM Unit := do
-    withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} go2:\n{MessageData.ofGoal mvarId}") do
-    if let some mvarId ← whnfReducibleLHS? mvarId then
-      go2 mvarId
-    else
-      go3 mvarId
-  /-- Step 3: Simplify the match and if statements on the left hand side, until we have rfl. -/
-  go3 (mvarId : MVarId) : MetaM Unit := do
-      withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} go3:\n{MessageData.ofGoal mvarId}") do
-      if (← tryURefl mvarId) then
-        trace[Elab.definition.structural.eqns] "tryURefl succeeded"
-        return ()
-      else if (← tryContradiction mvarId) then
-        trace[Elab.definition.structural.eqns] "tryContadiction succeeded"
-        return ()
-      else if let some mvarId ← simpMatch? mvarId then
-        trace[Elab.definition.structural.eqns] "simpMatch? succeeded"
-        go3 mvarId
-      else if let some mvarId ← simpIf? mvarId (useNewSemantics := true) then
-        trace[Elab.definition.structural.eqns] "simpIf? succeeded"
-        go3 mvarId
-      else
-        let ctx ← Simp.mkContext
-        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
-        | TacticResultCNM.closed =>
-          trace[Elab.definition.structural.eqns] "simpTargetStar closed the goal"
-        | TacticResultCNM.modified mvarId =>
-          trace[Elab.definition.structural.eqns] "simpTargetStar modified the goal"
-          go3 mvarId
-        | TacticResultCNM.noChange =>
-          if let some mvarIds ← casesOnStuckLHS? mvarId then
-            trace[Elab.definition.structural.eqns] "casesOnStuckLHS? succeeded"
-            mvarIds.forM go3
-          else
-            throwError "failed to generate equational theorem for `{.ofConstName declName}`\n{MessageData.ofGoal mvarId}"
-
-def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
-  withOptions (tactic.hygienic.set · false) do
-  let eqnTypes ← withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
-    let us := info.levelParams.map mkLevelParam
-    let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
-    let goal ← mkFreshExprSyntheticOpaqueMVar target
-    mkEqnTypes info.declNames goal.mvarId!
-  let mut thmNames := #[]
-  for h : i in *...eqnTypes.size do
-    let type := eqnTypes[i]
-    trace[Elab.definition.structural.eqns] "eqnType {i+1}: {type}"
-    let name := mkEqLikeNameFor (← getEnv) info.declName s!"{eqnThmSuffixBasePrefix}{i+1}"
-    thmNames := thmNames.push name
-    -- determinism: `type` should be independent of the environment changes since `baseName` was
-    -- added
-    realizeConst info.declNames[0]! name (doRealize name type)
-  return thmNames
-where
-  doRealize name type := withOptions (tactic.hygienic.set · false) do
-    let value ← withoutExporting do mkProof info.declName type
-    let (type, value) ← removeUnusedEqnHypotheses type value
-    let type ← letToHave type
-    addDecl <| Declaration.thmDecl {
-      name, type, value
-      levelParams := info.levelParams
-    }
-    inferDefEqAttr name
+            throwError "no progress at goal\n{MessageData.ofGoal mvarId}"
 
 public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
   mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
@@ -151,7 +153,7 @@ public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (r
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then
-    mkEqns info
+    mkEqns declName info.declNames
   else
     return none
 
@@ -165,11 +167,10 @@ where
     lambdaTelescope info.value fun xs body => do
       let us := info.levelParams.map mkLevelParam
       let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
-      let goal ← mkFreshExprSyntheticOpaqueMVar type
-      mkUnfoldProof declName goal.mvarId!
+      let value ← withoutExporting <| mkProof declName type
       let type ← mkForallFVars xs type
       let type ← letToHave type
-      let value ← mkLambdaFVars xs (← instantiateMVars goal)
+      let value ← mkLambdaFVars xs value
       addDecl <| Declaration.thmDecl {
         name, type, value
         levelParams := info.levelParams
@@ -187,6 +188,7 @@ def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
   let some info := eqnInfoExt.find? (← getEnv) declName | return none
   return some info.recArgPos
 
+
 builtin_initialize
   registerGetEqnsFn getEqnsFor?
   registerGetUnfoldEqnFn getUnfoldFor?
diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean
index 83b35c6478..6f02745ae1 100644
--- a/src/Lean/Meta/Constructions/BRecOn.lean
+++ b/src/Lean/Meta/Constructions/BRecOn.lean
@@ -6,15 +6,16 @@ Authors: Leonardo de Moura, Joachim Breitner
 module
 
 prelude
-public import Init.Data.Iterators.Consumers.Stream
-public import Init.Data.Range.Polymorphic.Stream
-public import Lean.Meta.InferType
-public import Lean.AuxRecursor
-public import Lean.AddDecl
-public import Lean.Meta.CompletionName
-public import Lean.Meta.PProdN
-
-public section
+public import Lean.Meta.Basic
+import Init.Data.Range.Polymorphic.Stream
+import Lean.Meta.InferType
+import Lean.AuxRecursor
+import Lean.AddDecl
+import Lean.Meta.CompletionName
+import Lean.Meta.PProdN
+import Lean.Meta.AppBuilder
+import Lean.Meta.Tactic.Cases
+import Lean.Meta.Tactic.Refl
 
 namespace Lean
 open Meta
@@ -57,10 +58,8 @@ Constructs the `.below` definition for a inductive predicate.
 
 For example for the `List` type, it constructs,
 ```
-@[reducible] protected def List.below.{u_1, u} : {α : Type u} →
-  {motive : List α → Sort u_1} → List α → Sort (max 1 u_1) :=
-fun {α} {motive} t =>
-  List.rec PUnit (fun head tail tail_ih => PProd (PProd (motive tail) tail_ih) PUnit) t
+@[reducible] protected def List.below.{u} : {a : Type} → {motive : List a → Sort u} → List a → Sort (max 1 u) :=
+fun {a} {motive} t => List.rec PUnit (fun a_1 a a_ih => motive a ×' a_ih) t
 ```
 -/
 private def mkBelowFromRec (recName : Name) (nParams : Nat)
@@ -117,7 +116,7 @@ private def mkBelowFromRec (recName : Name) (nParams : Nat)
   modifyEnv fun env => markAuxRecursor env decl.name
   modifyEnv fun env => addProtected env decl.name
 
-def mkBelow (indName : Name) : MetaM Unit := do
+public def mkBelow (indName : Name) : MetaM Unit := do
   withTraceNode `Meta.mkBelow (fun _ => return m!"{indName}") do
   let .inductInfo indVal ← getConstInfo indName | return
   unless indVal.isRec do return
@@ -181,25 +180,31 @@ Constructs the `.brecOn` definition for a inductive predicate.
 
 For example for the `List` type, it constructs,
 ```
-@[reducible] protected def List.brecOn.{u_1, u} : {α : Type u} → {motive : List α → Sort u_1} →
-  (t : List α) → ((t : List α) → List.below t → motive t) → motive t :=
-fun {α} {motive} t (F_1 : (t : List α) → List.below t → motive t) => (
-  @List.rec α (fun t => PProd (motive t) (@List.below α motive t))
-    ⟨F_1 [] PUnit.unit, PUnit.unit⟩
-    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩)
-    t
-  ).1
+@[reducible] protected def List.brecOn.go.{u} : {a : Type} →
+  {motive : List a → Sort u} →
+    (t : List a) → ((t : List a) → List.below t → motive t) → motive t ×' List.below t :=
+fun {a} {motive} t F_1 =>
+  List.rec ⟨F_1 List.nil PUnit.unit, PUnit.unit⟩ (fun a_1 a_2 a_ih => ⟨F_1 (List.cons a_1 a_2) a_ih, a_ih⟩) t
+
+@[reducible] protected def List.brecOn.{u} : {a : Type} →
+  {motive : List a → Sort u} → (t : List a) → ((t : List a) → List.below t → motive t) → motive t :=
+fun {a} {motive} t F_1 => (List.brecOn.go t F_1).1
+
+protected theorem List.brecOn.eq.{u} : ∀ {a : Type} {motive : List a → Sort u} (t : List a)
+  (F_1 : (t : List a) → List.below t → motive t), List.brecOn t F_1 = F_1 t (List.brecOn.go t F_1).2
 ```
 -/
 private def mkBRecOnFromRec (recName : Name) (nParams : Nat)
     (all : Array Name) (brecOnName : Name) : MetaM Unit := do
+  let brecOnGoName := brecOnName.str "go"
+  let brecOnEqName := brecOnName.str "eq"
   let .recInfo recVal ← getConstInfo recName | return
   let lvl::lvls := recVal.levelParams.map (Level.param ·)
     | throwError "recursor {recName} has no levelParams"
   -- universe parameter names of brecOn
   let blps := recVal.levelParams
 
-  let decl ← forallTelescope recVal.type fun refArgs refBody => do
+  forallTelescope recVal.type fun refArgs refBody => do
     assert! refArgs.size > nParams + recVal.numMotives + recVal.numMinors
     let params  : Array Expr := refArgs[*...nParams]
     let motives : Array Expr := refArgs[nParams...(nParams + recVal.numMotives)]
@@ -241,9 +246,9 @@ private def mkBRecOnFromRec (recName : Name) (nParams : Nat)
       let fName := .mkSimple s!"F_{i + 1}"
       fDecls := fDecls.push (fName, fun _ => pure fType)
     withLocalDeclsD fDecls fun fs => do
-      let mut val := .const recName (rlvl :: lvls)
+      let mut go_val := .const recName (rlvl :: lvls)
       -- add parameters
-      val := mkAppN val params
+      go_val := mkAppN go_val params
       -- add type formers
       for motive in motives, below in belows do
         -- example: (motive := fun t => PProd (motive t) (@List.below α motive t))
@@ -252,30 +257,63 @@ private def mkBRecOnFromRec (recName : Name) (nParams : Nat)
           let belowType := mkAppN below targs
           let arg ← mkPProd cType belowType
           mkLambdaFVars targs arg
-        val := .app val arg
+        go_val := .app go_val arg
       -- add minor premises
       for minor in minors do
         let arg ← buildBRecOnMinorPremise rlvl motives belows fs (← inferType minor)
-        val := .app val arg
+        go_val := .app go_val arg
       -- add indices and major premise
-      val := mkAppN val indices
-      val := mkApp val major
-      -- project out first component
-      val ← mkPProdFstM val
+      go_val := mkAppN go_val indices
+      go_val := mkApp go_val major
 
       -- All parameters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs`
       let below_params := params ++ motives ++ indices ++ #[major] ++ fs
-      let type ← mkForallFVars below_params (mkAppN motives[idx]! (indices ++ #[major]))
-      val ← mkLambdaFVars below_params val
+      let motive_app := mkAppN motives[idx]! (indices.push major)
+      let below_app := mkAppN belows[idx]! (indices.push major)
+      let type ← mkForallFVars below_params (← mkPProd motive_app below_app)
+      go_val ← mkLambdaFVars below_params go_val
 
-      mkDefinitionValInferringUnsafe brecOnName blps type val .abbrev
+      let go_decl ← mkDefinitionValInferringUnsafe brecOnGoName blps type go_val .abbrev
 
-  addDecl (.defnDecl decl)
-  setReducibleAttribute decl.name
-  modifyEnv fun env => markAuxRecursor env decl.name
-  modifyEnv fun env => addProtected env decl.name
+      addDecl (.defnDecl go_decl)
+      setReducibleAttribute go_decl.name
+      modifyEnv fun env => addProtected env go_decl.name
 
-def mkBRecOn (indName : Name) : MetaM Unit := do
+      -- project out first component
+      let brecOnGoApp := mkAppN (.const brecOnGoName blvls) below_params
+      let val ← mkPProdFstM brecOnGoApp
+      let val ← mkLambdaFVars below_params val
+      let type ← mkForallFVars below_params motive_app
+      let decl ← mkDefinitionValInferringUnsafe brecOnName blps type val .abbrev
+
+      addDecl (.defnDecl decl)
+      setReducibleAttribute decl.name
+      modifyEnv fun env => markAuxRecursor env decl.name
+      modifyEnv fun env => addProtected env decl.name
+
+      let lhs := mkAppN (.const decl.name blvls) below_params
+      let rhs := fs[idx]!
+      let rhs := mkAppN rhs (indices.push major)
+      let rhs := mkApp rhs (← mkPProdSndM brecOnGoApp)
+      let thm_type ← mkEq lhs rhs
+      let thm_val ← mkFreshExprSyntheticOpaqueMVar thm_type
+      let mvar := thm_val.mvarId!
+      let cases ← mvar.cases major.fvarId!
+      for case in cases do
+        case.mvarId.refl (check := false)
+      let thm_val ← instantiateMVars thm_val
+      let thm_type ← mkForallFVars below_params thm_type
+      let thm_val ← mkLambdaFVars below_params thm_val
+      let thm_decl ← mkThmOrUnsafeDef {
+        name := brecOnEqName
+        levelParams := blps
+        type := thm_type
+        value := thm_val
+      }
+      addDecl thm_decl
+      modifyEnv fun env => addProtected env brecOnEqName
+
+public def mkBRecOn (indName : Name) : MetaM Unit := do
   withTraceNode `Meta.mkBRecOn (fun _ => return m!"{indName}") do
   let .inductInfo indVal ← getConstInfo indName | return
   unless indVal.isRec do return
diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean
index 1932a974b9..7cd588e2b6 100644
--- a/src/Lean/Meta/Tactic/Refl.lean
+++ b/src/Lean/Meta/Tactic/Refl.lean
@@ -17,10 +17,13 @@ namespace Lean.Meta
 /--
 Close given goal using `Eq.refl`.
 
+With (`check := false`), the elaborator does not check if the goal is actually a definitionaly
+equality.
+
 See `Lean.MVarId.applyRfl` for the variant that also consults `@[refl]` lemmas, and which
 backs the `rfl` tactic.
 -/
-def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
+def _root_.Lean.MVarId.refl (mvarId : MVarId) (check := true) : MetaM Unit := do
   mvarId.withContext do
     mvarId.checkNotAssigned `refl
     let targetType ← mvarId.getType'
@@ -28,9 +31,10 @@ def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
       throwTacticEx `rfl mvarId m!"equality expected{indentExpr targetType}"
     let lhs ← instantiateMVars targetType.appFn!.appArg!
     let rhs ← instantiateMVars targetType.appArg!
-    let success ← isDefEq lhs rhs
-    unless success do
-      throwTacticEx `rfl mvarId m!"equality lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
+    if check then
+      let success ← isDefEq lhs rhs
+      unless success do
+        throwTacticEx `rfl mvarId m!"equality lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
     let us := targetType.getAppFn.constLevels!
     let α := targetType.appFn!.appFn!.appArg!
     mvarId.assign (mkApp2 (mkConst ``Eq.refl  us) α lhs)
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..6d16fd2bc5 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please test stage2
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/2961.lean b/tests/lean/run/2961.lean
deleted file mode 100644
index f93268bb80..0000000000
--- a/tests/lean/run/2961.lean
+++ /dev/null
@@ -1,99 +0,0 @@
-def replace (f : Nat → Option Nat) (t : Nat) : Nat :=
-  match f t with
-  | some u => u
-  | none =>
-    match t with
-    | .zero => .zero
-    | .succ t' => replace f t'
-
-/--
-info: equations:
-@[defeq] theorem replace.eq_1 : ∀ (f : Nat → Option Nat),
-  replace f Nat.zero =
-    match f Nat.zero with
-    | some u => u
-    | none => Nat.zero
-@[defeq] theorem replace.eq_2 : ∀ (f : Nat → Option Nat) (t' : Nat),
-  replace f t'.succ =
-    match f t'.succ with
-    | some u => u
-    | none => replace f t'
--/
-#guard_msgs in
-#print equations replace
-
-/--
-error: Failed to realize constant replace.eq_def:
-  failed to generate unfold theorem for `replace`
-  case h_1
-  f : Nat → Option Nat
-  t : Nat
-  x : Option Nat
-  u : Nat
-  heq✝ : f t = some u
-  ⊢ replace f t = u
----
-error: Failed to realize constant replace.eq_def:
-  failed to generate unfold theorem for `replace`
-  case h_1
-  f : Nat → Option Nat
-  t : Nat
-  x : Option Nat
-  u : Nat
-  heq✝ : f t = some u
-  ⊢ replace f t = u
----
-error: Unknown identifier `replace.eq_def`
--/
-#guard_msgs in
-#check replace.eq_def
-
-def replace2 (f : Nat → Option Nat) (t1 t2 : Nat) : Nat :=
-  match f t1 with
-  | some u => u
-  | none =>
-    match t2 with
-    | .zero => .zero
-    | .succ t' => replace2 f t1 t'
-
-/--
-info: equations:
-@[defeq] theorem replace2.eq_1 : ∀ (f : Nat → Option Nat) (t1 : Nat),
-  replace2 f t1 Nat.zero =
-    match f t1 with
-    | some u => u
-    | none => Nat.zero
-@[defeq] theorem replace2.eq_2 : ∀ (f : Nat → Option Nat) (t1 t' : Nat),
-  replace2 f t1 t'.succ =
-    match f t1 with
-    | some u => u
-    | none => replace2 f t1 t'
--/
-#guard_msgs in
-#print equations replace2
-
-/--
-error: Failed to realize constant replace2.eq_def:
-  failed to generate unfold theorem for `replace2`
-  case h_1
-  f : Nat → Option Nat
-  t1 t2 : Nat
-  x : Option Nat
-  u : Nat
-  heq✝ : f t1 = some u
-  ⊢ replace2 f t1 t2 = u
----
-error: Failed to realize constant replace2.eq_def:
-  failed to generate unfold theorem for `replace2`
-  case h_1
-  f : Nat → Option Nat
-  t1 t2 : Nat
-  x : Option Nat
-  u : Nat
-  heq✝ : f t1 = some u
-  ⊢ replace2 f t1 t2 = u
----
-error: Unknown identifier `replace2.eq_def`
--/
-#guard_msgs in
-#check replace2.eq_def
diff --git a/tests/lean/run/5667.lean b/tests/lean/run/5667.lean
index 3eb11b544c..cbc88450a7 100644
--- a/tests/lean/run/5667.lean
+++ b/tests/lean/run/5667.lean
@@ -10,64 +10,25 @@ def optimize : Expr → Expr
     | _, _ => .const 0
 
 /--
-error: Failed to realize constant optimize.eq_def:
-  failed to generate equational theorem for `optimize`
-  e1 : Expr
-  bop : Unit
-  i : BitVec 32
-  heq : optimize e1 = Expr.const i
-  ⊢ (match bop,
-        (Expr.rec (fun i => ⟨Expr.const i, PUnit.unit⟩)
-            (fun op e1 e1_ih =>
-              ⟨match op, e1_ih.1 with
-                | x, Expr.const i => Expr.op op (Expr.const 0)
-                | x, x_1 => Expr.const 0,
-                e1_ih⟩)
-            e1).1 with
+info: optimize.eq_def (x✝ : Expr) :
+  optimize x✝ =
+    match x✝ with
+    | Expr.const i => Expr.const i
+    | Expr.op bop e1 =>
+      match bop, optimize e1 with
       | x, Expr.const i => Expr.op bop (Expr.const 0)
-      | x, x_1 => Expr.const 0) =
-      Expr.op bop (Expr.const 0)
----
-error: Failed to realize constant optimize.eq_def:
-  failed to generate equational theorem for `optimize`
-  e1 : Expr
-  bop : Unit
-  i : BitVec 32
-  heq : optimize e1 = Expr.const i
-  ⊢ (match bop,
-        (Expr.rec (fun i => ⟨Expr.const i, PUnit.unit⟩)
-            (fun op e1 e1_ih =>
-              ⟨match op, e1_ih.1 with
-                | x, Expr.const i => Expr.op op (Expr.const 0)
-                | x, x_1 => Expr.const 0,
-                e1_ih⟩)
-            e1).1 with
-      | x, Expr.const i => Expr.op bop (Expr.const 0)
-      | x, x_1 => Expr.const 0) =
-      Expr.op bop (Expr.const 0)
----
-error: Unknown identifier `optimize.eq_def`
+      | x, x_1 => Expr.const 0
 -/
 #guard_msgs in
 #check optimize.eq_def
 
 /--
-error: failed to generate equational theorem for `optimize`
-e1 : Expr
-bop : Unit
-i : BitVec 32
-heq : optimize e1 = Expr.const i
-⊢ (match bop,
-      (Expr.rec (fun i => ⟨Expr.const i, PUnit.unit⟩)
-          (fun op e1 e1_ih =>
-            ⟨match op, e1_ih.1 with
-              | x, Expr.const i => Expr.op op (Expr.const 0)
-              | x, x_1 => Expr.const 0,
-              e1_ih⟩)
-          e1).1 with
-    | x, Expr.const i => Expr.op bop (Expr.const 0)
-    | x, x_1 => Expr.const 0) =
-    Expr.op bop (Expr.const 0)
+info: equations:
+@[defeq] theorem optimize.eq_1 : ∀ (i : BitVec 32), optimize (Expr.const i) = Expr.const i
+theorem optimize.eq_2 : ∀ (e1 : Expr) (bop : Unit) (i : BitVec 32),
+  optimize e1 = Expr.const i → optimize (Expr.op bop e1) = Expr.op bop (Expr.const 0)
+theorem optimize.eq_3 : ∀ (e1 : Expr) (bop : Unit),
+  (∀ (i : BitVec 32), optimize e1 = Expr.const i → False) → optimize (Expr.op bop e1) = Expr.const 0
 -/
 #guard_msgs in
 #print equations optimize
@@ -112,3 +73,59 @@ theorem optimize3.eq_3 : ∀ (bop : Unit) (e1 : Expr),
 -/
 #guard_msgs in
 #print equations optimize3
+
+
+-- Mutual
+
+namespace Mutual
+
+mutual
+inductive Expr where
+  | const (i : BitVec 32)
+  | op (op : Unit) (e1 : Expr')
+inductive Expr' where
+  | const (i : BitVec 32)
+  | op (op : Unit) (e1 : Expr)
+end
+
+mutual
+def optimize : Expr → Expr
+  | .const i => .const i
+  | .op bop e1 =>
+    match bop, optimize' e1 with
+    | _, .const _ => .op bop (.const 0)
+    | _, _ => .const 0
+def optimize' : Expr' → Expr'
+  | .const i => .const i
+  | .op bop e1 =>
+    match bop, optimize e1 with
+    | _, .const _ => .op bop (.const 0)
+    | _, _ => .const 0
+end
+
+/--
+info: Mutual.optimize.eq_def (x✝ : Expr) :
+  optimize x✝ =
+    match x✝ with
+    | Expr.const i => Expr.const i
+    | Expr.op bop e1 =>
+      match bop, optimize' e1 with
+      | x, Expr'.const i => Expr.op bop (Expr'.const 0)
+      | x, x_1 => Expr.const 0
+-/
+#guard_msgs in
+#check optimize.eq_def
+/--
+info: Mutual.optimize'.eq_def (x✝ : Expr') :
+  optimize' x✝ =
+    match x✝ with
+    | Expr'.const i => Expr'.const i
+    | Expr'.op bop e1 =>
+      match bop, optimize e1 with
+      | x, Expr.const i => Expr'.op bop (Expr.const 0)
+      | x, x_1 => Expr'.const 0
+-/
+#guard_msgs in
+#check optimize'.eq_def
+
+end Mutual
diff --git a/tests/lean/run/eqValue.lean b/tests/lean/run/eqValue.lean
index d014a3d2e8..96be6cbf0e 100644
--- a/tests/lean/run/eqValue.lean
+++ b/tests/lean/run/eqValue.lean
@@ -4,6 +4,7 @@
   | 100  => 2
   | 1000 => 3
   | x+1  => f x
+termination_by structural x
 
 /-- info: f.eq_1 : f 0 = 1 -/
 #guard_msgs in
diff --git a/tests/lean/run/issue10195.lean b/tests/lean/run/issue10195.lean
index b2a221c10d..6ffb7ced42 100644
--- a/tests/lean/run/issue10195.lean
+++ b/tests/lean/run/issue10195.lean
@@ -82,22 +82,3 @@ info: theorem foo.eq_def.{u_1, u_2} : ∀ {n : Nat} (x : I n) (x' : I n),
 -/
 #guard_msgs(pass trace, all) in
 #print sig foo.eq_def
-
-
-noncomputable def nondep (x x' : I n) : Bool :=
- if h : P x then
- match (generalizing := false) x, x', id h with --NB: non-FVar discr
- | .cons a_2, .cons a_2', _ => nondep a_2 a_2'
- else false
-termination_by structural x
-
-/--
-info: theorem nondep.eq_def.{u_1, u_2} : ∀ {n : Nat} (x : I n) (x' : I n),
-  nondep x x' =
-    if h : P x then
-      match n, x, x', ⋯ with
-      | .(n + 1), a_2.cons, a_2'.cons, x => nondep a_2 a_2'
-    else false
--/
-#guard_msgs in
-#print sig nondep.eq_def
diff --git a/tests/lean/run/issue10424.lean b/tests/lean/run/issue10424.lean
index 0b96e6d3a4..3636bdb5fb 100644
--- a/tests/lean/run/issue10424.lean
+++ b/tests/lean/run/issue10424.lean
@@ -55,58 +55,6 @@ example (n0 n : Nat) (h : id n0 = n) :
   · sorry
   · sorry
 
--- Variant where the discriminant is already a constructor (so substituting the generalized equation
--- may actually help)
-
-/--
-error: Tactic `split` failed: Could not split an `if` or `match` expression in the goal
-
-Hint: Use `set_option trace.split.failure true` to display additional diagnostic information
-
-n : Nat
-⊢ Fin.last n.succ =
-    match n.succ with
-    | 0 => Fin.last 0
-    | n.succ => Fin.last (n + 1)
--/
-#guard_msgs in
-example (n : Nat) : Fin.last n.succ = match (motive := ∀ n, Fin (n+1)) Nat.succ n with
-  | 0 => Fin.last 0
-  | n + 1 => Fin.last (n + 1) := by
-  split <;> rfl
-
--- Manual generalization; the type-incorrect variant done by split
-
-/--
-error: Type mismatch
-  match m with
-  | 0 => Fin.last 0
-  | n.succ => Fin.last (n + 1)
-has type
-  Fin (m + 1)
-but is expected to have type
-  Fin (n.succ + 1)
----
-error: (kernel) declaration has metavariables '_example'
--/
-#guard_msgs in
-example (n m : Nat) (h : n.succ = m) : Fin.last n.succ = match (motive := ∀ n, Fin (n+1)) m with
-  | 0 => Fin.last 0
-  | n + 1 => Fin.last (n + 1) := sorry
-
--- What about using ndrec here?
-
-example (n m : Nat) (h : n.succ = m) : Fin.last n.succ =
-  h.symm.ndrec (motive := fun n => Fin (n + 1))
-    (match (motive := ∀ n, Fin (n+1)) m with
-    | 0 => Fin.last 0
-    | n + 1 => Fin.last (n + 1)) := by
-  split
-  · contradiction
-  · -- the cast is still here!
-    cases h
-    -- now the cast can rfl away
-    rfl
 
 -- Variant with proof-valued discriminant. This works (and always has):
 
diff --git a/tests/lean/run/issue10431.lean b/tests/lean/run/issue10431.lean
new file mode 100644
index 0000000000..dbf5ddab35
--- /dev/null
+++ b/tests/lean/run/issue10431.lean
@@ -0,0 +1,78 @@
+inductive L (α : Type u) : Type u where
+  | nil : L α
+  | cons : α → L α → L α
+
+def L.eq [BEq α] (xs ys : L α) : Bool :=
+  match _ : xs.ctorIdx == ys.ctorIdx with
+  | false => false
+  | true =>
+    match xs, ys with
+    | .nil, .nil => true
+    | .cons x xs, .cons y ys => x == y && xs.eq ys
+
+/--
+info: theorem L.eq.eq_def.{u_1} : ∀ {α : Type u_1} [inst : BEq α] (xs ys : L α),
+  xs.eq ys =
+    match h : xs.ctorIdx == ys.ctorIdx with
+    | false => false
+    | true =>
+      match xs, ys, h with
+      | L.nil, L.nil, h => true
+      | L.cons x xs, L.cons y ys, h => x == y && xs.eq ys
+-/
+#guard_msgs in
+#print sig L.eq.eq_def
+
+-- and mutual
+
+mutual
+inductive L1 (α : Type u) : Type u where
+  | nil : L1 α
+  | cons : α → L2 α → L1 α
+inductive L2 (α : Type u) : Type u where
+  | nil : L2 α
+  | cons : α → L1 α → L2 α
+end
+
+mutual
+def L1.eq [BEq α] (xs ys : L1 α) : Bool :=
+  match _ : xs.ctorIdx == ys.ctorIdx with
+  | false => false
+  | true =>
+    match xs, ys with
+    | .nil, .nil => true
+    | .cons x xs, .cons y ys => x == y && xs.eq ys
+def L2.eq [BEq α] (xs ys : L2 α) : Bool :=
+  match _ : xs.ctorIdx == ys.ctorIdx with
+  | false => false
+  | true =>
+    match xs, ys with
+    | .nil, .nil => true
+    | .cons x xs, .cons y ys => x == y && xs.eq ys
+end
+
+
+/--
+info: theorem L1.eq.eq_def.{u_1} : ∀ {α : Type u_1} [inst : BEq α] (xs ys : L1 α),
+  xs.eq ys =
+    match h : xs.ctorIdx == ys.ctorIdx with
+    | false => false
+    | true =>
+      match xs, ys, h with
+      | L1.nil, L1.nil, h => true
+      | L1.cons x xs, L1.cons y ys, h => x == y && xs.eq ys
+-/
+#guard_msgs in
+#print sig L1.eq.eq_def
+/--
+info: theorem L2.eq.eq_def.{u_1} : ∀ {α : Type u_1} [inst : BEq α] (xs ys : L2 α),
+  xs.eq ys =
+    match h : xs.ctorIdx == ys.ctorIdx with
+    | false => false
+    | true =>
+      match xs, ys, h with
+      | L2.nil, L2.nil, h => true
+      | L2.cons x xs, L2.cons y ys, h => x == y && xs.eq ys
+-/
+#guard_msgs in
+#print sig L2.eq.eq_def
diff --git a/tests/lean/run/issue2237.lean b/tests/lean/run/issue2237.lean
new file mode 100644
index 0000000000..e48e2722e9
--- /dev/null
+++ b/tests/lean/run/issue2237.lean
@@ -0,0 +1,35 @@
+inductive Ty where
+| star: Ty
+notation " ✶ " => Ty.star
+
+abbrev Context : Type := List Ty
+
+inductive Lookup : Context → Ty → Type where
+| z : Lookup (t :: Γ) t
+
+inductive Term : Context → Ty → Type where
+| var : Lookup Γ a → Term Γ a
+| lam : Term (✶ :: Γ) ✶ → Term Γ ✶
+| ap : Term Γ ✶ → Term Γ ✶ → Term Γ ✶
+
+abbrev plus : Term Γ a → Term Γ a
+| .var i => .var i
+| .lam n => .lam (plus n)
+| .ap (.lam _) m => plus m -- This case takes precedence over the next one.
+| .ap l m => (plus l).ap (plus m)
+
+/--
+error: failed to generate equational theorem for `plus`
+  failed to generate equality theorems for `match` expression `plus.match_1`
+  Γ✝ : Context
+  a✝ : Ty
+  motive✝ : Term Γ✝ a✝ → Sort u_1
+  n✝ : Term ( ✶ :: Γ✝) ✶
+  h_1✝ : (i : Lookup Γ✝ a✝) → motive✝ (Term.var i)
+  h_2✝ : (n : Term ( ✶ :: Γ✝) ✶ ) → motive✝ n.lam
+  h_3✝ : (a : Term ( ✶ :: Γ✝) ✶ ) → (m : Term Γ✝ ✶ ) → motive✝ (a.lam.ap m)
+  h_4✝ : (l m : Term Γ✝ ✶ ) → motive✝ (l.ap m)
+  ⊢ (⋯ ▸ fun x motive h_1 h_2 h_3 h_4 h => ⋯ ▸ h_2 n✝) n✝.lam motive✝ h_1✝ h_2✝ h_3✝ h_4✝ ⋯ = h_2✝ n✝
+-/
+#guard_msgs in
+#print equations plus
diff --git a/tests/lean/run/issue2962.lean b/tests/lean/run/issue2962.lean
new file mode 100644
index 0000000000..4ed83945aa
--- /dev/null
+++ b/tests/lean/run/issue2962.lean
@@ -0,0 +1,105 @@
+inductive N where
+  | zero : N
+  | succ : N → N
+
+def replace (f : N → Option N) (t : N) : N :=
+  match f t with
+  | some u => u
+  | none =>
+    match t with
+    | .zero => .zero
+    | .succ t' => replace f t'
+
+/--
+info: equations:
+@[defeq] theorem replace.eq_1 : ∀ (f : N → Option N),
+  replace f N.zero =
+    match f N.zero with
+    | some u => u
+    | none => N.zero
+@[defeq] theorem replace.eq_2 : ∀ (f : N → Option N) (t' : N),
+  replace f t'.succ =
+    match f t'.succ with
+    | some u => u
+    | none => replace f t'
+-/
+#guard_msgs in
+#print equations replace
+
+def replace2 (f : N → Option N) (t1 t2 : N) : N :=
+  match f t1 with
+  | some u => u
+  | none =>
+    match t2 with
+    | .zero => .zero
+    | .succ t' => replace2 f t1 t'
+
+/--
+info: equations:
+@[defeq] theorem replace2.eq_1 : ∀ (f : N → Option N) (t1 : N),
+  replace2 f t1 N.zero =
+    match f t1 with
+    | some u => u
+    | none => N.zero
+@[defeq] theorem replace2.eq_2 : ∀ (f : N → Option N) (t1 t' : N),
+  replace2 f t1 t'.succ =
+    match f t1 with
+    | some u => u
+    | none => replace2 f t1 t'
+-/
+#guard_msgs in
+#print equations replace2
+
+
+-- Now also mutual
+
+mutual
+inductive N1 where
+  | zero : N1
+  | succ : N2 → N1
+inductive N2 where
+  | zero : N2
+  | succ : N1 → N2
+end
+
+mutual
+def replaceMut1 (f : N1 → Option N1) (g : N2 → Option N2) (t : N1) : N1 :=
+  match f t with
+  | some u => u
+  | none =>
+    match t with
+    | .zero => .zero
+    | .succ t' => .succ (replaceMut2 f g t')
+def replaceMut2 (f : N1 → Option N1) (g : N2 → Option N2) (t : N2) : N2 :=
+  match g t with
+  | some u => u
+  | none =>
+    match t with
+    | .zero => .zero
+    | .succ t' => .succ (replaceMut1 f g t')
+end
+
+/--
+info: theorem replaceMut1.eq_def : ∀ (f : N1 → Option N1) (g : N2 → Option N2) (t : N1),
+  replaceMut1 f g t =
+    match f t with
+    | some u => u
+    | none =>
+      match t with
+      | N1.zero => N1.zero
+      | N1.succ t' => N1.succ (replaceMut2 f g t')
+-/
+#guard_msgs in
+#print sig replaceMut1.eq_def
+/--
+info: theorem replaceMut2.eq_def : ∀ (f : N1 → Option N1) (g : N2 → Option N2) (t : N2),
+  replaceMut2 f g t =
+    match g t with
+    | some u => u
+    | none =>
+      match t with
+      | N2.zero => N2.zero
+      | N2.succ t' => N2.succ (replaceMut1 f g t')
+-/
+#guard_msgs in
+#print sig replaceMut2.eq_def
diff --git a/tests/lean/run/issue6592.lean b/tests/lean/run/issue6592.lean
new file mode 100644
index 0000000000..05ca187c50
--- /dev/null
+++ b/tests/lean/run/issue6592.lean
@@ -0,0 +1,136 @@
+/--
+Colors of red black tree nodes.
+-/
+inductive Color where
+  | black
+  | red
+
+/--
+The basic red black tree data structure without any invariant etc. attached.
+-/
+inductive Raw (α : Type u) where
+  /--
+  The empty tree.
+  -/
+  | nil : Raw α
+  /--
+  A node with left and right successor, its color and a piece of data
+  -/
+  | node (left : Raw α) (data : α) (color : Color) (right : Raw α) : Raw α
+
+namespace Raw
+
+/--
+Paint the color of the root of `t` to given color `c`.
+-/
+@[inline]
+def paintColor (c : Color) (t : Raw α) : Raw α :=
+  match t with
+  | .nil => .nil
+  | .node l d _ r => .node l d c r
+
+-- Balanced insert into the left child, fixing red on red sequences on the way.
+@[inline]
+def baliL (d : α) : Raw α → Raw α → Raw α
+  | .node (.node t₁ data₁ .red t₂) data₂ .red t₃, right
+  | .node t₁ data₁ .red (.node t₂ data₂ .red t₃), right =>
+      .node (.node t₁ data₁ .black t₂) data₂ .red (.node t₃ d .black right)
+  | left, right => .node left d .black right
+
+-- Balanced insert into the right child, fixing red on red sequences on the way.
+@[inline]
+def baliR (d : α) : Raw α → Raw α → Raw α
+  | left, .node t₁ data₁ .red (.node t₂ data₂ .red t₃)
+  | left, .node (.node t₁ data₁ .red t₂) data₂ .red t₃ =>
+      .node (.node left d .black t₁) data₁ .red (.node t₂ data₂ .black t₃)
+  | left, right => .node left d .black right
+
+-- Balance a tree on the way up from deletion, prioritizing the left side.
+def baldL (d : α) : Raw α → Raw α → Raw α
+  | .node t₁ data .red t₂, right =>
+      .node (.node t₁ data .black t₂) d .red right
+  | left, .node t₁ data .black t₂ =>
+      baliR d left (.node t₁ data .red t₂)
+  | left, .node (.node t₁ data₁ .black t₂) data₂ .red t₃ =>
+      .node (.node left d .black t₁) data₁ .red (baliR data₂ t₂ (paintColor .red t₃))
+  | left, right => .node left d .red right
+
+-- Balance a tree on the way up from deletion, prioritizing the right side.
+def baldR (d : α) : Raw α → Raw α → Raw α
+  | left, .node t₁ data .red t₂ =>
+      .node left d .red (.node t₁ data .black t₂)
+  | .node t₁ data .black t₂, right =>
+      baliL d (.node t₁ data .red t₂) right
+  | .node  t₁ data₁ .red (.node t₂ data₂ .black t₃), right =>
+      .node (baliL data₁ (paintColor .red t₁) t₂) data₁ .red (.node t₃ data₂ .black right)
+  | left, right => .node left d .red right
+
+-- Appends one tree to another while painting the correct color
+def appendTrees : Raw α → Raw α → Raw α
+  | .nil, t => t
+  | t, .nil => t
+  | .node left₁ data₁ .red right₁, .node left₂ data₂ .red right₂ =>
+    match appendTrees right₁ left₂ with
+    | .node left₃ data₃ .red right₃ =>
+        .node (.node left₁ data₁ .red left₃) data₃ .red (.node right₃ data₂ .red right₂)
+    | t                   => .node left₁ data₁ .red (.node t data₂ .red right₂)
+  | .node left₁ data₁ .black right₁, .node left₂ data₂ .black right₂ =>
+    match appendTrees right₁ left₂ with
+    | .node left₃ data₃ .red right₃ =>
+        .node (node left₁ data₁ .black left₃) data₃ .red (node right₃ data₂ .black right₂)
+    | t                   => baldL data₁ left₁ (node t data₂ .black right₂)
+  | t, .node left data .red right => node (appendTrees t left) data .red right
+  | .node left data .red right, t => .node left data .red (appendTrees right t)
+
+def del [Ord α] (d : α) : Raw α → Raw α
+  | .nil => .nil
+  | .node left data _ right =>
+    match compare d data with
+    | .lt =>
+      match left with
+      | .node _ _ .black _ => baldL data (del d left) right
+      | _ => .node (del d left) data .red right
+    | .eq => appendTrees left right
+    | .gt =>
+      match right with
+      | .node _ _ .black _ => baldR data left (del d right)
+      | _ => .node left data .red (del d right)
+
+
+/--
+info: equations:
+@[defeq] theorem Raw.del.eq_1.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α), del d nil = nil
+@[defeq] theorem Raw.del.eq_2.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d d_1 : α) (color : Color) (left_1 : Raw α)
+  (data : α) (right left_3 : Raw α) (data_1 : α) (right_1 : Raw α),
+  del d ((left_1.node data Color.black right).node d_1 color (left_3.node data_1 Color.black right_1)) =
+    match compare d d_1 with
+    | Ordering.lt => baldL d_1 (del d (left_1.node data Color.black right)) (left_3.node data_1 Color.black right_1)
+    | Ordering.eq => (left_1.node data Color.black right).appendTrees (left_3.node data_1 Color.black right_1)
+    | Ordering.gt => baldR d_1 (left_1.node data Color.black right) (del d (left_3.node data_1 Color.black right_1))
+theorem Raw.del.eq_3.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d d_1 : α) (color : Color) (r left_1 : Raw α) (data : α)
+  (right : Raw α),
+  (∀ (left : Raw α) (data : α) (right : Raw α), r = left.node data Color.black right → False) →
+    del d ((left_1.node data Color.black right).node d_1 color r) =
+      match compare d d_1 with
+      | Ordering.lt => baldL d_1 (del d (left_1.node data Color.black right)) r
+      | Ordering.eq => (left_1.node data Color.black right).appendTrees r
+      | Ordering.gt => (left_1.node data Color.black right).node d_1 Color.red (del d r)
+theorem Raw.del.eq_4.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α) (l : Raw α) (d_1 : α) (color : Color)
+  (left_2 : Raw α) (data : α) (right : Raw α),
+  (∀ (left : Raw α) (data : α) (right : Raw α), l = left.node data Color.black right → False) →
+    del d (l.node d_1 color (left_2.node data Color.black right)) =
+      match compare d d_1 with
+      | Ordering.lt => (del d l).node d_1 Color.red (left_2.node data Color.black right)
+      | Ordering.eq => l.appendTrees (left_2.node data Color.black right)
+      | Ordering.gt => baldR d_1 l (del d (left_2.node data Color.black right))
+theorem Raw.del.eq_5.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α) (l : Raw α) (d_1 : α) (color : Color) (r : Raw α),
+  (∀ (left : Raw α) (data : α) (right : Raw α), l = left.node data Color.black right → False) →
+    (∀ (left : Raw α) (data : α) (right : Raw α), r = left.node data Color.black right → False) →
+      del d (l.node d_1 color r) =
+        match compare d d_1 with
+        | Ordering.lt => (del d l).node d_1 Color.red r
+        | Ordering.eq => l.appendTrees r
+        | Ordering.gt => l.node d_1 Color.red (del d r)
+-/
+#guard_msgs in
+#print equations del
diff --git a/tests/lean/run/issue9846.lean b/tests/lean/run/issue9846.lean
new file mode 100644
index 0000000000..95779d1c5d
--- /dev/null
+++ b/tests/lean/run/issue9846.lean
@@ -0,0 +1,21 @@
+def testMatch : Array α → Unit
+  | #[_] => ()
+  | _ => ()
+
+/--
+error: Failed to realize constant testMatch.match_1.eq_1:
+  failed to generate equality theorems for `match` expression `testMatch.match_1`
+  case isTrue
+  α✝ : Type u_1
+  motive✝ : Array α✝ → Sort u_2
+  x✝¹ : Array α✝
+  h_1✝ : (head : α✝) → motive✝ #[head]
+  h_2✝ : (x : Array α✝) → motive✝ x
+  x✝ : ∀ (head : α✝), x✝¹ = #[head] → False
+  h✝ : x✝¹.size = 1
+  ⊢ (⋯ ▸ fun h => ⋯ ▸ h_1✝ (x✝¹.getLit 0 ⋯ ⋯)) ⋯ = h_2✝ x✝¹
+---
+error: Unknown constant `testMatch.match_1.eq_1`
+-/
+#guard_msgs in
+#print testMatch.match_1.eq_1
diff --git a/tests/lean/run/partial_fixpoint.lean b/tests/lean/run/partial_fixpoint.lean
index ef727dd57b..893bcbebea 100644
--- a/tests/lean/run/partial_fixpoint.lean
+++ b/tests/lean/run/partial_fixpoint.lean
@@ -13,7 +13,7 @@ partial_fixpoint
 
 /--
 info: equations:
-@[defeq] theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1)
+theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1)
 -/
 #guard_msgs in
 #print equations loop
diff --git a/tests/lean/run/structuralEqn6.lean b/tests/lean/run/structuralEqn6.lean
new file mode 100644
index 0000000000..1acb9df7b5
--- /dev/null
+++ b/tests/lean/run/structuralEqn6.lean
@@ -0,0 +1,87 @@
+def trailingZeros (i : Int) : Nat :=
+  if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
+where
+  aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
+    match k, (by omega : k ≠ 0) with
+    | k + 1, _ =>
+      if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
+      else acc
+  termination_by structural k
+
+/--
+info: equations:
+@[defeq] theorem trailingZeros.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
+  (hk_2 : i.natAbs ≤ k_2 + 1),
+  trailingZeros.aux k_2.succ i hi hk_2 acc = if h : i % 2 = 0 then trailingZeros.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
+-/
+#guard_msgs(pass trace, all) in
+#print equations trailingZeros.aux
+
+
+-- set_option trace.Elab.definition.eqns true
+-- set_option trace.split.debug true
+-- set_option trace.Meta.Match.unify true
+
+def trailingZeros' (i : Int) : Nat :=
+  if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
+where
+  aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
+    match k, (by omega : k ≠ 0) with
+    | k + 1, _ =>
+      if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
+      else acc
+  termination_by k
+
+/--
+info: equations:
+theorem trailingZeros'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
+  (hk_2 : i.natAbs ≤ k_2 + 1),
+  trailingZeros'.aux k_2.succ i hi hk_2 acc =
+    if h : i % 2 = 0 then trailingZeros'.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
+-/
+#guard_msgs(pass trace, all) in
+#print equations trailingZeros'.aux
+
+def trailingZeros2 (i : Int) : Nat :=
+  if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
+where
+  aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
+    match k  with
+    | k + 1 =>
+      if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
+      else acc
+    | 0 => by omega
+  termination_by structural k
+
+/--
+info: equations:
+@[defeq] theorem trailingZeros2.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (hk_2 : i.natAbs ≤ k_2 + 1),
+  trailingZeros2.aux k_2.succ i hi hk_2 acc =
+    if h : i % 2 = 0 then trailingZeros2.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
+@[defeq] theorem trailingZeros2.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
+  trailingZeros2.aux 0 i hi hk_2 acc = acc
+-/
+#guard_msgs(pass trace, all) in
+#print equations trailingZeros2.aux
+
+def trailingZeros2' (i : Int) : Nat :=
+  if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
+where
+  aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
+    match k  with
+    | k + 1 =>
+      if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
+      else acc
+    | 0 => by omega
+  termination_by  k
+
+/--
+info: equations:
+theorem trailingZeros2'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (hk_2 : i.natAbs ≤ k_2 + 1),
+  trailingZeros2'.aux k_2.succ i hi hk_2 acc =
+    if h : i % 2 = 0 then trailingZeros2'.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
+theorem trailingZeros2'.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
+  trailingZeros2'.aux 0 i hi hk_2 acc = acc
+-/
+#guard_msgs(pass trace, all) in
+#print equations trailingZeros2'.aux
diff --git a/tests/lean/run/structuralEqns2.lean b/tests/lean/run/structuralEqns2.lean
index 8b5e568076..7ca1e91667 100644
--- a/tests/lean/run/structuralEqns2.lean
+++ b/tests/lean/run/structuralEqns2.lean
@@ -12,7 +12,7 @@ def g (i j : Nat) : Nat :=
   | Nat.succ j => g i j
 
 /-- info: (some g.eq_def) -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #eval tst ``g
 #check g.eq_1
 #check g.eq_2
diff --git a/tests/lean/run/structuralEqns4.lean b/tests/lean/run/structuralEqns4.lean
new file mode 100644
index 0000000000..b0226587e2
--- /dev/null
+++ b/tests/lean/run/structuralEqns4.lean
@@ -0,0 +1,44 @@
+inductive N where | zero | succ (n : N)
+
+/--
+info: protected theorem N.brecOn.eq.{u} : ∀ {motive : N → Sort u} (t : N) (F_1 : (t : N) → N.below t → motive t),
+  N.brecOn t F_1 = F_1 t (N.brecOn.go t F_1).2
+-/
+#guard_msgs in #print sig N.brecOn.eq
+
+-- set_option trace.Elab.definition.structural.eqns true
+
+def g (i : Nat) (j : N) : N :=
+  if i < 5 then .zero else
+  match j with
+  | .zero => N.zero.succ
+  | .succ j => g i j
+termination_by structural j
+
+
+/--
+info: theorem g.eq_def : ∀ (i : Nat) (j : N),
+  g i j =
+    if i < 5 then N.zero
+    else
+      match j with
+      | N.zero => N.zero.succ
+      | j.succ => g i j
+-/
+#guard_msgs(pass trace, all) in #print sig g.eq_def
+
+
+def N.beq : (m n : N) → Bool
+| .zero, .zero => true
+| .succ m, .succ n => N.beq m n
+| _, _ => false
+
+/--
+info: theorem N.beq.eq_def : ∀ (x x_1 : N),
+  x.beq x_1 =
+    match x, x_1 with
+    | N.zero, N.zero => true
+    | m.succ, n.succ => m.beq n
+    | x, x_2 => false
+-/
+#guard_msgs(pass trace, all) in #print sig N.beq.eq_def
diff --git a/tests/lean/run/structuralEqns5.lean b/tests/lean/run/structuralEqns5.lean
new file mode 100644
index 0000000000..bb9ee64f9e
--- /dev/null
+++ b/tests/lean/run/structuralEqns5.lean
@@ -0,0 +1,76 @@
+inductive Tree (α : Type u) : Type u where
+  | node : α → (Bool → List (Tree α)) → Tree α
+
+mutual
+def Tree.size : Tree α → Nat
+  | .node _ tsf => 1 + size_aux (tsf true) + size_aux (tsf false)
+termination_by structural t => t
+def Tree.size_aux : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size t + size_aux ts
+end
+
+/--
+info: theorem Tree.size.eq_def.{u_1} : ∀ {α : Type u_1} (x : Tree α),
+  x.size =
+    match x with
+    | Tree.node a tsf => 1 + Tree.size_aux (tsf true) + Tree.size_aux (tsf false)
+-/
+#guard_msgs in
+#print sig Tree.size.eq_def
+
+/--
+info: theorem Tree.size_aux.eq_def.{u_1} : ∀ {α : Type u_1} (x : List (Tree α)),
+  Tree.size_aux x =
+    match x with
+    | [] => 0
+    | t :: ts => t.size + Tree.size_aux ts
+-/
+#guard_msgs in
+#print sig Tree.size_aux.eq_def
+
+mutual
+def Tree.size1 : Tree α → Nat
+  | .node _ tsf => 1 + size_aux2 (tsf true) + size_aux2 (tsf false)
+termination_by structural t => t
+def Tree.size2 : Tree α → Nat
+  | .node _ tsf => 1 + size_aux1 (tsf true) + size_aux1 (tsf false)
+termination_by structural t => t
+def Tree.size_aux1 : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size2 t + size_aux2 ts
+def Tree.size_aux2 : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size1 t + size_aux1 ts
+end
+
+/--
+info: theorem Tree.size1.eq_def.{u_1} : ∀ {α : Type u_1} (x : Tree α),
+  x.size1 =
+    match x with
+    | Tree.node a tsf => 1 + Tree.size_aux2 (tsf true) + Tree.size_aux2 (tsf false)
+-/
+#guard_msgs in #print sig Tree.size1.eq_def
+/--
+info: theorem Tree.size2.eq_def.{u_1} : ∀ {α : Type u_1} (x : Tree α),
+  x.size2 =
+    match x with
+    | Tree.node a tsf => 1 + Tree.size_aux1 (tsf true) + Tree.size_aux1 (tsf false)
+-/
+#guard_msgs in #print sig Tree.size2.eq_def
+/--
+info: theorem Tree.size_aux1.eq_def.{u_1} : ∀ {α : Type u_1} (x : List (Tree α)),
+  Tree.size_aux1 x =
+    match x with
+    | [] => 0
+    | t :: ts => t.size2 + Tree.size_aux2 ts
+-/
+#guard_msgs in #print sig Tree.size_aux1.eq_def
+/--
+info: theorem Tree.size_aux2.eq_def.{u_1} : ∀ {α : Type u_1} (x : List (Tree α)),
+  Tree.size_aux2 x =
+    match x with
+    | [] => 0
+    | t :: ts => t.size1 + Tree.size_aux1 ts
+-/
+#guard_msgs in #print sig Tree.size_aux2.eq_def