diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 6961e0d625ec..fb08fa575869 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -4,19 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Joachim Breitner
 -/
 module
-
 prelude
-
 import Lean.Elab.PreDefinition.EqnsUtils
+import Lean.Meta.HaveTelescope
+import Lean.Meta.LetToHave
 import Lean.Meta.Match.NamedPatterns
+import Lean.Meta.Match.Rewrite
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Split
+import Lean.Meta.Tactic.SplitIf
 import Lean.Meta.Tactic.CasesOnStuckLHS
 
 /-!
 This module implements the generation of equational theorems, given unfolding theorems.
 The unfolding theorems are generated differently for different kinds of recursive definition,
-but the code here is no longer cares about that.
+but the code here no longer cares about that.
 
 -/
 
@@ -38,6 +40,10 @@ def unfoldThmType (declName : Name) : MetaM Expr := do
       let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
       mkForallFVars xs type
 
+/--
+Unfolds the application of `declName` on the left-hand side of an equality goal, using its
+unfolding theorem when available and delta reduction otherwise.
+-/
 def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   if let some unfoldThm ← getUnfoldEqnFor? declName (nonRec := false) then
     -- Recursive definition: Use unfolding lemma
@@ -55,6 +61,29 @@ def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withC
     -- Else use delta reduction
     deltaLHS mvarId
 
