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
2025-10-07 14:53:09 +02:00 · 2025-10-07 14:53:09 +02:00 · 8655f7706f
commit 8655f7706f
parent 5c92ffc64d
22 changed files with 834 additions and 356 deletions
--- 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
--- 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
--- 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

--- 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?
--- 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
--- 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)
--- 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;
--- a/tests/lean/run/2961.lean
+++ b/tests/lean/run/2961.lean
@ -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
--- 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
--- 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
--- 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
--- 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):

--- a/tests/lean/run/issue10431.lean
+++ 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
--- a/tests/lean/run/issue2237.lean
+++ 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
--- a/tests/lean/run/issue2962.lean
+++ 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
--- a/tests/lean/run/issue6592.lean
+++ 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
--- a/tests/lean/run/issue9846.lean
+++ 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
--- 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
--- a/tests/lean/run/structuralEqn6.lean
+++ 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
--- 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
--- a/tests/lean/run/structuralEqns4.lean
+++ 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
--- a/tests/lean/run/structuralEqns5.lean
+++ 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