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