+/--
+Rewrites a matcher application on the left-hand side of an equality goal with the congruence
+equation of the first alternative that applies. Equation statements are computed with the same
+rewrite, so it proves equations whose discriminants are not constructor applications.
+-/
+def rwMatcherLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do
+  let target ← mvarId.getType'
+  let some (_, lhs, rhs) := target.eq? | return none
+  let some app ← matchMatcherApp? lhs | return none
+  for i in *...app.numAlts do
+    let r ← rwMatcher i lhs
+    if r.expr != lhs then
+      let targetNew ← mkEq r.expr rhs
+      let some proof := r.proof? | return some (← mvarId.replaceTargetDefEq targetNew)
+      let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew
+      mvarId.assign (← mkEqTrans proof mvarNew)
+      return some mvarNew.mvarId!
+  return none
+
+/--
+Proves a generated equation type for `declName`. After introducing its parameters and hypotheses,
+tries reflexivity, then unfolds the definition and reduces or splits the remaining cases.
+-/
 partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do
   withTraceNode `Elab.definition.eqns (fun _ => return m!"proving:{indentExpr type}") do
   withNewMCtxDepth do
@@ -99,9 +128,15 @@ partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do
           mvarIds.forM go
         else if let some mvarIds ← splitTarget? mvarId (useNewSemantics := true) then
           mvarIds.forM go
+        else if let some mvarId ← rwMatcherLHS? mvarId then
+          go mvarId
         else
           throwError "failed to generate equational theorem for `{.ofConstName declName}`\n{MessageData.ofGoal mvarId}"
 
+/--
+Checks whether the left-hand side of a quantified equality depends on `fvarId`.
+For a non-equality conclusion, checks the entire conclusion.
+-/
 def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
   forallTelescope type fun _ type => do
     if let some (_, lhs, _) ← matchEq? type then
@@ -109,9 +144,7 @@ def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
     else
       dependsOn type fvarId
 
-/--
-  Eliminate `namedPatterns` from equation, and trivial hypotheses.
--/
+/-- Eliminates named-pattern annotations and redundant equality hypotheses from an equation type. -/
 def simpEqnType (eqnType : Expr) : MetaM Expr := do
   forallTelescopeReducing (← instantiateMVars eqnType) fun ys type => do
     let proofVars := collect type
@@ -152,6 +185,10 @@ where
     runST (go e)
 
 
+/--
+Closes a terminal goal over its free variables and relevant propositional hypotheses, simplifies
+the resulting equation type, and appends it to the state. RHS bindings remain inside the target.
+-/
 partial def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := mvarId.withContext do
   let target ← mvarId.getType'
   let fvarState := collectFVars {} target
@@ -182,7 +219,7 @@ where
     We say the type/proposition is "irrelevant" if
     1- It does not contain any variable in `fvarIdSet` OR
     2- It is of the form `x = t` or `t = x` where `x` is a free variable
-       that is not in `fvarIdSet`. This can of equality can be eliminated by substitution.  -/
+       that is not in `fvarIdSet`. This kind of equality can be eliminated by substitution.  -/
   isIrrelevant (fvarIdSet : FVarIdSet) (type : Expr) : MetaM Bool := do
     if Option.isNone <| type.find? fun e => e.isFVar && fvarIdSet.contains e.fvarId! then
       return true
@@ -192,10 +229,12 @@ where
     else
       return false
 
+  /-- Adds a declaration after recursively collecting the dependencies of its type. -/
   pushDecl (fvarIdSet : FVarIdSet) (fvarIds : Array FVarId) (localDecl : LocalDecl) : MetaM (FVarIdSet × Array FVarId) := do
     let (fvarIdSet, fvarIds) ← collectDeps fvarIdSet fvarIds (← instantiateMVars localDecl.type)
     return (fvarIdSet.insert localDecl.fvarId, fvarIds.push localDecl.fvarId)
 
+  /-- Extends the selected declarations with the transitive type dependencies of `type`. -/
   collectDeps (fvarIdSet : FVarIdSet) (fvarIds : Array FVarId) (type : Expr) : MetaM (FVarIdSet × Array FVarId) := do
     let s := collectFVars {} type
     let usedFVarIds ← sortFVarIds <| s.fvarSet.toArray
@@ -207,114 +246,355 @@ where
     return (fvarIdSet, fvarIds)
 
 /--
-Zeta reduces `let` and `have` while consuming metadata.
-Returns true if progress is made.
+A matcher splitter invocation whose arguments are well-scoped in the goal's local context.
+Dependencies on bindings inside the RHS are enclosed in `let`/`have` expressions in the arguments.
 -/
-partial def expand (progress : Bool) (e : Expr) : Bool × Expr :=
-  match e with
-  | Expr.letE _ _ v b _ => expand true (b.instantiate1 v)
-  | Expr.mdata _ b      => expand true b
-  | e                   => (progress, e)
+structure MatchToSplit where
+  declName : Name
+  levels : Array Level
+  params : Array Expr
+  discrs : Array Expr
+  deriving BEq, Hashable
 
-def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do
-  let target ← mvarId.getType'
-  let some (_, lhs, rhs) := target.eq? | return none
-  let (true, rhs') := expand false rhs | return none
-  return some (← mvarId.replaceTargetDefEq (← mkEq lhs rhs'))
+/--
+Follows a chain of local `let`/`have` aliases until reaching an ordinary variable or a non-variable
+value. Only aliases at the head are followed; subexpressions of the value remain shared.
+-/
+partial def resolveLetVar (e : Expr) : MetaM Expr := do
+  match e.consumeMData with
+  | .fvar fvarId =>
+    if let some value := (← fvarId.getDecl).value? (allowNondep := true) then
+      resolveLetVar value
+    else
+      return e
+  | _ => return e
+
+/--
+Finds the first eligible matcher in `rhs` whose splitter invocation is not in `exceptions`.
+At least one discriminant must resolve to a variable in the goal's local context. Enclosing RHS
+bindings are closed over the splitter arguments; captures of enclosing lambda or alternative
+parameters make a matcher ineligible.
 
+Binding values are searched before their bodies. For recursive definitions, unless deep splitting
+is enabled, a candidate must have an alternative with a recursive call depending on its binders.
+-/
+partial def findMatchToSplit? (rhs : Expr) (declNames : Array Name)
+    (exceptions : Std.HashSet MatchToSplit) : MetaM (Option MatchToSplit) := do
+  let outer ← getLCtx
+  let deep := backward.eqns.deepRecursiveSplit.get (← getOptions)
+  visit outer deep #[] rhs
+where
+  visit (outer : LocalContext) (deep : Bool) (lets : Array Expr) (e : Expr) :
+      MetaM (Option MatchToSplit) := do
+    checkSystem "findMatchToSplit"
+    if let some app ← matchMatcherApp? e then
+      let eligible := declNames.isEmpty || deep || app.alts.any fun alt =>
+        (alt.find? fun e => declNames.any e.isAppOf && e.hasLooseBVars).isSome
+      if eligible then
+        let hasVar ← app.discrs.anyM fun discr => do
+          let discr ← resolveLetVar discr
+          return discr.isFVar && outer.contains discr.fvarId!
+        if hasVar then
+          let closed ← mkLetFVars lets e (generalizeNondepLet := false)
+          -- Captures of enclosing lambdas and match alternatives prevent a split.
+          if !closed.hasAnyFVar (fun x => !outer.contains x) then
+            let params ← app.params.mapM fun e => mkLetFVars lets e (generalizeNondepLet := false)
+            let discrs ← app.discrs.mapM fun e => do
+              let resolved ← resolveLetVar e
+              mkLetFVars lets resolved (generalizeNondepLet := false)
+            unless (params ++ discrs).any (fun e => e.hasAnyFVar fun x => !outer.contains x) do
+              let candidate := { declName := app.matcherName, levels := app.matcherLevels, params, discrs }
+              unless exceptions.contains candidate do return some candidate
+    if let .const name _ := e.getAppFn then
+      if name == ``WellFounded.fix || isBRecOnRecursor (← getEnv) name then
+        return none
+    match e with
+    | .letE .. =>
+      letTelescope e fun xs body => do
+        let mut lets := lets
+        for x in xs do
+          if let some candidate ← visit outer deep lets ((← x.fvarId!.getDecl).value (allowNondep := true)) then
+            return some candidate
+          lets := lets.push x
+        visit outer deep lets body
+    | .lam n t b bi | .forallE n t b bi =>
+      withLocalDecl n bi t fun x => visit outer deep lets (b.instantiate1 x)
+    | .app .. =>
+      if !e.getAppFn.isConst then
+        if let some candidate ← visit outer deep lets e.getAppFn then return some candidate
+      for arg in e.getAppArgs do
+        if let some candidate ← visit outer deep lets arg then return some candidate
+      return none
+    | .mdata _ b | .proj _ _ b => visit outer deep lets b
+    | _ => return none
 
 /--
-  Quick filter for deciding whether to use `simpMatch?` at `mkEqnTypes`.
-  If the result is `false`, then it is not worth trying `simpMatch`.
+Result of simplifying a telescope suffix. All fields use loose bound variables for the preceding
+bindings. `proof?`, when present, proves equality from the original suffix to `expr`; otherwise
+the change is definitional. `type` is the type of the suffix in that prefix context.
 -/
-def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
-  let env ← getEnv
-  let find (root : Expr) : ExceptT Unit MetaM Unit :=
-    root.forEach fun e => do
-      if let some info := isMatcherAppCore? env e then
-        let args := e.getAppArgs
-        for discr in args[info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs)] do
-          if (← Meta.isConstructorApp discr) then
-            throwThe Unit ()
-  return (← (find e).run) matches .error _
-
-def findMatchToSplit? (deepRecursiveSplit : Bool) (env : Environment) (e : Expr)
-    (declNames : Array Name) (exceptionSet : ExprSet) : Option Expr :=
-  e.findExt? fun e => Id.run do
-    if e.hasLooseBVars || exceptionSet.contains e then
-      return Expr.FindStep.visit
-    else if let some info := isMatcherAppCore? env e then
-      let args := e.getAppArgs
-      -- If none of the discriminants is a free variable, then it is not worth splitting the match
-      let mut hasFVarDiscr := false
-      for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do
-        let discr := args[i]!
-        if discr.isFVar then
-          hasFVarDiscr := true
-          break
-      unless hasFVarDiscr do
-        return Expr.FindStep.visit
-      -- For non-recursive functions (`declNames` empty), we split here
-      if declNames.isEmpty then
-          return Expr.FindStep.found
-      -- For recursive functions, the “new” behavior is to likewise split
-      if deepRecursiveSplit then
-          return Expr.FindStep.found
-      -- Else, the “old” behavior is split only when at least one alternative contains a `declNames`
-      -- application with loose bound variables.
-      for i in info.getFirstAltPos...(info.getFirstAltPos + info.numAlts) do
-        let alt := args[i]!
-        if Option.isSome <| alt.find? fun e => declNames.any e.isAppOf && e.hasLooseBVars then
-          return Expr.FindStep.found
-      return Expr.FindStep.visit
-    else
-      let Expr.const declName .. := e.getAppFn | return Expr.FindStep.visit
-      if declName == ``WellFounded.fix || isBRecOnRecursor env declName then
-        -- We should not go inside unfolded nested recursive applications
-        return Expr.FindStep.done
-      else
-        return Expr.FindStep.visit
+structure EqnTelescopeResult where
+  expr : Expr
+  type : Expr
+  proof? : Option Expr := none
 
-partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := commitWhenSome? do
-  let target ← mvarId.getType'
-  let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do
-    if let some e := findMatchToSplit? (backward.eqns.deepRecursiveSplit.get (← getOptions)) (← getEnv)
-                                       target declNames badCases then
-      try
-        Meta.Split.splitMatch mvarId e
-      catch ex =>
-        trace[Elab.definition.eqns] "cannot split {e}\n{ex.toMessageData}"
-        go (badCases.insert e)
+/--
+Simplifies the suffix `e` beginning at binding `i` of the telescope described by `info`.
+The preceding bindings are represented by free variables in `xs` and the cached expressions in
+`info`, but by loose bound variables in `e` and the result. Abstraction is batched so that closing
+each binder does not repeatedly traverse the entire remaining body and proof.
+
+Unused values are skipped. Fixed values admit only `dsimp`; other values admit propositional
+rewrites. Each updated value is entered as a dependent local definition so that matcher reduction
+can use its value while simplifying the remainder. The simplifier cache is isolated for that
+scope. A changed body is rebuilt with `let`; `simpEqn` then uses `letToHave` to recover `have`
+bindings where their bodies remain well typed with the variable abstract.
+
+A value rewrite is lifted with `congrArg (fun x => originalBody)`. The body proof is closed with
+`let x := updatedValue`, since it may rely on that value; the two proofs compose by transitivity.
+For a nonfixed binding the result type cannot depend on `x`, so its bound-variable slot is removed.
+For a fixed binding the result type is closed with the binding itself.
+-/
+partial def simpEqnTelescope (info : HaveTelescopeInfo) (fixed used : Array Bool)
+    (e : Expr) (i : Nat) (xs : Array Expr) : Simp.SimpM EqnTelescopeResult := do
+  if h : i < info.haveInfo.size then
+    let hi := info.haveInfo[i]
+    /-
+    **Note**: `hi.decl` has no loose de-Bruijn indices, but `t`, `v`, and `b` might have.
+    We extract them from `e` to avoid unnecessary `abstract` steps.
+    -/
+    let .letE n t v b nondep := e | unreachable!
+    let x := hi.decl.toExpr
+    let val := hi.decl.value (allowNondep := true)
+    let rv ← if !used[i]! then pure { expr := val }
+      else if fixed[i]! then pure { expr := (← Simp.dsimp val) }
+      else Simp.simp val
+    let v' := if rv.expr == val then v else rv.expr.abstract xs
+    let hv? := rv.proof?.map (·.abstract xs)
+    /-
+    Given `have a := 0; ... match a with | 0 => ... | _ => ...`,
+    we want to make sure `a` is transparent when reducing the `match`.
+    -/
+    let decl := (hi.decl.setValue rv.expr).setNondep false
+    let rb ← withExistingLocalDecls [decl] <| Simp.withNewLemmas #[x] do
+      simpEqnTelescope info fixed used b (i + 1) (xs.push x)
+    let type := if fixed[i]! then
+      /- A fixed binding may occur in the result type, so close the type with the binding. -/
+      mkLet n t v' rb.type false
     else
-      trace[Elab.definition.eqns] "did not find term to split\n{MessageData.ofGoal mvarId}"
-      return none
-  go {}
+      /- The type does not depend on this binding; remove its unused bound-variable slot. -/
+      rb.type.lowerLooseBVars 1 1
+    /- A changed body may need the value of `x` to typecheck. Use `let` until `letToHave`
+    checks whether the body can still be abstracted over `x`. -/
+    let expr := mkLet n t v' rb.expr (nondep && rb.expr == b)
+    let hb? := rb.proof?.map fun h => mkLet n t v' h false
+    let hv? := hv?.map fun h => mkApp6 (mkConst ``congrArg [hi.level, info.level])
+      t type v v' (mkLambda n .default t b) h
+    let proof? := match hv?, hb? with
+      | none, hb? => hb?
+      | hv?, none => hv?
+      | some hv, some hb => some <| mkEqTransCore info.level type e
+          (mkLet n t v' b nondep) expr hv hb
+    return { expr, type, proof? }
+  else
+    /- Simplify the body. -/
+    let rb ← Simp.simp info.body
+    return {
+      expr := if rb.expr == info.body then e else rb.expr.abstract xs
+      type := info.bodyType.abstract xs
+      proof? := rb.proof?.map (·.abstract xs)
+    }
 
-partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
-  let (_, eqnTypes) ← go mvarId |>.run #[]
-  return eqnTypes
-where
-  go (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := do
-    trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
+/--
+Opens a leading telescope of mixed `let`/`have` bindings once and records its declarations,
+instantiated body, and dependencies between bindings.
 
-    -- The `let`s and `have`s at the root of the RHS are zeta-reduced only to expose a `match`.
-    let mvarId' := (← expandRHS? mvarId).getD mvarId
+`computeFixedUsed false` then computes two dependency closures: `used` starts from the body;
+`fixed` starts from its result type and every dependent `let`. A dependent let's body may rely on
+its value to typecheck even when the result type does not mention it, so that value and its
+dependencies must be restricted to definitional simplification.
+-/
+def getEqnTelescopeInfo (e : Expr) : MetaM HaveTelescopeInfo := do
+  letTelescope e fun xs body => do
+    let mut indices : Std.HashMap FVarId Nat := {}
+    for i in *...xs.size do
+      indices := indices.insert xs[i]!.fvarId! i
+    let getDeps (e : Expr) : Std.HashSet Nat :=
+      (collectFVars {} e).fvarIds.foldl (init := {}) fun deps id =>
+        match indices[id]? with
+        | none => deps
+        | some i => deps.insert i
+    let bodyType ← inferType body
+    let mut info : HaveTelescopeInfo := {
+      body, bodyType
+      level := ← getLevel bodyType
+      bodyDeps := getDeps body
+      bodyTypeDeps := getDeps bodyType
+    }
+    for i in *...xs.size do
+      let decl ← xs[i]!.fvarId!.getDecl
+      let hi : HaveInfo := {
+        decl
+        level := ← getLevel decl.type
+        typeBackDeps := getDeps decl.type
+        valueBackDeps := getDeps (decl.value (allowNondep := true))
+      }
+      info := { info with haveInfo := info.haveInfo.push hi }
+      unless decl.isNondep do
+        info := { info with bodyTypeDeps := info.bodyTypeDeps.insert i }
+    return info
 
-    if (← shouldUseSimpMatch (← mvarId'.getType')) then
-      if let some mvarId ← simpMatch? mvarId' then
-        return (← go mvarId)
+/--
+The `simp` callback for equation normalization. It handles complete binding telescopes before the
+default traversal, using `simpEqnTelescope` to preserve their nesting and sharing. Unused bindings
+are removed afterward, and `letToHave` determines which bindings can be nondependent.
+A changed telescope is revisited: removing dependent uses or restoring a `have` can make a
+previously fixed value eligible for propositional rewriting. A stable telescope returns `.done`.
+
+For a matcher, first try definitional reduction, then its congruence equations using local
+hypotheses to discharge branch conditions. Other expressions use the default traversal.
+Since matcher rewriting can use hypotheses introduced under binders, callers with
+`contextual := false` must set `wellBehavedDischarge := false` to isolate cached results by scope.
+-/
+partial def simpEqn : Simp.Simproc := fun e => do
+  if e.isLet then
+    let info ← getEqnTelescopeInfo e
+    let (fixed, used) ← info.computeFixedUsed false
+    let r ← simpEqnTelescope info fixed used e 0 #[]
+    let r := { expr := ← zetaUnused r.expr, proof? := r.proof? : Simp.Result }
+    if r.expr == e then return .done r
+    return .visit { r with expr := (← letToHave r.expr) }
+  if let some app ← matchMatcherApp? e then
+    if let some e' ← reduceRecMatcher? e then
+      return .visit { expr := e' }
+    for i in *...app.numAlts do
+      let r ← rwMatcher i e
+      if r.expr != e then return .visit r
+  return .continue
 
-    if let some mvarIds ← splitMatch? mvarId' declNames then
-      return (← mvarIds.forM go)
+/--
+The definitional counterpart of `simpEqn`, used for fixed binding values and dependent arguments
+that `simp` cannot rewrite propositionally. It opens a whole binding telescope, skips unused
+values, and definitionally simplifies the other values and body with preceding values available
+as local definitions. Changed bodies are rebuilt with `let`, and `letToHave` recovers `have`
+bindings where possible. Unused bindings are removed.
+
+Matchers are reduced only definitionally; no congruence-equation proofs are used. Changed results
+are revisited, and the returned expression is definitionally equal to the input.
+-/
+partial def dsimpEqn : Simp.DSimproc := fun e => do
+  if e.isLet then
+    let info ← getEqnTelescopeInfo e
+    let (_, used) ← info.computeFixedUsed false
+    let r ← Simp.withFreshCache <| visit info used e 0 #[]
+    let r ← zetaUnused r
+    if r == e then return .done r
+    return .visit (← letToHave r)
+  if ← isMatcherApp e then
+    if let some e' ← reduceRecMatcher? e then return .visit e'
+  return .continue
+where
+  visit (info : HaveTelescopeInfo) (used : Array Bool) (e : Expr) (i : Nat)
+      (xs : Array Expr) : Simp.SimpM Expr := do
+    if h : i < info.haveInfo.size then
+      let decl := info.haveInfo[i].decl
+      /-
+      **Note**: `decl` has no loose de-Bruijn indices, but `t`, `v`, and `b` might have.
+      We extract them from `e` to avoid unnecessary `abstract` steps.
+      -/
+      let .letE n t v b nondep := e | unreachable!
+      /- Recall that the original `decl` may be a `have`, and without `allowNondep := true`, `value` will fail. -/
+      let value := decl.value (allowNondep := true)
+      let value' ← if used[i]! then Simp.dsimp value else pure value
+      let v' := if value' == value then v else value'.abstract xs
+      /-
+      Given `have a := 0; ... match a with | 0 => ... | _ => ...`,
+      we want to make sure `a` is transparent when reducing the `match`.
+      -/
+      let decl := (decl.setValue value').setNondep false
+      let b' ← withExistingLocalDecls [decl] <| visit info used b (i+1) (xs.push decl.toExpr)
+      /- As in `simpEqnTelescope`, a changed body must be checked before retaining `have`. -/
+      return mkLet n t v' b' (nondep && b' == b)
+    else
+      return (← Simp.dsimp info.body).abstract xs
 
-    saveEqn mvarId
+/--
+Normalizes the RHS of an equality goal using `simpEqn` and `dsimpEqn`, preserving shared bindings.
+The neutral configuration disables general reductions, including zeta expansion, while `simp`
+provides traversal and congruence. Congruence proofs are built in place, so normalization adds no
+`congr_simp` theorems to the environment. Propositional RHS rewrites are lifted to the whole target;
+definitional rewrites directly replace the target.
+Returns the original goal when unchanged, which lets `splitMatch?` detect normalization progress.
+-/
+def normalizeEqn (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  let target ← mvarId.getType'
+  let some (_, lhs, rhs) := target.eq? | return mvarId
+  let ctx ← Simp.mkContext
+    (config := { Simp.neutralConfig with dsimp := true, etaStruct := .none, congrConsts := false })
+  let methods : Simp.Methods := {
+    pre := simpEqn
+    dpre := dsimpEqn
+    discharge? := ← SplitIf.mkDischarge?
+    -- Matcher rewrites can use hypotheses introduced while descending under binders.
+    wellBehavedDischarge := false
+  }
+  let (r, _) ← Simp.main rhs ctx (methods := methods)
+  if r.expr == rhs then return mvarId
+  let target' ← mkEq lhs r.expr
+  if let some proof := r.proof? then
+    let eq := target.appFn!
+    return ← mvarId.replaceTargetEq target' (← mkCongrArg eq proof)
+  else
+    mvarId.replaceTargetDefEq target'
 
 /--
-  Some of the hypotheses added by `mkEqnTypes` may not be used by the actual proof (i.e., `value` argument).
-  This method eliminates them.
+Tries eligible RHS matchers until a splitter produces branches whose RHSs all change under
+normalization. Each attempt saves the metavariable state; failure restores it and excludes that
+splitter invocation from further attempts. Returned branches are already normalized.
+-/
+partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) :
+    MetaM (Option (List MVarId)) := mvarId.withContext do
+  let target ← mvarId.getType'
+  let some (_, _, rhs) := target.eq? | return none
+  let rec go (exceptions : Std.HashSet MatchToSplit) : MetaM (Option (List MVarId)) := do
+    let some candidate ← findMatchToSplit? rhs declNames exceptions | return none
+    let saved ← saveState
+    try
+      let branches ← Split.refineMatch mvarId candidate.declName candidate.levels candidate.params candidate.discrs
+      let branches ← branches.mapM fun branch => do
+        let normalized ← normalizeEqn branch
+        if normalized == branch then
+          throwError "case split did not reduce the right-hand side"
+        return normalized
+      return some branches
+    catch ex =>
+      saved.restore
+      trace[Elab.definition.eqns] "cannot split {.ofConstName candidate.declName}\n{ex.toMessageData}"
+      go (exceptions.insert candidate)
+  go {}
 
-  Alternative solution: improve `saveEqn` and make sure it never includes unnecessary hypotheses.
-  These hypotheses are leftovers from tactics such as `splitMatch?` used in `mkEqnTypes`.
+/--
+Calculates equation statements by normalizing the initial goal, recursively splitting eligible
+matches, and saving terminal goals. Each recursive call receives an already-normalized RHS.
+The resulting statements are proved separately by `mkEqnProof`.
+The body of a definition can mention private auxiliary proofs even if the equations are public,
+so the statements are computed with private declarations visible.
+-/
+partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) :=
+  withoutExporting do
+    let (_, eqnTypes) ← go (← normalizeEqn mvarId) |>.run #[]
+    return eqnTypes
+where
+  go (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := do
+    trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
+    if let some mvarIds ← splitMatch? mvarId declNames then
+      mvarIds.forM go
+    else
+      saveEqn mvarId
+
+/--
+Removes parameters unused by both the equation's conclusion and its proof, retaining the
+transitive type dependencies of the remaining parameters.
 -/
 def removeUnusedEqnHypotheses (declType declValue : Expr) : CoreM (Expr × Expr) := do
   go declType declValue #[] {}
@@ -386,6 +666,11 @@ def mkEqns (declName : Name) (declNames : Array Name) : MetaM (Array Name) := do
     throwError "internal error: failed to generate equations for `{.ofConstName declName}`"
   return thmNames
 
+/--
+Equation-theorem provider for definitions. Recursive definitions use split equations;
+nonrecursive definitions use either split equations or one unfolding equation, according to
+`backward.eqns.nonrecursive`.
+-/
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if (← isRecursiveDefinition declName) then
     let some (.defnInfo info) := (← getEnv).find? declName |
diff --git a/src/Lean/Meta/Match/Rewrite.lean b/src/Lean/Meta/Match/Rewrite.lean
index 66b56cff539f..15057ee9ea8e 100644
--- a/src/Lean/Meta/Match/Rewrite.lean
+++ b/src/Lean/Meta/Match/Rewrite.lean
@@ -65,6 +65,8 @@ In the `onAlt` handler of a `MatcherApp.transform`, you can use this function on
 substituted matcher application with the alternative `altIdx`.
 
 If it fails, it returns a rewrite with `proof? := none` and the unchanged expression.
+If the matcher is applied to more arguments than its arity, the rewrite applies to the matcher
+application and carries the extra arguments along.
 
 "Properly substituted" here means that the discriminants have been substituted according to the
 alternative; otherwise, the rewrite might fail because some hypothesis of the congruence
@@ -72,7 +74,7 @@ equation theorem cannot be discharged by assumption or reflixivity.
 See `Lean.Meta.Tactic.FunInd.buildInductionBody` and `Lean.Elab.Tactic.Do.VCGen.Split` for examples
 of how to coerce `MatherApp.transform` into doing the substitution on the motive for you.
 -/
-def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
+partial def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
   if e.isAppOf ``PSum.casesOn || e.isAppOf ``PSigma.casesOn then
     let mut e := e
     while true do
@@ -90,6 +92,11 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
       trace[Meta.Match.debug] "Not a matcher application:{indentExpr e}"
       return { expr := e }
     let matcherDeclName := e.getAppFn.constName!
+    let some info ← getMatcherInfo? matcherDeclName | return { expr := e }
+    let args := e.getAppArgs
+    if info.arity < args.size then
+      let r ← rwMatcher altIdx (mkAppN e.getAppFn (args.extract 0 info.arity))
+      return ← r.addExtraArgs (args.extract info.arity)
     let eqns ← Match.genMatchCongrEqns matcherDeclName
     unless altIdx < eqns.size do
       trace[Meta.Match.debug] "When trying to reduce arm {altIdx}, only {eqns.size} equations for {.ofConstName matcherDeclName}"
@@ -128,7 +135,9 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
           else if hType.isEq then
             h.assumption <|> h.refl <|> throwError m!"Failed to resolve `{h}`"
           else if hType.isHEq then
-            h.assumption <|> h.hrefl <|> throwError m!"Failed to resolve `{h}`"
+            -- Splitting may provide an `Eq` hypothesis where the matcher equation requires `HEq`.
+            h.assumption <|> h.hrefl <|> (do (← h.heqOfEq).assumption) <|>
+              throwError m!"Failed to resolve `{h}`"
       let unassignedHyps ← hyps.filterM fun h => return !(← h.isAssigned)
       unless unassignedHyps.isEmpty do
         throwError m!"Not all hypotheses of `{.ofConstName eqnThm}` could be discharged: {unassignedHyps}"
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 926a29ced11c..85c076b5cdda 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -10,6 +10,7 @@ public import Lean.Meta.Match.MatcherApp.Basic
 public import Lean.Meta.Tactic.Apply
 public import Lean.Meta.Tactic.Generalize
 public import Lean.Meta.Tactic.Simp.Types
+import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.SplitIf
 
@@ -249,7 +250,10 @@ private def substDiscrEqs (mvarId : MVarId) (fvarSubst : FVarSubst) (discrEqs :
       | none => mvarId := mvarId'
   return mvarId
 
-def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := do
+private def applyMatchSplitterCore (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level)
+    (params : Array Expr) (discrs : Array Expr)
+    (generalize : MVarId → Expr → Array Expr → MetaM (Array FVarId × Array FVarId × MVarId)) :
+    MetaM (List MVarId) := do
   let some info ← getMatcherInfo? matcherDeclName | throwInternalMisuseError m!"Internal error in `split` tactic: `{matcherDeclName}` is not an auxiliary declaration used to encode `match`-expressions"
   let matchEqns ← Match.getEquationsFor matcherDeclName
   -- splitterPre does not have the correct universe elimination level, but this is fine, we only use it to compute the `motiveType`,
@@ -257,9 +261,7 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
   let splitterPre := mkAppN (mkConst matchEqns.splitterName us.toList) params
   let motiveType := (← whnfForall (← inferType splitterPre)).bindingDomain!
   trace[split.debug] "applyMatchSplitter\n{mvarId}"
-  let (discrs, mvarId) ← generalizeMatchPropDiscrs mvarId discrs
-  trace[split.debug] "after generalizeMatchPropDiscrs\n{mvarId}"
-  let (discrFVarIds, discrEqs, mvarId) ← generalizeMatchDiscrs mvarId matcherDeclName motiveType discrs
+  let (discrFVarIds, discrEqs, mvarId) ← generalize mvarId motiveType discrs
   trace[split.debug] "after generalizeMatchDiscrs\n{mvarId}"
   let mvarId ← generalizeTargetsEq mvarId motiveType (discrFVarIds.map mkFVar)
   mvarId.withContext do trace[split.debug] "discrEqs after generalizeTargetsEq: {discrEqs.map mkFVar}"
@@ -303,6 +305,40 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
         return (i+1, mvarId::mvarIds)
     return mvarIds.reverse
 
+def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) :=
+  applyMatchSplitterCore mvarId matcherDeclName us params discrs fun mvarId motiveType discrs => do
+    let (discrs, mvarId) ← generalizeMatchPropDiscrs mvarId discrs
+    trace[split.debug] "after generalizeMatchPropDiscrs\n{mvarId}"
+    generalizeMatchDiscrs mvarId matcherDeclName motiveType discrs
+
+/--
+Refines a goal into the cases of a matcher applied to `params` and `discrs`, without replacing
+matcher occurrences in the target. The arguments must be well-typed in the goal's context, but
+the matcher application need not occur in the target.
+
+Computed discriminants are linked to fresh variables by equalities. After splitting, these
+equalities specialize the goal where possible. Contradictory branches are closed; unresolved
+conditions remain as hypotheses. The target is not simplified.
+-/
+def refineMatch (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level)
+    (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := mvarId.withContext do
+  let mvarIds ← applyMatchSplitterCore mvarId matcherDeclName us params discrs fun mvarId motiveType discrs =>
+    mvarId.withContext do
+      if ← discrs.allM fun discr => do
+        unless discr.isFVar do return false
+        return !(← discr.fvarId!.getDecl).isLet
+      then
+        return (discrs.map (·.fvarId!), #[], mvarId)
+      let mvarId ← generalizeTargetsEq mvarId motiveType discrs
+      let (discrFVarIds, mvarId) ← mvarId.introN discrs.size
+      let (discrEqs, mvarId) ← mvarId.introN discrs.size
+      return (discrFVarIds, discrEqs, mvarId)
+  /- Substitution can expose contradictions in the generalized discriminant equalities
+     (e.g. `0 = n.succ`) or overlap exclusions (e.g. `0 = 0 → False`). These hypotheses
+     are already in the local context, so `Cases.unifyEqs?` does not process them. -/
+  mvarIds.filterM fun mvarId => do
+    return !(← mvarId.contradictionCore { useDecide := false, emptyType := false, genDiseq := true })
+
 def mkDiscrGenErrorMsg (e : Expr) : MessageData :=
   m!"`split` tactic failed to generalize discriminant(s) at{indentExpr e}\nresulting expression was not type correct\npossible solution: generalize discriminant(s) manually before using `split`"
 
diff --git a/tests/elab/1074a.lean b/tests/elab/1074a.lean
index 229bd10201a9..336b7a79a7ef 100644
--- a/tests/elab/1074a.lean
+++ b/tests/elab/1074a.lean
@@ -1,3 +1,5 @@
+/-! Equation generation for recursive elimination of proofs. -/
+
 inductive Term : Type
 | id2: Term -> Term -> Term
 
@@ -19,10 +21,7 @@ def Brx.interp_nil (H: Brx a): H.interp = H.interp
   }
 
 /--
-info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (n.id2 z)) :
-  H_2.interp =
-    match ⋯ with
-    | ⋯ => Hz.interp
+info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (n.id2 z)) : H_2.interp = ⋯.interp
 -/
 #guard_msgs in
 #check Brx.interp.eq_1
diff --git a/tests/elab/5667.lean b/tests/elab/5667.lean
index 78cbc1663cbf..71807490f311 100644
--- a/tests/elab/5667.lean
+++ b/tests/elab/5667.lean
@@ -1,3 +1,5 @@
+/-! Equation generation for structural and mutual recursion with multiple discriminants (#5667). -/
+
 inductive Expr where
   | const (i : BitVec 32)
   | op (op : Unit) (e1 : Expr)
@@ -25,10 +27,10 @@ info: optimize.eq_def (x✝ : Expr) :
 /--
 info: equations:
 @[backward_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
+theorem optimize.eq_2 : ∀ (e1 : Expr) (bop_1 : Unit) (i : BitVec 32),
+  optimize e1 = Expr.const i → optimize (Expr.op bop_1 e1) = Expr.op bop_1 (Expr.const 0)
+theorem optimize.eq_3 : ∀ (e1 : Expr) (bop_1 : Unit),
+  (∀ (i : BitVec 32), optimize e1 = Expr.const i → False) → optimize (Expr.op bop_1 e1) = Expr.const 0
 -/
 #guard_msgs in
 #print equations optimize
diff --git a/tests/elab/ack.lean b/tests/elab/ack.lean
index 63bbd96477e8..2640908b487c 100644
--- a/tests/elab/ack.lean
+++ b/tests/elab/ack.lean
@@ -16,8 +16,8 @@ trace: [simp] Diagnostics
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---
 trace: [diag] Diagnostics
-  [kernel] unfolded declarations (max: 86, num: 1):
-    [kernel] OfNat.ofNat ↦ 86
+  [kernel] unfolded declarations (max: 91, num: 1):
+    [kernel] OfNat.ofNat ↦ 91
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
diff --git a/tests/elab/byteSliceIssue.lean b/tests/elab/byteSliceIssue.lean
index 4d2388365857..974f2899b926 100644
--- a/tests/elab/byteSliceIssue.lean
+++ b/tests/elab/byteSliceIssue.lean
@@ -1,3 +1,5 @@
+/-! Equation generation for a well-founded monadic byte-slice loop. -/
+
 def Nat.Up (ub a i : Nat) := i < a ∧ i < ub
 
 theorem Nat.Up.next {ub i} (h : i < ub) : Up ub (i+1) i := ⟨Nat.lt_succ_self _, h⟩
diff --git a/tests/elab/byteSliceIssue.lean.out.expected b/tests/elab/byteSliceIssue.lean.out.expected
index 5566ffd9435e..b05a0aae73fd 100644
--- a/tests/elab/byteSliceIssue.lean.out.expected
+++ b/tests/elab/byteSliceIssue.lean.out.expected
@@ -5,7 +5,5 @@
       let __do_lift ← f (arr.get! i) b
       match __do_lift with
         | ForInStep.done b => pure b
-        | ForInStep.yield b =>
-          have this := ⋯;
-          forIn.loop f arr off _end (i + 1) b
+        | ForInStep.yield b => forIn.loop f arr off _end (i + 1) b
     else pure b
diff --git a/tests/elab/eqns_have_invariant.lean b/tests/elab/eqns_have_invariant.lean
new file mode 100644
index 000000000000..6984488ec4ef
--- /dev/null
+++ b/tests/elab/eqns_have_invariant.lean
@@ -0,0 +1,115 @@
+module
+
+/-! Simplifying generated equations must preserve the `have` abstraction invariant (#16122). -/
+
+def dependentMatcher : Nat :=
+  have a := 0
+  have q : { n : Nat // n = a } :=
+    match a with
+    | 0 => ⟨0, rfl⟩
+    | n+1 => ⟨n+1, rfl⟩
+  q.val
+
+example (n : Nat) : dependentMatcher = 0 := by
+  simp -zeta only [dependentMatcher.eq_1, ← Nat.sub_self n]
+  simp -zeta only [Nat.sub_self]
+  rfl
+
+opaque usesProof (n : Nat) (h : n = 0) : Nat
+
+-- The dependency occurs inside a proof argument, while the result type remains `Nat`.
+def namedMatcher : Nat :=
+  have a := 0
+  match h : a with
+  | 0 => usesProof a h
+  | _+1 => 0
+
+example (n : Nat) : namedMatcher = usesProof 0 rfl := by
+  simp -zeta only [namedMatcher.eq_1, ← Nat.sub_self n] <;>
+    simp -zeta only [Nat.sub_self] <;> rfl
+
+-- The dependent `let` makes equation normalization use `dsimp` for `n`'s value.
+set_option cleanup.letToHave false in
+def fixedHave : Nat :=
+  have n :=
+    have a := 0
+    have q : {n : Nat // n = a} := match a with
+      | 0 => ⟨0, rfl⟩
+      | n+1 => ⟨n+1, rfl⟩
+    q.val
+  let v : Fin (n+1) := ⟨0, Nat.zero_lt_succ n⟩
+  n + v.val
+
+example (m : Nat) : fixedHave = 0 := by
+  simp -zeta only [fixedHave.eq_1, ← Nat.sub_self m]
+  simp -zeta only [Nat.sub_self]
+  rfl
+
+/- The second and fourth alternatives are impossible because `a = 0`. Equation generation
+must eliminate them, including the contradiction in the second alternative's overlap condition. -/
+def depMatch (x : Nat) : Nat :=
+  have a := 0
+  have q : { n : Nat // n ≤ x + a } :=
+    match x, a with
+    | 0, 0 => ⟨0, by simp⟩
+    | 0, a => ⟨0, by simp⟩
+    | x+1, 0 => ⟨x, by simp⟩
+    | x+1, a+1 => ⟨x+a, by lia⟩
+  q.val
+
+/--
+info: depMatch.eq_1 :
+  depMatch 0 =
+    let a := 0;
+    have q := ⟨0, depMatch._proof_1⟩;
+    q.val
+-/
+#guard_msgs in #check depMatch.eq_1
+
+/--
+info: depMatch.eq_2 (x_3 : Nat) :
+  depMatch x_3.succ =
+    let a := 0;
+    have q := ⟨x_3, ⋯⟩;
+    q.val
+-/
+#guard_msgs in #check depMatch.eq_2
+
+example : depMatch 0 = 0 := depMatch.eq_1
+example (n : Nat) : depMatch (n+1) = n := depMatch.eq_2 n
+
+/-- error: Unknown identifier `depMatch.eq_3` -/
+#guard_msgs in #check depMatch.eq_3
+
+-- Constant discriminants must eliminate impossible alternatives without any local bindings.
+def constantDiscr (x : Nat) : Nat :=
+  match x, (0 : Nat) with
+  | 0, 0 => 0
+  | 0, _ => 0
+  | n+1, 0 => n
+  | n+1, k+1 => n+k
+
+example : constantDiscr 0 = 0 := constantDiscr.eq_1
+example (n : Nat) : constantDiscr (n+1) = n := constantDiscr.eq_2 n
+
+/-- error: Unknown identifier `constantDiscr.eq_3` -/
+#guard_msgs in #check constantDiscr.eq_3
+
+-- The impossible overlap condition quantifies over the payload of `some`.
+def constructorDiscr (x : Nat) : Nat :=
+  match x, (some 0 : Option Nat) with
+  | 0, some n => n
+  | 0, _ => 0
+  | n+1, _ => n
+
+example : constructorDiscr 0 = 0 := constructorDiscr.eq_1
+example (n : Nat) : constructorDiscr (n+1) = n := constructorDiscr.eq_2 n
+
+/-- info: constructorDiscr.eq_1 : constructorDiscr 0 = 0 -/
+#guard_msgs in #check constructorDiscr.eq_1
+
+/-- info: constructorDiscr.eq_2 (n : Nat) : constructorDiscr n.succ = n -/
+#guard_msgs in #check constructorDiscr.eq_2
+
+/-- error: Unknown identifier `constructorDiscr.eq_3` -/
+#guard_msgs in #check constructorDiscr.eq_3
diff --git a/tests/elab/eqns_issues.lean b/tests/elab/eqns_issues.lean
new file mode 100644
index 000000000000..33ed20d629dc
--- /dev/null
+++ b/tests/elab/eqns_issues.lean
@@ -0,0 +1,362 @@
+module
+
+import Lean
+
+/-!
+Regression tests for equation lemmas preserving shared values and valid nested binding scopes
+while splitting matches (#16122).
+-/
+@[expose] public section
+
+set_option linter.unusedVariables false
+
+-- 1. A `have` inside the value of a `have` whose `match` is split.
+def innerHave (x : Nat) : Nat :=
+  have a :=
+    have b := x * x + x
+    match x with
+    | 0 => b
+    | n + 1 => b + b + n
+  a + a
+
+/--
+info: innerHave.eq_1 :
+  innerHave 0 =
+    have a :=
+      have b := 0 * 0 + 0;
+      b;
+    a + a
+-/
+#guard_msgs in #check innerHave.eq_1
+
+/--
+info: innerHave.eq_2 (n : Nat) :
+  innerHave n.succ =
+    have a :=
+      have b := n.succ * n.succ + n.succ;
+      b + b + n;
+    a + a
+-/
+#guard_msgs in #check innerHave.eq_2
+
+-- 2. The same, with a non-variable discriminant `x + 1`.
+def mixedUnderHave (x : Nat) : Nat :=
+  have a :=
+    have b := x * x
+    match x, x + 1 with
+    | 0, _ => b
+    | n + 1, m => b + b + n + m
+  a + a
+
+/--
+info: mixedUnderHave.eq_1 :
+  mixedUnderHave 0 =
+    have a :=
+      have b := 0 * 0;
+      b;
+    a + a
+-/
+#guard_msgs in #check mixedUnderHave.eq_1
+
+/--
+info: mixedUnderHave.eq_2 (n : Nat) :
+  mixedUnderHave n.succ =
+    have a :=
+      have b := n.succ * n.succ;
+      b + b + n + (n.succ + 1);
+    a + a
+-/
+#guard_msgs in #check mixedUnderHave.eq_2
+
+-- 3. A `have` that is a discriminant, with a value that depends on the split variable.
+def discrDep (x : Nat) : Nat :=
+  have k := x * x + x
+  match x, k with
+  | 0, _ => 1
+  | n + 1, m => n + m + m
+
+/-- info: discrDep.eq_1 : discrDep 0 = 1 -/
+#guard_msgs in #check discrDep.eq_1
+
+/--
+info: discrDep.eq_2 (n : Nat) :
+  discrDep n.succ =
+    have k := n.succ * n.succ + n.succ;
+    n + k + k
+-/
+#guard_msgs in #check discrDep.eq_2
+
+-- 4. With `cleanup.letToHave false`, the `have` stays a `have`.
+set_option cleanup.letToHave false in
+def noCleanup (x : Nat) : Nat :=
+  have y := x + 1
+  y + y
+
+/--
+info: noCleanup.eq_1 (x : Nat) :
+  noCleanup x =
+    have y := x + 1;
+    y + y
+-/
+#guard_msgs in #check noCleanup.eq_1
+
+-- An unchanged telescope does not need another `letToHave` pass.
+set_option cleanup.letToHave false in
+def noCleanupLet (x : Nat) : Nat :=
+  let y := x + 1
+  y + y
+
+/--
+info: noCleanupLet.eq_1 (x : Nat) :
+  noCleanupLet x =
+    let y := x + 1;
+    y + y
+-/
+#guard_msgs in #check noCleanupLet.eq_1
+
+-- When normalization changes the body, an original nondependent `let` becomes a `have`.
+set_option cleanup.letToHave false in
+def noCleanupLetMatch (x : Nat) : Nat :=
+  let y := x + 1
+  match x with
+  | 0 => y + y
+  | n + 1 => y + y + n
+
+/--
+info: noCleanupLetMatch.eq_1 :
+  noCleanupLetMatch 0 =
+    have y := 0 + 1;
+    y + y
+-/
+#guard_msgs in #check noCleanupLetMatch.eq_1
+
+-- A binding whose body needs its value remains a `let`.
+set_option cleanup.letToHave false in
+def noCleanupDependent (x : Nat) : Fin 5 :=
+  let n := 4
+  match x with
+  | 0 => (⟨n, by decide⟩ : Fin (n + 1))
+  | _ + 1 => 0
+
+/--
+info: noCleanupDependent.eq_1 :
+  noCleanupDependent 0 =
+    let n := 4;
+    ⟨n, noCleanupDependent._proof_1⟩
+-/
+#guard_msgs in #check noCleanupDependent.eq_1
+
+-- The computed discriminant remains shared even when it also occurs in a branch hypothesis.
+def computedPremise (f : Nat → Nat) (x : Nat) : Nat :=
+  have k := f x
+  match x, k with
+  | 0, _ => 1
+  | _, 0 => 2
+  | n + 1, m + 1 => n + k + k + m
+
+/--
+info: equations:
+@[backward_defeq] theorem computedPremise.eq_1 : ∀ (f : Nat → Nat), computedPremise f 0 = 1
+theorem computedPremise.eq_2 : ∀ (f : Nat → Nat) (x_1 : Nat), (x_1 = 0 → False) → f x_1 = 0 → computedPremise f x_1 = 2
+theorem computedPremise.eq_3 : ∀ (f : Nat → Nat) (n m : Nat),
+  f n.succ = m.succ →
+    computedPremise f n.succ =
+      have k := f n.succ;
+      n + k + k + m
+-/
+#guard_msgs in #print equations computedPremise
+
+-- Each inner `y` belongs to its own binding value, including the value without a match.
+def nestedScopes (x : Nat) : Nat :=
+  have a :=
+    have y := x + 1
+    match x with
+    | 0 => y + y
+    | n + 1 => y + y + n
+  have b :=
+    have y := x * x
+    a + y + y
+  a + b + b
+
+/--
+info: nestedScopes.eq_2 (n : Nat) :
+  nestedScopes n.succ =
+    have a :=
+      have y := n.succ + 1;
+      y + y + n;
+    have b :=
+      have y := n.succ * n.succ;
+      a + y + y;
+    a + b + b
+-/
+#guard_msgs in #check nestedScopes.eq_2
+
+-- A match in a dead binding must not produce extra equations.
+def unusedValue (x : Nat) : Nat :=
+  have y := match x with
+    | 0 => 1
+    | _ + 1 => 2
+  7
+
+/--
+info: equations:
+@[backward_defeq] theorem unusedValue.eq_1 : ∀ (x : Nat), unusedValue x = 7
+-/
+#guard_msgs in #print equations unusedValue
+
+-- Matches capturing a lambda parameter stay inside the lambda; independent matches can split.
+def lambdaCapture (x : Nat) (ys : List Nat) : List Nat :=
+  ys.map fun y => match x with
+    | 0 => y
+    | n + 1 => n + y
+
+def lambdaIndependent (x : Nat) (ys : List Nat) : List Nat :=
+  ys.map fun _ => match x with
+    | 0 => 7
+    | n + 1 => n
+
+open Lean Meta in
+run_meta do
+  for (decl, count) in #[(``lambdaCapture, 1), (``lambdaIndependent, 2)] do
+    let some eqns ← getEqnsFor? decl | throwError "missing equations for {decl}"
+    unless eqns.size == count do
+      throwError "expected {count} equations for {decl}, got {eqns.size}"
+
+-- A value fixed by the result type still reduces matches through local constructor aliases.
+set_option cleanup.letToHave false in
+def fixedValue (x : Nat) : Fin (x + 1) :=
+  let n :=
+    have a := some x
+    have b := a
+    match b with
+    | none => 0
+    | some k => k
+  (⟨0, Nat.zero_lt_succ n⟩ : Fin (n + 1))
+
+open Lean Meta in
+run_meta do
+  let some eqns ← getEqnsFor? ``fixedValue | throwError "missing equations"
+  unless eqns.size == 1 do throwError "expected one equation, got {eqns.size}"
+  forallTelescope (← getConstInfo eqns[0]!).type fun xs body => do
+    let some (_, _, .letE _ _ value _ true) := body.eq?
+      | throwError "expected a nondependent binding"
+    unless value == xs[0]! do throwError "constructor aliases in the fixed value did not reduce"
+
+example (x : Nat) : (fixedValue x).val = 0 := by
+  rw [fixedValue.eq_1]
+
+-- Once a branch drops dependent uses, its remaining shared value can simplify propositionally.
+set_option cleanup.letToHave false in
+def branchDeadValueBarrier (x : Nat) : Nat :=
+  have a := match x with | 5 => 1 | _ => 2
+  let n := a + 1
+  have v : Fin n := ⟨a, Nat.lt_succ_self a⟩
+  match x with
+  | 5 => v.val
+  | _ => a + a
+
+open Lean Meta in
+run_meta do
+  let some eqns ← getEqnsFor? ``branchDeadValueBarrier | throwError "missing equations"
+  unless eqns.size == 2 do throwError "expected two equations, got {eqns.size}"
+  for eqn in eqns do
+    discard <| getConstInfo eqn
+  forallTelescope (← getConstInfo eqns[1]!).type fun _ body => do
+    let some (_, _, .letE _ _ value _ true) := body.eq?
+      | throwError "shared value was lost"
+    unless ← isDefEq value (mkNatLit 2) do throwError "branch value did not simplify"
+
+-- Expanding this value before finding the match would duplicate the chain exponentially.
+def nestedChain (x : Nat) : Nat :=
+  have a :=
+    have v0 := x * x + x
+    have v1 := v0 + v0
+    have v2 := v1 + v1
+    have v3 := v2 + v2
+    have v4 := v3 + v3
+    have v5 := v4 + v4
+    have v6 := v5 + v5
+    have v7 := v6 + v6
+    have v8 := v7 + v7
+    have v9 := v8 + v8
+    have v10 := v9 + v9
+    have v11 := v10 + v10
+    have v12 := v11 + v11
+    have v13 := v12 + v12
+    have v14 := v13 + v13
+    have v15 := v14 + v14
+    have v16 := v15 + v15
+    have v17 := v16 + v16
+    have v18 := v17 + v17
+    have v19 := v18 + v18
+    have v20 := v19 + v19
+    have v21 := v20 + v20
+    have v22 := v21 + v21
+    have v23 := v22 + v22
+    have v24 := v23 + v23
+    match x with
+    | 0 => v24
+    | n + 1 => v24 + v24 + n
+  a + a
+
+open Lean Meta in
+run_meta do
+  let some eqns ← getEqnsFor? ``nestedChain | throwError "missing equations"
+  unless eqns.size == 2 do throwError "expected two equations, got {eqns.size}"
+  for eqn in eqns do
+    let type := (← getConstInfo eqn).type
+    forallTelescope type fun _ body => do
+      let some (_, _, rhs) := body.eq? | throwError "expected an equation"
+      let .letE `a _ value _ true := rhs | throwError "outer have was lost"
+      let mut value := value
+      let mut count : Nat := 0
+      while let .letE _ _ _ body true := value do
+        count := count + 1
+        value := body
+      unless count == 25 do throwError "expected 25 nested haves, got {count}"
+      unless (← rhs.numObjs) < 1000 do throwError "equation exceeded the size bound"
+
+open Lean Meta in
+run_meta do
+  for (decl, nondep) in #[(``noCleanup, true), (``noCleanupLet, false),
+      (``noCleanupDependent, false)] do
+    let some eqns ← getEqnsFor? decl | throwError "missing equations for {decl}"
+    forallTelescope (← getConstInfo eqns[0]!).type fun _ body => do
+      let some (_, _, .letE _ _ _ _ actual) := body.eq?
+        | throwError "binding was lost in {decl}"
+      unless actual == nondep do throwError "binding kind changed in {decl}"
+
+/--
+info: nestedChain.eq_2 (n : Nat) :
+  nestedChain n.succ =
+    have a :=
+      have v0 := n.succ * n.succ + n.succ;
+      have v1 := v0 + v0;
+      have v2 := v1 + v1;
+      have v3 := v2 + v2;
+      have v4 := v3 + v3;
+      have v5 := v4 + v4;
+      have v6 := v5 + v5;
+      have v7 := v6 + v6;
+      have v8 := v7 + v7;
+      have v9 := v8 + v8;
+      have v10 := v9 + v9;
+      have v11 := v10 + v10;
+      have v12 := v11 + v11;
+      have v13 := v12 + v12;
+      have v14 := v13 + v13;
+      have v15 := v14 + v14;
+      have v16 := v15 + v15;
+      have v17 := v16 + v16;
+      have v18 := v17 + v17;
+      have v19 := v18 + v18;
+      have v20 := v19 + v19;
+      have v21 := v20 + v20;
+      have v22 := v21 + v21;
+      have v23 := v22 + v22;
+      have v24 := v23 + v23;
+      v24 + v24 + n;
+    a + a
+-/
+#guard_msgs in
+#check nestedChain.eq_2
diff --git a/tests/elab/eqns_keep_have.lean b/tests/elab/eqns_keep_have.lean
index a317097583a4..8cc24f3cfc63 100644
--- a/tests/elab/eqns_keep_have.lean
+++ b/tests/elab/eqns_keep_have.lean
@@ -1,7 +1,12 @@
+module
+
 /-!
-Tests that equation lemmas zeta-reduce the `have`s at the root of the right-hand side only when
-this exposes a `match` to split, so that `vcgen +jp [f]` sees the join points of `f` (#16122).
+Tests that equation lemmas keep the `have`s at the root of the right-hand side, also above a split
+`match`, so that `vcgen +jp [f]` sees the join points of `f` (#16122).
 -/
+@[expose] public section
+
+set_option linter.unusedVariables false
 
 def f (x : Nat) : Nat :=
   have y := x + 1
@@ -33,16 +38,204 @@ info: prog2.eq_1 (b : Nat → Bool) :
 -/
 #guard_msgs in #check prog2.eq_1
 
--- The `have` is zeta-reduced to split the `match`.
+-- The `have` stays above the split `match`, and is dropped where it is unused.
 def h (x : Option Nat) : Nat :=
   have y := 1
+  have z := y + 1
   match x with
-  | some a => a + y
+  | some v => v + z + z
   | none => y
 
-/-- info: h.eq_1 (a : Nat) : h (some a) = a + 1 -/
+/--
+info: h.eq_1 (v : Nat) :
+  h (some v) =
+    have y := 1;
+    have z := y + 1;
+    v + z + z
+-/
 #guard_msgs in #check h.eq_1
 
+/--
+info: h.eq_2 :
+  h none =
+    have y := 1;
+    y
+-/
+#guard_msgs in #check h.eq_2
+
+-- The join point of `do` stays above the split `match` and the `if`.
+def rootMatch (x : Nat) (b : Bool) : StateM Nat Nat := do
+  let mut y := 0
+  match x with
+  | 0 => y := 1
+  | _ + 1 => if b then y := 2 else y := 3
+  let s ← get
+  return y + s
+
+/--
+info: rootMatch.eq_2 (b : Bool) (n : Nat) :
+  rootMatch n.succ b =
+    have __do_jp := fun __r y => do
+      let s ← get
+      pure (y + s);
+    if b = true then
+      have y := 2;
+      __do_jp () y
+    else
+      have y := 3;
+      __do_jp () y
+-/
+#guard_msgs in #check rootMatch.eq_2
+
+-- Nested join points.
+def seqIfs (x : Nat) (b c : Bool) : StateM Nat Nat := do
+  let mut y := 0
+  match x with
+  | 0 => y := 1
+  | _ + 1 => if b then y := 2 else y := 3
+  if c then y := y + 1
+  let s ← get
+  return y + s
+
+/--
+info: seqIfs.eq_2 (b c : Bool) (n : Nat) :
+  seqIfs n.succ b c =
+    have __do_jp := fun __r y =>
+      have __do_jp := fun __r y => do
+        let s ← get
+        pure (y + s);
+      if c = true then
+        have y := y + 1;
+        __do_jp () y
+      else __do_jp () y;
+    if b = true then
+      have y := 2;
+      __do_jp () y
+    else
+      have y := 3;
+      __do_jp () y
+-/
+#guard_msgs in #check seqIfs.eq_2
+
+-- Zeta-reducing chained `have`s would be exponential.
+def chain (f : Nat → Nat) (x : Option Nat) : Nat :=
+  have p := f 0
+  have q := p + p
+  have r := q + q
+  match x with
+  | some a => r + a
+  | none => 0
+
+/--
+info: chain.eq_1 (f : Nat → Nat) (a : Nat) :
+  chain f (some a) =
+    have p := f 0;
+    have q := p + p;
+    have r := q + q;
+    r + a
+-/
+#guard_msgs in #check chain.eq_1
+
+-- The value of the `have` depends on the discriminant.
+def dep (x : Nat) : Nat :=
+  have y := x + 1
+  match x with
+  | 0 => y
+  | n + 1 => n + y
+
+/--
+info: dep.eq_2 (n : Nat) :
+  dep n.succ =
+    have y := n.succ + 1;
+    n + y
+-/
+#guard_msgs in #check dep.eq_2
+
+-- A dependent `let` stays a `let`.
+def depLet (x : Nat) : Fin 5 :=
+  let n := 4
+  match x with
+  | 0 => (⟨n, by decide⟩ : Fin (n + 1))
+  | _ + 1 => 0
+
+/--
+info: depLet.eq_1 :
+  depLet 0 =
+    let n := 4;
+    ⟨n, depLet._proof_1⟩
+-/
+#guard_msgs in #check depLet.eq_1
+
+-- The `have` is zeta-reduced if it is a discriminant.
+def discr (x : Nat) : Nat :=
+  have y := x
+  match y with
+  | 0 => 1
+  | n + 1 => n
+
+/-- info: discr.eq_2 (n : Nat) : discr n.succ = n -/
+#guard_msgs in #check discr.eq_2
+
+def discr2 (x : Nat) : Nat :=
+  have k := x + 2
+  match x, k with
+  | 0, _ => 1
+  | n + 1, m => n + m
+
+/--
+info: discr2.eq_2 (n : Nat) :
+  discr2 n.succ =
+    have k := n.succ + 2;
+    n + k
+-/
+#guard_msgs in #check discr2.eq_2
+
+-- The `match` in the value of the `have` is split, and the `have` is kept.
+def inValue (x : Option Nat) : Nat :=
+  have y := match x with
+    | some a => a
+    | none => 0
+  y + 1
+
+/--
+info: inValue.eq_1 (a : Nat) :
+  inValue (some a) =
+    have y := a;
+    y + 1
+-/
+#guard_msgs in #check inValue.eq_1
+
+-- Structural and well-founded recursion.
+def srec (f : Nat → Nat) (n : Nat) : Nat :=
+  have v := f n
+  match n with
+  | 0 => v + v
+  | m + 1 => srec f m + v + v
+
+/--
+info: srec.eq_2 (f : Nat → Nat) (n_1 : Nat) :
+  srec f n_1.succ =
+    have v := f n_1.succ;
+    srec f n_1 + v + v
+-/
+#guard_msgs in #check srec.eq_2
+
+def wrec (f : Nat → Nat) (n : Nat) : Nat :=
+  have v := f n
+  match n with
+  | 0 => v + v
+  | m + 1 => wrec f (m / 2) + v + v
+termination_by n
+decreasing_by grind
+
+/--
+info: wrec.eq_2 (f : Nat → Nat) (n_1 : Nat) :
+  wrec f n_1.succ =
+    have v := f n_1.succ;
+    wrec f (n_1 / 2) + v + v
+-/
+#guard_msgs in #check wrec.eq_2
+
 -- A `have` in a `match` alternative.
 def k (x : Option Nat) : Nat :=
   match x with
@@ -83,3 +276,433 @@ info: w.eq_1 (n : Nat) :
       y + y
 -/
 #guard_msgs in #check w.eq_1
+
+-- A `have` with a constructor value is inlined as a discriminant, so the `match` reduces.
+def ctorLet (x : Nat) : Nat :=
+  have y := some x
+  match y with
+  | none => 42
+  | some n =>
+    match n with
+    | 0 => 0
+    | m + 1 => m
+
+/-- info: ctorLet.eq_2 (n : Nat) : ctorLet n.succ = n -/
+#guard_msgs in #check ctorLet.eq_2
+
+-- The value of the `have` has the `match` below a nested `have`.
+def nestedLet (x : Nat) : Nat :=
+  have y :=
+    have z := x
+    match z with
+    | 0 => 42
+    | n + 1 => n
+  y
+
+/--
+info: nestedLet.eq_2 (n : Nat) :
+  nestedLet n.succ =
+    have y := n;
+    y
+-/
+#guard_msgs in #check nestedLet.eq_2
+
+-- The constructor value is reached through an alias.
+def ctorAlias (x : Nat) : Nat :=
+  have y := some x
+  have z := y
+  match z with
+  | none => 42
+  | some n =>
+    match n with
+    | 0 => 0
+    | m + 1 => m
+
+/-- info: ctorAlias.eq_1 : ctorAlias 0 = 0 -/
+#guard_msgs in #check ctorAlias.eq_1
+
+
+/-- info: ctorAlias.eq_2 (n : Nat) : ctorAlias n.succ = n -/
+#guard_msgs in #check ctorAlias.eq_2
+
+def g (n : Nat) : Option Nat := if n = 0 then none else some n
+
+-- An unused `have` is dropped, also above a `match` that is not split.
+def unusedRoot (x : Nat) : Nat :=
+  have k := x + 1
+  match g x with
+  | some a => a
+  | none => 0
+
+/--
+info: unusedRoot.eq_1 (x : Nat) :
+  unusedRoot x =
+    match g x with
+    | some a => a
+    | none => 0
+-/
+#guard_msgs in #check unusedRoot.eq_1
+
+-- Also inside a split branch.
+def unusedBranch (x : Nat) (y : Option Nat) : Nat :=
+  match y with
+  | some b =>
+    have k := b + 1
+    match g x with
+    | some a => a
+    | none => 0
+  | none => 0
+
+/--
+info: unusedBranch.eq_1 (x a : Nat) :
+  unusedBranch x (some a) =
+    match g x with
+    | some a => a
+    | none => 0
+-/
+#guard_msgs in #check unusedBranch.eq_1
+
+-- Nested matches in a binding value are split while its sharing and scope are preserved.
+def nestedValueCases (x : Nat) : Nat :=
+  have a :=
+    have b := x + 1
+    match x with
+    | 0 => b
+    | n + 1 => b + (match n with | 0 => 10 | m + 1 => m)
+  have c := a + a
+  match x with
+  | 0 => c
+  | n + 1 => c + n
+
+
+/--
+info: nestedValueCases.eq_1 :
+  nestedValueCases 0 =
+    have a :=
+      have b := 0 + 1;
+      b;
+    have c := a + a;
+    c
+-/
+#guard_msgs in #check nestedValueCases.eq_1
+
+/--
+info: nestedValueCases.eq_3 (n_1 : Nat) :
+  nestedValueCases n_1.succ.succ =
+    have a :=
+      have b := n_1.succ.succ + 1;
+      b + n_1;
+    have c := a + a;
+    c + n_1.succ
+-/
+#guard_msgs in #check nestedValueCases.eq_3
+
+-- Shared dependencies reach the nested match without expanding intermediate values.
+def nestedValueChain (x : Nat) : Nat :=
+  have a :=
+    have b := x + 1
+    match x with
+    | 0 => b
+    | n + 1 => b + (match n with | 0 => 10 | m + 1 => m)
+  have c := a + a
+  have d := c + c
+  match x with
+  | 0 => d
+  | n + 1 => d + n
+
+/--
+info: nestedValueChain.eq_3 (n_1 : Nat) :
+  nestedValueChain n_1.succ.succ =
+    have a :=
+      have b := n_1.succ.succ + 1;
+      b + n_1;
+    have c := a + a;
+    have d := c + c;
+    d + n_1.succ
+-/
+#guard_msgs in #check nestedValueChain.eq_3
+
+-- Literal patterns overlap: the `match` in the value is simplified with the hypotheses of the split.
+def valNatLit (x : Nat) : Nat :=
+  have y := match x with
+    | 5 => 1
+    | 7 => 3
+    | _ => 2
+  y + y
+/--
+info: equations:
+@[backward_defeq] theorem valNatLit.eq_1 : valNatLit 5 =
+  have y := 1;
+  y + y
+@[backward_defeq] theorem valNatLit.eq_2 : valNatLit 7 =
+  have y := 3;
+  y + y
+theorem valNatLit.eq_3 : ∀ (x : Nat),
+  (x = 5 → False) →
+    (x = 7 → False) →
+      valNatLit x =
+        have y := 2;
+        y + y
+-/
+#guard_msgs in #print equations valNatLit
+
+-- The `match`es in the values are split in the order in which they occur in the right-hand side.
+def twoVals (x z : Nat) : Nat :=
+  have a := match x with
+    | 0 => 1
+    | _ + 1 => 2
+  have b := match z with
+    | 0 => a
+    | _ + 1 => a + 1
+  b + b
+/--
+info: equations:
+@[backward_defeq] theorem twoVals.eq_1 : twoVals 0 0 =
+  have a := 1;
+  have b := a;
+  b + b
+@[backward_defeq] theorem twoVals.eq_2 : ∀ (n : Nat),
+  twoVals 0 n.succ =
+    have a := 1;
+    have b := a + 1;
+    b + b
+@[backward_defeq] theorem twoVals.eq_3 : ∀ (n : Nat),
+  twoVals n.succ 0 =
+    have a := 2;
+    have b := a;
+    b + b
+@[backward_defeq] theorem twoVals.eq_4 : ∀ (n n_1 : Nat),
+  twoVals n.succ n_1.succ =
+    have a := 2;
+    have b := a + 1;
+    b + b
+-/
+#guard_msgs in #print equations twoVals
+
+-- Overlapping patterns in a value.
+def valOverlap (x y : Nat) : Nat :=
+  have r := match x, y with
+    | 0, _ => 1
+    | _, 0 => 2
+    | n + 1, m + 1 => n + m
+  r + r
+/--
+info: equations:
+@[backward_defeq] theorem valOverlap.eq_1 : ∀ (y : Nat),
+  valOverlap 0 y =
+    have r := 1;
+    r + r
+theorem valOverlap.eq_2 : ∀ (x : Nat),
+  (x = 0 → False) →
+    valOverlap x 0 =
+      have r := 2;
+      r + r
+@[backward_defeq] theorem valOverlap.eq_3 : ∀ (n m : Nat),
+  valOverlap n.succ m.succ =
+    have r := n + m;
+    r + r
+-/
+#guard_msgs in #print equations valOverlap
+
+-- A `match` in a value whose discriminants are not all variables.
+def valMixedDiscr (x : Nat) : Nat :=
+  have y := match x, x + 1 with
+    | 0, _ => 1
+    | n + 1, m => n + m
+  y + y
+/--
+info: equations:
+@[backward_defeq] theorem valMixedDiscr.eq_1 : valMixedDiscr 0 =
+  have y := 1;
+  y + y
+@[backward_defeq] theorem valMixedDiscr.eq_2 : ∀ (n : Nat),
+  valMixedDiscr n.succ =
+    have y := n + (n.succ + 1);
+    y + y
+-/
+#guard_msgs in #print equations valMixedDiscr
+
+-- The same variable is matched in a value and in the right-hand side.
+def valAndTarget (x : Nat) : Nat :=
+  have y := match x with
+    | 0 => 1
+    | _ + 1 => 2
+  match x with
+  | 0 => y + y
+  | n + 1 => y + n
+/--
+info: equations:
+@[backward_defeq] theorem valAndTarget.eq_1 : valAndTarget 0 =
+  have y := 1;
+  y + y
+@[backward_defeq] theorem valAndTarget.eq_2 : ∀ (n : Nat),
+  valAndTarget n.succ =
+    have y := 2;
+    y + n
+-/
+#guard_msgs in #print equations valAndTarget
+
+-- Structural recursion through a `match` in a value.
+def listVal (xs : List Nat) : Nat :=
+  have r := match xs with
+    | [] => 0
+    | x :: ys => x + listVal ys
+  r + r
+/--
+info: equations:
+@[backward_defeq] theorem listVal.eq_1 : listVal [] =
+  have r := 0;
+  r + r
+@[backward_defeq] theorem listVal.eq_2 : ∀ (x : Nat) (ys : List Nat),
+  listVal (x :: ys) =
+    have r := x + listVal ys;
+    r + r
+-/
+#guard_msgs in #print equations listVal
+
+-- Well-founded recursion through a `match` in a value.
+def wfVal (n : Nat) : Nat :=
+  have r := match n with
+    | 0 => 0
+    | m + 1 => wfVal (m / 2)
+  r + r
+termination_by n
+decreasing_by grind
+/--
+info: equations:
+@[backward_defeq] theorem wfVal.eq_1 : wfVal 0 =
+  have r := 0;
+  r + r
+theorem wfVal.eq_2 : ∀ (n_1 : Nat),
+  wfVal n_1.succ =
+    have r := wfVal (n_1 / 2);
+    r + r
+-/
+#guard_msgs in #print equations wfVal
+
+inductive Vec (α : Type) : Nat → Type
+  | nil : Vec α 0
+  | cons : α → Vec α n → Vec α (n + 1)
+
+-- Indexed discriminants in a value.
+def vecTwo (n : Nat) (v w : Vec Nat n) : Nat :=
+  have r := match v, w with
+    | .nil, .nil => 0
+    | .cons a _, .cons b _ => match a with
+      | 0 => b
+      | k + 1 => k + b
+  r + r
+/--
+info: equations:
+@[backward_defeq] theorem vecTwo.eq_1 : vecTwo 0 Vec.nil Vec.nil =
+  have r := 0;
+  r + r
+@[backward_defeq] theorem vecTwo.eq_2 : ∀ (n_2 : Nat) (a_1 : Vec Nat n_2) (b : Nat) (a_2 : Vec Nat n_2),
+  vecTwo (n_2 + 1) (Vec.cons 0 a_1) (Vec.cons b a_2) =
+    have r := b;
+    r + r
+@[backward_defeq] theorem vecTwo.eq_3 : ∀ (n_2 : Nat) (a_1 : Vec Nat n_2) (b : Nat) (a_2 : Vec Nat n_2) (n : Nat),
+  vecTwo (n_2 + 1) (Vec.cons n.succ a_1) (Vec.cons b a_2) =
+    have r := n + b;
+    r + r
+-/
+#guard_msgs in #print equations vecTwo
+
+-- `y` is inlined as a discriminant, since `match y` then reduces. `big` is not, since
+-- `match g w, big` does not reduce.
+def ctorDiscrIrrelevant (x w : Nat) : Nat :=
+  have big := some (x * x + x * x)
+  have y := some x
+  (match y with
+   | some n => n
+   | none => 0) +
+  (match g w, big with
+   | some a, some k => a + k
+   | _, _ => 0) +
+  (match g w, big with
+   | some a, some k => a - k
+   | _, _ => big.get!)
+
+/--
+info: equations:
+@[backward_defeq] theorem ctorDiscrIrrelevant.eq_1 : ∀ (x w : Nat),
+  ctorDiscrIrrelevant x w =
+    have big := some (x * x + x * x);
+    (x +
+        match g w, big with
+        | some a, some k => a + k
+        | x, x_1 => 0) +
+      match g w, big with
+      | some a, some k => a - k
+      | x, x_1 => big.get!
+-/
+#guard_msgs in #print equations ctorDiscrIrrelevant
+
+-- The `match` has the index `n + 1` as a discriminant, which `simpMatch?` reduces.
+def ctorDiscrIndexed (n a : Nat) (v w : Vec Nat n) : Nat :=
+  have p := Vec.cons a v
+  have q := Vec.cons a w
+  match p, q with
+  | .cons b _, .cons c _ => b + c
+
+/--
+info: equations:
+@[backward_defeq] theorem ctorDiscrIndexed.eq_1 : ∀ (n a : Nat) (v w : Vec Nat n), ctorDiscrIndexed n a v w = a + a
+-/
+#guard_msgs in #print equations ctorDiscrIndexed
+
+
+def haveNested (x y : Nat) :=
+  have a := y + y + y
+  have a' := a + 1
+  match x with
+  | 0 =>
+    have b := a + a
+    b + b
+  | _ =>
+    have c := a' + a'
+    have d := c
+    c + c
+
+/--
+info: haveNested.eq_1 (y : Nat) :
+  haveNested 0 y =
+    have a := y + y + y;
+    have b := a + a;
+    b + b
+-/
+#guard_msgs in
+#check haveNested.eq_1
+
+/--
+info: haveNested.eq_2 (x y : Nat) (x_3 : x = 0 → False) :
+  haveNested x y =
+    have a := y + y + y;
+    have a' := a + 1;
+    have c := a' + a';
+    c + c
+-/
+#guard_msgs in
+#check haveNested.eq_2
+
+def bigHave (x : Nat) (y : Nat) : Nat :=
+  have r := match x with
+    | 0 => y + y * y + y^3
+    | _ => y^4 + y^5 + y
+  r + r + r
+
+/--
+info: bigHave.eq_1 (y : Nat) :
+  bigHave 0 y =
+    have r := y + y * y + y ^ 3;
+    r + r + r
+-/
+#guard_msgs in #check bigHave.eq_1
+
+/--
+info: bigHave.eq_2 (x y : Nat) (x_3 : x = 0 → False) :
+  bigHave x y =
+    have r := y ^ 4 + y ^ 5 + y;
+    r + r + r
+-/
+#guard_msgs in #check bigHave.eq_2
diff --git a/tests/elab/eqns_no_congr_simp.lean b/tests/elab/eqns_no_congr_simp.lean
new file mode 100644
index 000000000000..bc1d784606cf
--- /dev/null
+++ b/tests/elab/eqns_no_congr_simp.lean
@@ -0,0 +1,27 @@
+import Lean
+open Lean Meta
+
+/-!
+Generating equation lemmas adds no `congr_simp` theorems to the environment. A module that
+imports such a theorem cannot unfold it, which breaks tools that unfold `congr_simp` theorems
+in proofs, such as Mathlib's `to_dual`.
+-/
+
+structure S where
+  n : Nat
+  h : 0 < n + 1
+
+def g (b : Bool) (m : Nat) : S :=
+  match b with
+  | true => ⟨m + 0, Nat.succ_pos _⟩
+  | false => ⟨0, Nat.succ_pos _⟩
+
+/--
+info: [g.eq_1, g.eq_2]
+---
+info: false
+-/
+#guard_msgs in
+run_meta do
+  logInfo m!"{(← getEqnsFor? ``g).getD #[]}"
+  logInfo m!"{(← getEnv).contains `S.mk.congr_simp}"
diff --git a/tests/elab/eqns_over_applied_match.lean b/tests/elab/eqns_over_applied_match.lean
new file mode 100644
index 000000000000..5569f7f15c39
--- /dev/null
+++ b/tests/elab/eqns_over_applied_match.lean
@@ -0,0 +1,43 @@
+/-!
+Equation lemmas split a `match` that is applied to more arguments than its arity, also when an
+alternative needs an overlap hypothesis.
+-/
+
+def over (a b : Bool) (n : Nat) : Nat :=
+  (match a, b with
+    | true, true => fun n => n
+    | _, _ => fun _ => 0) n
+
+/--
+info: over.eq_1 (n : Nat) : over true true n = n
+-/
+#guard_msgs in
+#check over.eq_1
+
+/--
+info: over.eq_2 (a b : Bool) (n : Nat) (x_2 : a = true → b = true → False) : over a b n = (fun x => 0) n
+-/
+#guard_msgs in
+#check over.eq_2
+
+inductive WT where
+  | of : Nat → WT
+  | star : WT
+
+@[reducible] def WT.Hom : WT → WT → Type
+  | of _, of _ => Nat
+  | star, of _ => PEmpty
+  | _, star => PUnit
+
+/-- The over-applied `match` that `@[to_dual]` produces for a composition of morphisms. -/
+def WT.comp {X Y Z : WT} (f : Hom X Y) (g : Hom Y Z) : Hom X Z :=
+  (match (motive := (x y z : WT) → Hom x y → Hom y z → Hom x z) X, Y, Z with
+    | of _, of _, of _ => fun f g => (f + g : Nat)
+    | of _, _, star => fun _ _ => PUnit.unit
+    | star, of _, _ => fun f _ => PEmpty.elim f
+    | _, star, of _ => fun _ g => PEmpty.elim g
+    | star, star, star => fun _ _ => PUnit.unit) f g
+
+/-- info: WT.comp.eq_5 (f g : WT.star.Hom WT.star) : WT.comp f g = PUnit.unit -/
+#guard_msgs in
+#check WT.comp.eq_5
diff --git a/tests/elab/eqns_telescope_proofs.lean b/tests/elab/eqns_telescope_proofs.lean
new file mode 100644
index 000000000000..575d5390dcd8
--- /dev/null
+++ b/tests/elab/eqns_telescope_proofs.lean
@@ -0,0 +1,94 @@
+module
+import Lean
+public meta import Lean.Meta.Tactic.Refl
+import all Lean.Elab.PreDefinition.Eqns
+
+/-!
+Checks the kernel proofs produced by equation normalization for simultaneous binding-value and
+body rewrites, mixed let/have telescopes, transitive type dependencies, dependent results, and
+matcher rewriting under local assumptions.
+-/
+
+open Lean Meta Elab
+
+def valueAndBody (x y : Nat) : Nat :=
+  have a := match x with | 5 => 1 | _ => 2
+  have b := a + 1
+  have c := match y with | 5 => b | _ => b + b
+  match x with | 5 => c | _ => c + a
+
+set_option cleanup.letToHave false in
+def mixedDependent (x y : Nat) : Nat :=
+  have a := match x with | 5 => 1 | _ => 2
+  let t := Fin (a + 1)
+  have z : t := ⟨a, Nat.lt_succ_self a⟩
+  have b := match y with | 5 => z.val | _ => z.val + z.val
+  match y with | 5 => b | _ => b + a
+
+set_option cleanup.letToHave false in
+def dependentResult (x y : Nat) : Fin (x + 2) :=
+  let n := x + 1
+  have _a := match y with | 5 => 0 | _ => 1
+  have b : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
+  match y with | 5 => ⟨0, Nat.zero_lt_succ n⟩ | _ => b
+
+meta def checkNormalizationProof (body : Expr) : MetaM Expr := do
+  let lhs ← mkFreshExprMVar (← inferType body)
+  let goal ← mkFreshExprSyntheticOpaqueMVar (← mkEq lhs body)
+  let normalized ← Lean.Elab.Eqns.normalizeEqn goal.mvarId!
+  let some (_, _, rhs) := (← normalized.getType').eq? | throwError "expected an equation"
+  if ← isDefEq body rhs then throwError "expected a nondefinitional rewrite"
+  normalized.refl
+  let proof ← instantiateMVars goal
+  checkWithKernel proof
+  unless ← isDefEq (← inferType proof) (← mkEq rhs body) do
+    throwError "incorrect telescope proof type"
+  return rhs
+
+run_meta do
+  for name in #[``valueAndBody, ``mixedDependent, ``dependentResult] do
+    let info ← getConstInfoDefn name
+    lambdaTelescope info.value fun xs body => do
+      withLocalDeclD `hx (mkNot (← mkEq xs[0]! (mkNatLit 5))) fun _ => do
+        withLocalDeclD `hy (mkNot (← mkEq xs[1]! (mkNatLit 5))) fun _ => do
+          discard <| checkNormalizationProof body
+
+def literalMatcher (x : Nat) : Nat := match x with | 5 => 1 | _ => 2
+
+-- Reusing a matcher across a lambda boundary must respect the hypothesis's scope in either order.
+run_meta do
+  withLocalDeclD `x (mkConst ``Nat) fun x => do
+    let .lam _ _ body _ := (← getConstInfoDefn ``literalMatcher).value
+      | throwError "unexpected matcher template"
+    let matcher := body.instantiate1 x
+    let fn := mkLambda `h .default (mkNot (← mkEq x (mkNatLit 5))) matcher
+    for reverse in [false, true] do
+      let pair ← mkAppM ``Prod.mk (if reverse then #[matcher, fn] else #[fn, matcher])
+      let rhs ← checkNormalizationProof pair
+      let_expr Prod.mk _ _ fst snd := rhs | throwError "expected a pair"
+      let (fn', matcher') := if reverse then (snd, fst) else (fst, snd)
+      let .lam _ _ body' _ := fn' | throwError "expected a lambda"
+      unless ← isDefEq body' (mkNatLit 2) do
+        throwError "matcher did not simplify under the local hypothesis"
+      unless matcher' == matcher do
+        throwError "matcher changed outside the hypothesis's scope"
+
+def zeroMatcher (x : Nat) : Nat := match x with | 0 => 1 | _ => 2
+
+-- A proof binding can enable rewriting a matcher whose earlier occurrence was unchanged.
+run_meta do
+  lambdaTelescope (← getConstInfoDefn ``zeroMatcher).value fun xs matcher => do
+    let x := xs[0]!
+    let nat := mkConst ``Nat
+    withLocalDeclD `hx (← mkEq (mkNatAdd x x) (mkNatLit 0)) fun hx => do
+      let proof ← mkAppM ``Nat.eq_zero_of_add_eq_zero_left #[hx]
+      let body ← withLetDecl `a nat matcher (nondep := true) fun a => do
+        withLetDecl `h (← mkEq x (mkNatLit 0)) proof (nondep := true) fun h => do
+          withLetDecl `b nat matcher (nondep := true) fun b => do
+            mkLetFVars #[a, h, b] (mkNatAdd a b) (usedLetOnly := false) (generalizeNondepLet := false)
+      let rhs ← checkNormalizationProof body
+      let .letE _ _ valueA (.letE _ _ valueB _ true) true := rhs
+        | throwError "expected both shared bindings"
+      unless valueA == matcher do throwError "earlier matcher changed before the proof binding"
+      unless ← isDefEq valueB (mkNatLit 1) do
+        throwError "later matcher did not simplify under the proof binding"
diff --git a/tests/elab/grind_ematch_gen_pattern.lean b/tests/elab/grind_ematch_gen_pattern.lean
index 3b70fb8d7499..1ed5d9393111 100644
--- a/tests/elab/grind_ematch_gen_pattern.lean
+++ b/tests/elab/grind_ematch_gen_pattern.lean
@@ -40,7 +40,7 @@ example (a : Nat) (h : b = some a) : (b.pbind fun a h => some <| 2*a) = some (a
 
 /--
 trace: [grind.ematch.instance] pbind_some': (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯)
-[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a
+[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a
 -/
 #guard_msgs (trace) in
 example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
@@ -54,7 +54,7 @@ trace: [grind.ematch.instance] pbind_some': ∀ (h : b = some a), (b.pbind fun a
       (b.pbind fun a h => some (a + f b ⋯)) = some (2 * a + f b ⋯)
 [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + f b ⋯)),
       (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯ + f b ⋯)
-[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a
+[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a
 [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 2 * f b ⋯)),
       (b.pbind fun a h => some (a + f b ⋯)) = some (a + 2 * f b ⋯ + f b ⋯)
 [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 3 * f b ⋯)),
@@ -112,7 +112,7 @@ reset_grind_attrs%
 
 /--
 trace: [grind.ematch.instance] pbind_some'': (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯)
-[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a
+[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a
 -/
 #guard_msgs (trace) in
 example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
@@ -127,7 +127,7 @@ reset_grind_attrs%
 
 /--
 trace: [grind.ematch.instance] pbind_some''': some (a + f b ⋯) = b.pbind fun a h => some (a + f b ⋯)
-[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a
+[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a
 -/
 #guard_msgs (trace) in
 example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
diff --git a/tests/elab/grind_ematch_gen_pattern.lean.out.expected b/tests/elab/grind_ematch_gen_pattern.lean.out.expected
index d6f8d7ee4d8c..41fc72d982f9 100644
--- a/tests/elab/grind_ematch_gen_pattern.lean.out.expected
+++ b/tests/elab/grind_ematch_gen_pattern.lean.out.expected
@@ -3,7 +3,7 @@
       (b.pbind fun a h => some (a + f b ⋯)) = some (2 * a + f b ⋯)
 [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + f b ⋯)),
       (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯ + f b ⋯)
-[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a
+[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a
 [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 2 * f b ⋯)),
       (b.pbind fun a h => some (a + f b ⋯)) = some (a + 2 * f b ⋯ + f b ⋯)
 [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 3 * f b ⋯)),
diff --git a/tests/elab/heapSort.lean b/tests/elab/heapSort.lean
index 92b04f3f7326..e47fd51c3328 100644
--- a/tests/elab/heapSort.lean
+++ b/tests/elab/heapSort.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 
+/-! Tests heap operations, heap sorting, and their generated equation theorems. -/
+
 /-- A max-heap data structure. -/
 structure BinaryHeap (α) (lt : α → α → Bool) where
   arr : Array α
@@ -184,9 +186,7 @@ info: Array.heapSort.loop.eq_1 fun a b =>
     let gt := fun y x => decide (x < y);
     match e : a.max with
     | none => out
-    | some x =>
-      have this := ⋯;
-      Array.heapSort.loop (fun a b => decide (a < b)) a.popMax (out.push x)
+    | some x => Array.heapSort.loop (fun a b => decide (a < b)) a.popMax (out.push x)
 -/
 #guard_msgs in
 #check Array.heapSort.loop.eq_1 (fun (a b : Nat) => a < b)
diff --git a/tests/elab/heapSort.lean.out.expected b/tests/elab/heapSort.lean.out.expected
index 5aeaa1953627..29c2b2306a4f 100644
--- a/tests/elab/heapSort.lean.out.expected
+++ b/tests/elab/heapSort.lean.out.expected
@@ -1,11 +1,11 @@
-heapSort.lean:15:4-15:15: warning: declaration uses `sorry`
-heapSort.lean:15:4-15:15: warning: declaration uses `sorry`
-heapSort.lean:13:0-36:24: warning: declaration uses `sorry`
-heapSort.lean:13:0-36:24: warning: declaration uses `sorry`
-heapSort.lean:43:4-43:10: warning: declaration uses `sorry`
-heapSort.lean:58:4-58:13: warning: declaration uses `sorry`
-heapSort.lean:58:4-58:13: warning: declaration uses `sorry`
-heapSort.lean:56:0-69:24: warning: declaration uses `sorry`
-heapSort.lean:56:0-69:24: warning: declaration uses `sorry`
-heapSort.lean:102:4-102:13: warning: declaration uses `sorry`
+heapSort.lean:17:4-17:15: warning: declaration uses `sorry`
+heapSort.lean:17:4-17:15: warning: declaration uses `sorry`
+heapSort.lean:15:0-38:24: warning: declaration uses `sorry`
+heapSort.lean:15:0-38:24: warning: declaration uses `sorry`
+heapSort.lean:45:4-45:10: warning: declaration uses `sorry`
+heapSort.lean:60:4-60:13: warning: declaration uses `sorry`
+heapSort.lean:60:4-60:13: warning: declaration uses `sorry`
+heapSort.lean:58:0-71:24: warning: declaration uses `sorry`
+heapSort.lean:58:0-71:24: warning: declaration uses `sorry`
+heapSort.lean:104:4-104:13: warning: declaration uses `sorry`
 heapSort.lean:194:11-194:15: warning: declaration uses `sorry`
diff --git a/tests/elab/splitList.lean.out.expected b/tests/elab/splitList.lean.out.expected
index b3be2e52d89b..a196d0620e50 100644
--- a/tests/elab/splitList.lean.out.expected
+++ b/tests/elab/splitList.lean.out.expected
@@ -3,11 +3,7 @@
 @len.eq_3 : ∀ {α : Type u_1} (a b : α) (as : List α),
   len (a :: b :: as) =
     match h : a :: b :: as, h₂ : splitList (a :: b :: as), ⋯ with
-    | .(fst ++ snd), ListSplit.split fst snd, h₁ =>
-      have this := ⋯;
-      have dec₁ := ⋯;
-      have dec₂ := ⋯;
-      len fst + len snd
+    | .(fst ++ snd), ListSplit.split fst snd, h₁ => len fst + len snd
 @len.eq_def : ∀ {α : Type u_1} (x : List α),
   len x =
     match x with
diff --git a/tests/elab/split_refine_match.lean b/tests/elab/split_refine_match.lean
new file mode 100644
index 000000000000..d88dad9f1c35
--- /dev/null
+++ b/tests/elab/split_refine_match.lean
@@ -0,0 +1,69 @@
+module
+import Lean
+public meta import Lean.Meta.Tactic.Split
+
+/-!
+Tests matcher-based case refinement of a target containing no matcher application, including
+overlapping patterns, computed discriminants, and discriminants closed over shared bindings.
+-/
+
+open Lean Meta Elab
+
+private def matcherTemplate (x y : Nat) : Nat :=
+  match x, y with
+  | 0, _ => 1
+  | _, 0 => 2
+  | n + 1, m + 1 => n + m
+
+private meta def hasHypothesis (type : Expr) : MetaM Bool := do
+  for decl in ← getLCtx do
+    if ← isDefEq decl.type type then return true
+  return false
+
+private meta def checkRefinement (app : MatcherApp) (x p : Expr)
+    (discr : Expr → MetaM Expr) (shared : Bool) : MetaM Unit := do
+  let goal ← mkFreshExprSyntheticOpaqueMVar (mkApp p x)
+  let branches ← Split.refineMatch goal.mvarId! app.matcherName app.matcherLevels app.params
+    #[x, ← discr x]
+  unless branches.length == 3 do throwError "expected three branches"
+  for i in *...3 do
+    let branch := branches[i]!
+    branch.withContext do
+      let target ← branch.getType'
+      unless target.isApp && target.appFn! == p do
+        throwError "refinement changed the target predicate"
+      let arg := target.appArg!
+      match i with
+      | 0 =>
+        unless ← isDefEq arg (mkNatLit 0) do throwError "first branch did not specialize x to zero"
+      | 1 =>
+        unless arg.isFVar do throwError "overlapping branch specialized x"
+        unless ← hasHypothesis (mkNot (← mkEq arg (mkNatLit 0))) do
+          throwError "missing overlap hypothesis"
+        unless ← hasHypothesis (← mkEq (← discr arg) (mkNatLit 0)) do
+          throwError "missing computed-discriminant hypothesis"
+      | _ =>
+        unless arg.isAppOfArity ``Nat.succ 1 && arg.appArg!.isFVar do
+          throwError "last branch did not specialize x to a successor"
+        let expected ← discr arg
+        let mut found := false
+        for decl in ← getLCtx do
+          if let some (_, lhs, rhs) := decl.type.eq? then
+            if rhs.isAppOfArity ``Nat.succ 1 && rhs.appArg!.isFVar then
+              if ← isDefEq lhs expected then
+                if shared && !lhs.isLet then throwError "discriminant sharing was lost"
+                found := true
+        unless found do throwError "missing successor discriminant hypothesis"
+
+run_meta do
+  let info ← getConstInfoDefn ``matcherTemplate
+  lambdaTelescope info.value fun xs rhs => do
+    let some app ← matchMatcherApp? rhs | throwError "expected matcher"
+    let nat := mkConst ``Nat
+    withLocalDeclD `f (← mkArrow nat nat) fun f => do
+      withLocalDeclD `p (← mkArrow nat (mkSort 0)) fun p => do
+        checkRefinement app xs[0]! p (fun x => pure (mkApp f x)) false
+        checkRefinement app xs[0]! p (fun x =>
+          withLetDecl `a nat (mkApp f x) (nondep := true) fun a =>
+            withLetDecl `b nat (mkNatAdd a a) (nondep := true) fun b =>
+              mkLetFVars #[a, b] (mkNatAdd b b) (generalizeNondepLet := false)) true
diff --git a/tests/elab/streamEqIssue.lean.out.expected b/tests/elab/streamEqIssue.lean.out.expected
index 6113afb57bee..53641cf5b562 100644
--- a/tests/elab/streamEqIssue.lean.out.expected
+++ b/tests/elab/streamEqIssue.lean.out.expected
@@ -1,10 +1,10 @@
 @Std.Stream.hasLength.eq_1 : ∀ {stream : Type u_1} {value : Type u_2} [inst : Std.Stream stream value] (s : stream),
   Std.Stream.next? s = none → Std.Stream.hasLength 0 s = true
 @Std.Stream.hasLength.eq_2 : ∀ {stream : Type u_1} {value : Type u_2} [inst : Std.Stream stream value] (s : stream)
-  (n_2 : Nat) (s' : stream) (fst : value),
-  Std.Stream.next? s = some (fst, s') → Std.Stream.hasLength n_2.succ s = Std.Stream.hasLength n_2 s'
+  (n_3 : Nat) (s' : stream) (fst : value),
+  Std.Stream.next? s = some (fst, s') → Std.Stream.hasLength n_3.succ s = Std.Stream.hasLength n_3 s'
 @Std.Stream.hasLength.eq_3 : ∀ {stream : Type u_1} {value : Type u_2} [inst : Std.Stream stream value] (s : stream)
-  (n : Nat),
-  (n = 0 → Std.Stream.next? s = none → False) →
-    (∀ (n_1 : Nat) (fst : value) (s' : stream), n = n_1.succ → Std.Stream.next? s = some (fst, s') → False) →
-      Std.Stream.hasLength n s = false
+  (n_1 : Nat),
+  (n_1 = 0 → Std.Stream.next? s = none → False) →
+    (∀ (n : Nat) (fst : value) (s' : stream), n_1 = n.succ → Std.Stream.next? s = some (fst, s') → False) →
+      Std.Stream.hasLength n_1 s = false
diff --git a/tests/elab/structuralEqn6.lean b/tests/elab/structuralEqn6.lean
index 0336c5142e03..4786bab4f10a 100644
--- a/tests/elab/structuralEqn6.lean
+++ b/tests/elab/structuralEqn6.lean
@@ -1,3 +1,5 @@
+/-! Tests structural and well-founded equation theorems with proof discriminants. -/
+
 def trailingZeros (i : Int) : Nat :=
   if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
 where
@@ -10,9 +12,8 @@ where
 
 /--
 info: equations:
-@[backward_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
+@[backward_defeq] theorem trailingZeros.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_3 : Nat) (hk_3 : i.natAbs ≤ k_3 + 1),
+  trailingZeros.aux k_3.succ i hi hk_3 acc = if h : i % 2 = 0 then trailingZeros.aux k_3 (i / 2) ⋯ ⋯ (acc + 1) else acc
 -/
 #guard_msgs(pass trace, all) in
 #print equations trailingZeros.aux
@@ -34,10 +35,9 @@ where
 
 /--
 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
+theorem trailingZeros'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_3 : Nat) (hk_3 : i.natAbs ≤ k_3 + 1),
+  trailingZeros'.aux k_3.succ i hi hk_3 acc =
+    if h : i % 2 = 0 then trailingZeros'.aux k_3 (i / 2) ⋯ ⋯ (acc + 1) else acc
 -/
 #guard_msgs(pass trace, all) in
 #print equations trailingZeros'.aux
diff --git a/tests/elab/structuralEqns2.lean.out.expected b/tests/elab/structuralEqns2.lean.out.expected
index df4559555524..fffeac9030d3 100644
--- a/tests/elab/structuralEqns2.lean.out.expected
+++ b/tests/elab/structuralEqns2.lean.out.expected
@@ -7,8 +7,14 @@ g.eq_def (i j : Nat) :
       match j with
       | Nat.zero => 1
       | j.succ => g i j
-h.eq_1 (i : Nat) : h i Nat.zero = 1 + 1
-h.eq_2 (i j_2 : Nat) : h i j_2.succ = h i j_2 + h i j_2
+h.eq_1 (i : Nat) :
+  h i Nat.zero =
+    have z := 1;
+    z + z
+h.eq_2 (i j_2 : Nat) :
+  h i j_2.succ =
+    have z := h i j_2;
+    z + z
 h.eq_def (i j : Nat) :
   h i j =
     have z :=
diff --git a/tests/elab/vcgenJPs.lean b/tests/elab/vcgenJPs.lean
index 9afd0385e794..5ddad37263df 100644
--- a/tests/elab/vcgenJPs.lean
+++ b/tests/elab/vcgenJPs.lean
@@ -326,3 +326,28 @@ def match_in_match (o p : Option Nat) : StateM Nat Nat := do
 theorem match_in_match_triple :
     ⦃ fun _ => True ⦄ match_in_match o p ⦃ fun r => ⌜r > 0⌝ ⦄ := by
   vcgen +jp [match_in_match] with finish
+
+-- The join point above a split `match` is kept by `root_match.eq_2` and shared by `vcgen +jp`.
+def root_match (x : Nat) (b : Bool) : StateM Nat Nat := do
+  let mut y := 0
+  match x with
+  | 0 => y := 1
+  | _ + 1 => if b then y := 2 else y := 3
+  let s ← get
+  return y + s
+
+/--
+trace: case vc1
+k : Nat
+b : Bool
+s✝ : Nat
+x✝¹ : PUnit
+x✝ s : Nat
+h✝ : b = true ∧ x✝ = 2 ∧ s = s✝ ∨ ¬b = true ∧ x✝ = 3 ∧ s = s✝
+⊢ 0 < x✝ + s
+-/
+#guard_msgs in
+example : ⦃fun _ => True⦄ root_match (k + 1) b ⦃fun r => ⌜r > 0⌝⦄ := by
+  vcgen +jp [root_match]
+  trace_state
+  all_goals grind