diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
new file mode 100644
index 000000000000..f12a0bbadcfa
--- /dev/null
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -0,0 +1,592 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+import Lean.Util.HasConstCache
+import Lean.Meta.CasesOn
+import Lean.Meta.Match.Match
+import Lean.Meta.Tactic.Cleanup
+import Lean.Meta.Tactic.Refl
+import Lean.Elab.Quotation
+import Lean.Elab.RecAppSyntax
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Structural.Basic
+import Lean.Elab.PreDefinition.WF.TerminationHint
+
+
+/-!
+This module finds lexicographic termination arguments for well-founded recursion.
+
+Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), it tries all combinations
+until it finds one where all proof obligations go through with the given tactic (`decerasing_by`),
+if given, or the default `decreasing_tactic`.
+
+For mutual recursion, a single measure is not just one parameter, but one from each recursive
+function. Enumerating these can lead to a combinatoric explosion, so we bound
+the nubmer of measures tried.
+
+In addition to measures derived from `sizeOf xᵢ`, it also considers measures
+that assign an order to the functions themselves. This way we can support mutual
+function definitions where no arguments decrease from one function to another.
+
+
+The result of this module is a `TerminationWF`, which is then passed on to `wfRecursion`; this
+design is crucial so that whatever we infer in this module could also be written manually by the
+user. It would be bad if there are function definitions that can only be processed with the
+guessed lexicographic order.
+
+The following optimizations are applied to make this feasible:
+
+1. The crucial optimiziation is to look at each argument of each recursive call
+   _once_, try to prove `<` and (if that fails `≤`), and then look at that table to
+   pick a suitable measure.
+
+2. The next-crucial optimization is to fill that table lazily.  This way, we run the (likely
+   expensive) tactics as few times as possible, while still being able to consider a possibly
+   large number of combinations.
+
+3. Before we even try to prove `<`, we check if the arguments are equal (`=`). No well-founded
+   measure will relate equal terms, likely this check is faster than firing up the tactic engine,
+   and it adds more signal to the output.
+
+4. Instead of traversing the whole function body over and over, we traverse it once and store
+   the arguments (in unpacked form) and the local `MetaM` state at each recursive call
+   (see `collectRecCalls`), which we then re-use for the possibly many proof attempts.
+
+The logic here is based on “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL”
+by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, 10.1007/978-3-540-74591-4_5
+<https://www21.in.tum.de/~nipkow/pubs/tphols07.pdf>.
+-/
+
+set_option autoImplicit false
+
+open Lean Meta Elab
+
+namespace Lean.Elab.WF.GuessLex
+
+/--
+Given a predefinition, find good variable names for its parameters.
+Use user-given parameter names if present; use x1...xn otherwise.
+The length of the returned array is also used to determine the arity
+of the function, so it should match what `packDomain` does.
+-/
+def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name):= do
+  lambdaTelescope preDef.value fun xs _ => do
+    let xs := xs.extract fixedPrefixSize xs.size
+    let mut ns := #[]
+    for h : i in [:xs.size] do
+      let n ← (xs[i]'h.2).fvarId!.getUserName
+      if n.hasMacroScopes then
+        ns := ns.push (← mkFreshUserName (.mkSimple s!"x{i+1}"))
+      else
+        ns := ns.push n
+    return ns
+
+/-- Internal monad used by `withRecApps` -/
+abbrev M (recFnName : Name) (α β : Type) : Type :=
+  StateRefT (Array α) (StateRefT (HasConstCache recFnName) MetaM) β
+
+/--
+Traverses the given expression `e`, and invokes the continuation `k`
+at every saturated call to `recFnName`.
+
+The expression `scrut` is passed along, and refined when going under a matcher
+or `casesOn` application.
+-/
+partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (scrut : Expr) (e : Expr)
+    (k : Expr → Array Expr → MetaM α) : MetaM (Array α) := do
+  trace[Elab.definition.wf] "withRecApps: {indentExpr e}"
+  let (_, as) ← loop scrut e |>.run #[] |>.run' {}
+  return as
+where
+  processRec (scrut : Expr) (e : Expr) : M recFnName α Unit := do
+    if e.getAppNumArgs < fixedPrefixSize + 1 then
+      loop scrut (← etaExpand e)
+    else
+      let a ← k scrut e.getAppArgs
+      modifyThe (Array α) (·.push a)
+
+  processApp (scrut : Expr) (e : Expr) : M recFnName α Unit := do
+    e.withApp fun f args => do
+      args.forM (loop scrut)
+      if f.isConstOf recFnName then
+        processRec scrut e
+      else
+        loop scrut f
+
+  containsRecFn (e : Expr) : M recFnName α Bool := do
+    modifyGetThe (HasConstCache recFnName) (·.contains e)
+
+  loop (scrut : Expr) (e : Expr) : M recFnName α Unit := do
+    if !(← containsRecFn e) then
+      return
+    match e with
+    | Expr.lam n d b c =>
+      loop scrut d
+      withLocalDecl n c d fun x => do
+        loop scrut (b.instantiate1 x)
+    | Expr.forallE n d b c =>
+      loop scrut d
+      withLocalDecl n c d fun x => do
+        loop scrut (b.instantiate1 x)
+    | Expr.letE n type val body _ =>
+      loop scrut type
+      loop scrut val
+      withLetDecl n type val fun x => do
+        loop scrut (body.instantiate1 x)
+    | Expr.mdata _d b =>
+      if let some stx := getRecAppSyntax? e then
+        withRef stx <| loop scrut b
+      else
+        loop scrut b
+    | Expr.proj _n _i e => loop scrut e
+    | Expr.const .. => if e.isConstOf recFnName then processRec scrut e
+    | Expr.app .. =>
+      match (← matchMatcherApp? e) with
+      | some matcherApp =>
+        if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
+          processApp scrut e
+        else
+          if let some altScruts ← matcherApp.refineThrough? scrut then
+            (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altScruts)).forM
+              fun (alt, altNumParam, altScrut) =>
+                lambdaTelescope alt fun xs altBody => do
+                  unless altNumParam ≤ xs.size do
+                    throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
+                  let altScrut := altScrut.instantiateRev xs[:altNumParam]
+                  loop altScrut altBody
+          else
+            processApp scrut e
+      | none =>
+      match (← toCasesOnApp? e) with
+      | some casesOnApp =>
+        if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
+          processApp scrut e
+        else
+          if let some altScruts ← casesOnApp.refineThrough? scrut then
+          (Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altScruts)).forM
+            fun (alt, altNumParam, altScrut) =>
+              lambdaTelescope alt fun xs altBody => do
+                unless altNumParam ≤ xs.size do
+                  throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
+                let altScrut := altScrut.instantiateRev xs[:altNumParam]
+                loop altScrut altBody
+          else
+            processApp scrut e
+      | none => processApp scrut e
+    | e => do
+      let _ ← ensureNoRecFn recFnName e
+
+/--
+A `SavedLocalContext` captures the state and local context of a `MetaM`, to be continued later.
+-/
+structure SavedLocalContext where
+  savedLocalContext : LocalContext
+  savedLocalInstances : LocalInstances
+  savedState : Meta.SavedState
+
+/-- Capture the `MetaM` state including local context. -/
+def SavedLocalContext.create : MetaM SavedLocalContext := do
+  let savedLocalContext ← getLCtx
+  let savedLocalInstances ← getLocalInstances
+  let savedState ← saveState
+  return { savedLocalContext, savedLocalInstances, savedState }
+
+/-- Run a `MetaM` action in the saved state. -/
+def SavedLocalContext.run {α} (slc : SavedLocalContext) (k : MetaM α) :
+    MetaM α :=
+  withoutModifyingState $ do
+    withLCtx slc.savedLocalContext slc.savedLocalInstances do
+      slc.savedState.restore
+      k
+
+/-- A `RecCallWithContext` focuses on a single recursive call in a unary predefinition,
+and runs the given action in the context of that call.  -/
+structure RecCallWithContext where
+  /-- Function index of caller -/
+  caller : Nat
+  /-- Parameters of caller -/
+  params : Array Expr
+  /-- Function index of callee -/
+  callee : Nat
+  /-- Arguments to callee -/
+  args : Array Expr
+  ctxt : SavedLocalContext
+
+/-- Store the current recursive call and its context. -/
+def RecCallWithContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) :
+    MetaM RecCallWithContext := do
+  return { caller, params, callee, args, ctxt := (← SavedLocalContext.create) }
+
+/-- Given the packed argument of a (possibly) mutual and (possibly) nary call,
+return the function index that is called and the arguments individually.
+
+We expect precisely the expressions produced by `packMutual`, with manifest
+`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
+rather than using projectinos. -/
+def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) :
+    m (Nat × Array Expr) := do
+  -- count PSum injections to find out which function is doing the call
+  let mut funidx := 0
+  let mut e := e
+  while funidx + 1 < arities.size do
+    if e.isAppOfArity ``PSum.inr 3 then
+      e := e.getArg! 2
+      funidx := funidx + 1
+    else if e.isAppOfArity ``PSum.inl 3 then
+      e := e.getArg! 2
+      break
+    else
+      throwError "Unexpected expression while unpacking mutual argument"
+
+  -- now unpack PSigmas
+  let arity := arities[funidx]!
+  let mut args := #[]
+  while args.size + 1 < arity do
+    if e.isAppOfArity ``PSigma.mk 4 then
+      args := args.push (e.getArg! 2)
+      e := e.getArg! 3
+    else
+      throwError "Unexpected expression while unpacking n-ary argument"
+  args := args.push e
+  return (funidx, args)
+
+/-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive
+call site.
+-/
+def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat)
+    : MetaM (Array RecCallWithContext) := withoutModifyingState do
+  addAsAxiom unaryPreDef
+  lambdaTelescope unaryPreDef.value fun xs body => do
+    unless xs.size == fixedPrefixSize + 1 do
+      -- Maybe cleaner to have lambdaBoundedTelescope?
+      throwError "Unexpected number of lambdas in unary pre-definition"
+    -- trace[Elab.definition.wf] "collectRecCalls: {xs} {body}"
+    let param := xs[fixedPrefixSize]!
+    withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do
+      unless args.size ≥ fixedPrefixSize + 1 do
+        throwError "Insufficient arguments in recursive call"
+      let arg := args[fixedPrefixSize]!
+      let (caller, params) ← unpackArg arities param
+      let (callee, args) ← unpackArg arities arg
+      RecCallWithContext.create caller params callee args
+
+/-- A `GuessLexRel` described how a recursive call affects a measure; whether it
+decreases strictly, non-strictly, is equal, or else.  -/
+inductive GuessLexRel | lt | eq | le | no_idea
+deriving Repr, DecidableEq
+
+instance : ToFormat GuessLexRel where
+  format | .lt => "<"
+         | .eq => "="
+         | .le => "≤"
+         | .no_idea => "?"
+
+/-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly. -/
+def GuessLexRel.toNatRel : GuessLexRel → Expr
+  | lt => mkAppN (mkConst ``LT.lt [levelZero]) #[mkConst ``Nat, mkConst ``instLTNat]
+  | eq => mkAppN (mkConst ``Eq [levelOne]) #[mkConst ``Nat]
+  | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat]
+  | no_idea => unreachable!
+
+/-- Given an expression `e`, produce `sizeOf e` with a suitable instance. -/
+def mkSizeOf (e : Expr) : MetaM Expr := do
+  let ty ← inferType e
+  let lvl ← getLevel ty
+  let inst ← synthInstance (mkAppN (mkConst ``SizeOf [lvl]) #[ty])
+  let res := mkAppN (mkConst ``sizeOf [lvl]) #[ty,  inst, e]
+  check res
+  return res
+
+/--
+For a given recursive call, and a choice of parameter and argument index,
+try to prove equality, < or ≤.
+-/
+def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallWithContext) (paramIdx argIdx : Nat) :
+    MetaM GuessLexRel := do
+  rcc.ctxt.run do
+    let param := rcc.params[paramIdx]!
+    let arg := rcc.args[argIdx]!
+    trace[Elab.definition.wf] "inspectRecCall: {rcc.caller} ({param}) → {rcc.callee} ({arg})"
+    let arg ← mkSizeOf rcc.args[argIdx]!
+    let param ← mkSizeOf rcc.params[paramIdx]!
+    for rel in [GuessLexRel.eq, .lt, .le] do
+      let goalExpr := mkAppN rel.toNatRel #[arg, param]
+      trace[Elab.definition.wf] "Goal for {rel}: {goalExpr}"
+      check goalExpr
+
+      let mvar ← mkFreshExprSyntheticOpaqueMVar goalExpr
+      let mvarId := mvar.mvarId!
+      let mvarId ← mvarId.cleanup
+      -- logInfo m!"Remaining goals: {goalsToMessageData [mvarId]}"
+      try
+        if rel = .eq then
+          MVarId.refl mvarId
+        else do
+          Lean.Elab.Term.TermElabM.run' do
+            match decrTactic? with
+            | none =>
+              let remainingGoals ← Tactic.run mvarId do
+                Tactic.evalTactic (← `(tactic| decreasing_tactic))
+              remainingGoals.forM fun mvarId => Term.reportUnsolvedGoals [mvarId]
+              -- trace[Elab.definition.wf] "Found {rel} proof: {← instantiateMVars mvar}"
+              pure ()
+            | some decrTactic => Term.withoutErrToSorry do
+              -- make info from `runTactic` available
+              pushInfoTree (.hole mvarId)
+              Term.runTactic mvarId decrTactic
+              -- trace[Elab.definition.wf] "Found {rel} proof: {← instantiateMVars mvar}"
+              pure ()
+        trace[Elab.definition.wf] "inspectRecCall: success!"
+        return rel
+      catch _e =>
+        trace[Elab.definition.wf] "Did not find {rel} proof: {goalsToMessageData [mvarId]}"
+        continue
+    return .no_idea
+
+/- A cache for `evalRecCall` -/
+structure RecCallCache where mk'' ::
+  decrTactic? : Option Syntax
+  rcc : RecCallWithContext
+  cache : IO.Ref (Array (Array (Option GuessLexRel)))
+
+/-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/
+def RecCallCache.mk (decrTactic? : Option Syntax) (rcc : RecCallWithContext) :
+    BaseIO RecCallCache := do
+  let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none)
+  return { decrTactic?, rcc, cache }
+
+/-- Run `evalRecCall` and cache there result -/
+def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do
+  -- Check the cache first
+  if let Option.some res := (← rc.cache.get)[paramIdx]![argIdx]! then
+    return res
+  else
+    let res ← evalRecCall rc.decrTactic? rc.rcc paramIdx argIdx
+    rc.cache.modify (·.modify paramIdx (·.set! argIdx res))
+    return res
+
+/-- Pretty-print the cache entries -/
+def RecCallCache.pretty (rc : RecCallCache) : IO Format := do
+  let mut r := Format.nil
+  let d ← rc.cache.get
+  for h₁ : paramIdx in [:d.size] do
+    for h₂ : argIdx in [:(d[paramIdx]'h₁.2).size] do
+      if let .some entry := (d[paramIdx]'h₁.2)[argIdx]'h₂.2 then
+        r := r ++
+          f!"(Param {paramIdx}, arg {argIdx}): {entry}" ++ Format.line
+  return r
+
+/-- The measures that we order lexicographically can be comparing arguments,
+or numbering the functions -/
+inductive MutualMeasure where
+  /-- For every function, the given argument index -/
+  | args : Array Nat → MutualMeasure
+  /-- The given function index is assigned 1, the rest 0 -/
+  | func : Nat → MutualMeasure
+
+/-- Evaluate a recursive call at a given `MutualMeasure` -/
+def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
+  | .args argIdxs => do
+    let paramIdx := argIdxs[rc.rcc.caller]!
+    let argIdx := argIdxs[rc.rcc.callee]!
+    rc.eval paramIdx argIdx
+  | .func funIdx => do
+    if rc.rcc.caller == funIdx && rc.rcc.callee != funIdx then
+      return .lt
+    if rc.rcc.caller != funIdx && rc.rcc.callee == funIdx then
+      return .no_idea
+    else
+      return .eq
+
+/--
+Given a predefinition with value `fun (x_₁ ... xₙ) (y_₁ : α₁)... (yₘ : αₘ) => ...`,
+where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `sizeOf yᵢ` reduces to a literal.
+This is the case for types such as `Prop`, `Type u`, etc.
+These arguments should not be considered when guessing a well-founded relation.
+See `generateCombinations?`
+-/
+def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
+  lambdaTelescope preDef.value fun xs _ => do
+    let mut result := #[]
+    for x in xs[fixedPrefixSize:], i in [:xs.size] do
+      try
+        let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
+        if sizeOf.isLit then
+         result := result.push i
+      catch _ =>
+        result := result.push i
+    return result
+
+
+/--
+Generate all combination of arguments, skipping those that are forbidden.
+
+Sorts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
+try first, when the mutually recursive functions have similar argument structures
+-/
+partial def generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat)
+    (threshold : Nat := 32) : Option (Array (Array Nat)) :=
+  (do goUniform 0; go 0 #[]) |>.run #[] |>.2
+where
+  isForbidden (fidx : Nat) (argIdx : Nat) : Bool :=
+    if h : fidx < forbiddenArgs.size then
+       forbiddenArgs[fidx] |>.contains argIdx
+    else
+      false
+
+  -- Enumerate all permissible uniform combinations
+  goUniform (argIdx : Nat) : OptionT (StateM (Array (Array Nat))) Unit  := do
+    if numArgs.all (argIdx < ·) then
+      unless forbiddenArgs.any (·.contains argIdx) do
+        modify (·.push (Array.mkArray numArgs.size argIdx))
+      goUniform (argIdx + 1)
+
+  -- Enumerate all other permissible combinations
+  go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do
+    if h : fidx < numArgs.size then
+      let n := numArgs[fidx]
+      for argIdx in [:n] do
+        unless isForbidden fidx argIdx do
+          withReader (·.push argIdx) (go (fidx + 1))
+    else
+      let comb ← read
+      unless comb.all (· == comb[0]!) do
+        modify (·.push comb)
+      if (← get).size > threshold then
+        failure
+
+
+/--
+Enumerate all meausures we want to try: All arguments (resp. combinations thereof) and
+possible orderings of functions (if more than one)
+-/
+def generateMeasures (forbiddenArgs : Array (Array Nat)) (arities : Array Nat) :
+    MetaM (Array MutualMeasure) := do
+  let some arg_measures := generateCombinations? forbiddenArgs arities
+      | throwError "Too many combinations"
+
+  let func_measures :=
+    if arities.size > 1 then
+      (List.range arities.size).toArray
+    else
+      #[]
+
+  return arg_measures.map .args ++ func_measures.map .func
+
+/--
+The core logic of guessing the lexicographic order
+Given a matrix that for each call and measure indicates whether that measure is
+decreasing, equal, less-or-equal or unknown, It finds a sequence of measures
+that is lexicographically decreasing.
+
+The matrix is implemented here as an array of monadic query methods only so that
+we can fill is lazily. Morally, this is a pure function
+-/
+partial def solve {m} {α} [Monad m] (measures : Array α)
+  (calls : Array (α → m GuessLexRel)) : m (Option (Array α)) := do
+  go measures calls #[]
+  where
+  go (measures : Array α) (calls : Array (α → m GuessLexRel)) (acc : Array α) := do
+    if calls.isEmpty then return .some acc
+
+    -- Find the first measure that has at least one < and otherwise only = or <=
+    for h : measureIdx in [:measures.size] do
+      let measure := measures[measureIdx]'h.2
+      let mut has_lt := false
+      let mut all_le := true
+      let mut todo := #[]
+      for call in calls do
+        let entry ← call measure
+        if entry = .lt then
+          has_lt := true
+        else
+          todo := todo.push call
+          if entry != .le && entry != .eq then
+            all_le := false
+            break
+      -- No progress here? Try the next measure
+      if not (has_lt && all_le) then continue
+      -- We found a suitable measure, remove it from the list (mild optimization)
+      let measures' := measures.eraseIdx measureIdx
+      return ← go measures' todo (acc.push measure)
+    -- None found, we have to give up
+    return .none
+
+/--
+Create Tuple syntax (`()` if the array is empty, and just the value if its a singleton)
+-/
+def mkTupleSyntax : Array Term → MetaM Term
+  | #[]  => `(())
+  | #[e] => return e
+  | es   => `(($(es[0]!), $(es[1:]),*))
+
+/--
+Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic
+combination of these measures.
+-/
+def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
+    (measures : Array MutualMeasure) : MetaM TerminationWF := do
+  let mut termByElements := #[]
+  for h : funIdx in [:varNamess.size] do
+    let vars := (varNamess[funIdx]'h.2).map mkIdent
+    let body ← mkTupleSyntax (← measures.mapM fun
+      | .args varIdxs =>
+          let v := vars.get! (varIdxs[funIdx]!)
+          let sizeOfIdent := mkIdent ``sizeOf
+          `($sizeOfIdent $v)
+      | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
+      )
+    let declName := declNames[funIdx]!
+
+    trace[Elab.definition.wf] "Using termination {declName}: {vars} => {body}"
+    termByElements := termByElements.push
+      { ref := .missing
+        declName, vars, body,
+        implicit := true
+      }
+  return .ext termByElements
+
+end Lean.Elab.WF.GuessLex
+
+namespace Lean.Elab.WF
+
+open Lean.Elab.WF.GuessLex
+
+/--
+Main entry point of this module:
+
+Try to find a lexicographic ordering of the arguments for which the recursive definition
+terminates. See the module doc string for a high-level overview.
+-/
+def guessLex (preDefs : Array PreDefinition)  (unaryPreDef : PreDefinition)
+    (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) :
+    MetaM TerminationWF := do
+  try
+    let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
+    let arities := varNamess.map (·.size)
+    trace[Elab.definition.wf] "varNames is: {varNamess}"
+
+    -- Collect all recursive calls and extract their context
+    let recCalls ←collectRecCalls unaryPreDef fixedPrefixSize arities
+    let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·)
+    let callMatrix := rcs.map (inspectCall ·)
+
+    let forbiddenArgs ← preDefs.mapM fun preDef =>
+      getForbiddenByTrivialSizeOf fixedPrefixSize preDef
+
+    -- The list of measures, including the measures that order functions.
+    -- The function ordering measures come last
+    let measures ← generateMeasures forbiddenArgs arities
+
+    match ← liftMetaM <| solve measures callMatrix with
+    | .some solution => do
+      let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
+      return wf
+    | .none => throwError "Cannot find a decreasing lexicographic order"
+  catch _ =>
+    -- Hide all errors from guessing lexicographic orderings, as before
+    -- Future work: explain the failure to the user, like  Isabelle does
+    throwError "failed to prove termination, use `termination_by` to specify a well-founded relation"
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index 7067c1b43988..ea82f6baf3f5 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -12,6 +12,7 @@ import Lean.Elab.PreDefinition.WF.Rel
 import Lean.Elab.PreDefinition.WF.Fix
 import Lean.Elab.PreDefinition.WF.Eqns
 import Lean.Elab.PreDefinition.WF.Ite
+import Lean.Elab.PreDefinition.WF.GuessLex
 
 namespace Lean.Elab
 open WF
@@ -89,10 +90,17 @@ def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (de
     let preDefsDIte ← preDefs.mapM fun preDef => return { preDef with value := (← iteToDIte preDef.value) }
     let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte
     return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
+
+  let wf ←
+    if let .some wf := wf? then
+      pure wf
+    else
+      guessLex preDefs unaryPreDef fixedPrefixSize decrTactic?
+
   let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
     let type ← whnfForall type
     let packedArgType := type.bindingDomain!
-    elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf? fun wfRel => do
+    elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 9b872e659206..6ca0bd16ea51 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -53,67 +53,21 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
       mvarId.rename fvarId varNames.back
   go 0 mvarId fvarId
 
-def getNumCandidateArgs (fixedPrefixSize : Nat) (preDefs : Array PreDefinition) : MetaM (Array Nat) := do
-  preDefs.mapM fun preDef =>
-    lambdaTelescope preDef.value fun xs _ =>
-      return xs.size - fixedPrefixSize
-
-/--
-  Given a predefinition with value `fun (x_₁ ... xₙ) (y_₁ : α₁)... (yₘ : αₘ) => ...`,
-  where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `sizeOf yᵢ` reduces to a literal.
-  This is the case for types such as `Prop`, `Type u`, etc.
-  This arguments should not be considered when guessing a well-founded relation.
-  See `generateCombinations?`
--/
-def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
-  lambdaTelescope preDef.value fun xs _ => do
-    let mut result := #[]
-    for x in xs[fixedPrefixSize:], i in [:xs.size] do
-      try
-        let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
-        if sizeOf.isLit then
-         result := result.push i
-      catch _ =>
-        result := result.push i
-    return result
-
-def generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat) (threshold : Nat := 32) : Option (Array (Array Nat)) :=
-  go 0 #[] |>.run #[] |>.2
-where
-  isForbidden (fidx : Nat) (argIdx : Nat) : Bool :=
-    if h : fidx < forbiddenArgs.size then
-       forbiddenArgs.get ⟨fidx, h⟩ |>.contains argIdx
-    else
-      false
-
-  go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do
-    if h : fidx < numArgs.size then
-      let n := numArgs.get ⟨fidx, h⟩
-      for argIdx in [:n] do
-        unless isForbidden fidx argIdx do
-          withReader (·.push argIdx) (go (fidx + 1))
-    else
-      modify (·.push (← read))
-      if (← get).size > threshold then
-        failure
-termination_by _ fidx => numArgs.size - fidx
-
-def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat) (argType : Expr) (wf? : Option TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do
+def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat)
+    (argType : Expr) (wf : TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do
   let α := argType
   let u ← getLevel α
   let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
   trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
-  match wf? with
-  | some (TerminationWF.core wfStx) => withDeclName unaryPreDefName do
+  withDeclName unaryPreDefName do
+  match wf with
+  | TerminationWF.core wfStx =>
       let wfRel ← instantiateMVars (← withSynthesize <| elabTermEnsuringType wfStx expectedType)
       let pendingMVarIds ← getMVars wfRel
       discard <| logUnassignedUsingErrorInfos pendingMVarIds
       k wfRel
-  | some (TerminationWF.ext elements) => go expectedType elements
-  | none => guess expectedType
-where
-  go (expectedType : Expr) (elements : Array TerminationByElement) : TermElabM α :=
-    withDeclName unaryPreDefName <| withRef (getRefFromElems elements) do
+  | TerminationWF.ext elements =>
+    withRef (getRefFromElems elements) do
       let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
       let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
       let (d, fMVarId) ← fMVarId.intro1
@@ -127,38 +81,4 @@ where
       wfRelMVarId.assign wfRelVal
       k (← instantiateMVars (mkMVar mainMVarId))
 
-  generateElements (numArgs : Array Nat) (argCombination : Array Nat) : TermElabM (Array TerminationByElement) := do
-    let mut result := #[]
-    let var ← `(x)
-    let hole ← `(_)
-    for preDef in preDefs, numArg in numArgs, argIdx in argCombination, i in [:preDefs.size] do
-      let mut vars := #[var]
-      for _ in [:numArg - argIdx - 1] do
-        vars := vars.push hole
-      -- TODO: improve this.
-      -- The following trick allows a function `f` in a mutual block to invoke `g` appearing before it with the input argument.
-      -- We should compute the "right" order (if there is one) in the future.
-      let body ← if preDefs.size > 1 then `((sizeOf x, $(quote i))) else `(sizeOf x)
-      result := result.push {
-        ref := preDef.ref
-        declName := preDef.declName
-        vars := vars
-        body := body
-        implicit := false
-      }
-    return result
-
-  guess (expectedType : Expr) : TermElabM α := do
-    -- TODO: add support for lex
-    let numArgs ← getNumCandidateArgs fixedPrefixSize preDefs
-    -- TODO: include in `forbiddenArgs` arguments that are fixed but are not in the fixed prefix
-    let forbiddenArgs ← preDefs.mapM fun preDef => getForbiddenByTrivialSizeOf fixedPrefixSize preDef
-    -- TODO: add option to control the maximum number of cases to try
-    if let some combs := generateCombinations? forbiddenArgs numArgs then
-      for comb in combs do
-        let elements ← generateElements numArgs comb
-        if let some r ← observing? (go expectedType elements) then
-          return r
-    throwError "failed to prove termination, use `termination_by` to specify a well-founded relation"
-
 end Lean.Elab.WF
diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean
index 7646455f9e2d..86371632a4cc 100644
--- a/src/Lean/Meta/CasesOn.lean
+++ b/src/Lean/Meta/CasesOn.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.KAbstract
 import Lean.Meta.Check
+import Lean.Meta.AppBuilder
 
 namespace Lean.Meta
 
@@ -50,13 +51,17 @@ def CasesOnApp.toExpr (c : CasesOnApp) : Expr :=
 /--
   Given a `casesOn` application `c` of the form
   ```
-  casesOn As (fun is x => motive[i, xs]) is major  (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
+  casesOn As (fun is x => motive[is, xs]) is major  (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
   ```
   and an expression `e : B[is, major]`, construct the term
   ```
-  casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining
+  casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[_, C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[_, C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining
   ```
   We use `kabstract` to abstract the `is` and `major` from `B[is, major]`.
+
+  This is used in in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to
+  the argument provided by `fix` to refine the termination argument, which may mention `major`.
+  See there for how to use this function.
 -/
 def CasesOnApp.addArg (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := false) : MetaM CasesOnApp := do
   lambdaTelescope c.motive fun motiveArgs motiveBody => do
@@ -106,11 +111,72 @@ where
       throwError "failed to add argument to `casesOn` application, argument type was not refined by `casesOn`"
     return altsNew
 
-/-- Similar `CasesOnApp.addArg`, but returns `none` on failure. -/
+/-- Similar to `CasesOnApp.addArg`, but returns `none` on failure. -/
 def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := false) : MetaM (Option CasesOnApp) :=
   try
     return some (← c.addArg arg checkIfRefined)
   catch _ =>
     return none
 
+/--
+  Given a `casesOn` application `c` of the form
+  ```
+  casesOn As (fun is x => motive[is, xs]) is major  (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
+  ```
+  and an expression `B[is, major]` (which may not be a type, e.g. `n : Nat`)
+  for every alternative `i`, construct the type `B[_, C_i[ys_i]]`
+  with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `CasesOnApp.altNumParams`.
+
+  This is similar to `CasesOnApp.addArg` when you only have an expression to
+  refined, and not a type with a value.
+
+  This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive
+  calls to refine the functions' paramter, which may mention `major`.
+  See there for how to use this function.
+
+  It returns an open term, rather than following the idiom of applying a continuation,
+  so that `CasesOn.refineThrough?` can reliably recognize failure from within this function.
+-/
+def CasesOnApp.refineThrough (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) :=
+  lambdaTelescope c.motive fun motiveArgs _motiveBody => do
+    unless motiveArgs.size == c.indices.size + 1 do
+      throwError "failed to transfer argument through `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders"
+    let discrs := c.indices ++ #[c.major]
+    let mut eAbst := e
+    for motiveArg in motiveArgs.reverse, discr in discrs.reverse do
+      eAbst ← kabstract eAbst discr
+      eAbst := eAbst.instantiate1 motiveArg
+    -- Let's create something that’s a `Sort` and mentions `e`
+    -- (recall that `e` itself possibly isn't a type),
+    -- by writing `e = e`, so that we can use it as a motive
+    let eEq ← mkEq eAbst eAbst
+    let motive ← mkLambdaFVars motiveArgs eEq
+    let us := if c.propOnly then c.us else levelZero :: c.us.tail!
+    -- Now instantiate the casesOn wth this synthetic motive
+    let aux := mkAppN (mkConst c.declName us) c.params
+    let aux := mkApp aux motive
+    let aux := mkAppN aux discrs
+    check aux
+    let auxType ← inferType aux
+    -- The type of the remaining arguments will mention `e` instantiated for each arg
+    -- so extract them
+    forallTelescope auxType fun altAuxs _ => do
+      let altAuxTys ← altAuxs.mapM (inferType ·)
+      (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do
+        forallTelescope altAuxTy fun fvs body => do
+          unless fvs.size = altNumParams do
+            throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments"
+          -- extract type from our synthetic equality
+          let body := body.getArg! 2
+          -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out
+          Expr.abstractM body fvs
+
+/-- A non-failing version of `CasesOnApp.refineThrough` -/
+def CasesOnApp.refineThrough? (c : CasesOnApp) (e : Expr) :
+    MetaM (Option (Array Expr)) :=
+  try
+    return some (← c.refineThrough e)
+  catch _ =>
+    return none
+
 end Lean.Meta
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index b4ce22790431..00295e4cc1dc 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -910,11 +910,17 @@ private partial def updateAlts (typeNew : Expr) (altNumParams : Array Nat) (alts
   - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and
   - expression `e : B[discrs]`,
   Construct the term
-  `match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`, and
+  `match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`.
+
   We use `kabstract` to abstract the discriminants from `B[discrs]`.
+
   This method assumes
   - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size`
   - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]`
+
+  This is used in in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to
+  the argument provided by `fix` to refine the termination argument, which may mention `major`.
+  See there for how to use this function.
 -/
 def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
   lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
@@ -951,13 +957,80 @@ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
       remaining     := #[e] ++ matcherApp.remaining
     }
 
-/-- Similar `MatcherApp.addArg?`, but returns `none` on failure. -/
+/-- Similar to `MatcherApp.addArg`, but returns `none` on failure. -/
 def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option MatcherApp) :=
   try
     return some (← matcherApp.addArg e)
   catch _ =>
     return none
 
+
+/-- Given
+  - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and
+  - a type `B[discrs]` (which may not be a type, e.g. `n : Nat`),
+  returns the types `B[C_1[ys_1]] ... B[C_n[ys_n]]`,
+  with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `matcherApp.altNumParams`.
+
+  This method assumes
+  - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size`
+  - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]`
+
+  This is similar to `MatcherApp.addArg` when you only have an expression to
+  refined, and not a type with a value.
+
+  This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive
+  calls to refine the functions' paramter, which may mention `major`.
+  See there for how to use this function.
+
+  It returns an open term, rather than following the idiom of applying a continuation,
+  so that `MatcherApp.refineThrough?` can reliably recognize failure from within this function
+-/
+def MatcherApp.refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) :=
+  lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do
+    unless motiveArgs.size == matcherApp.discrs.size do
+      -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`.
+      throwError "failed to transfer argument through matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments"
+
+    let eAbst ← matcherApp.discrs.size.foldRevM (init := e) fun i eAbst => do
+      let motiveArg := motiveArgs[i]!
+      let discr     := matcherApp.discrs[i]!
+      let eTypeAbst ← kabstract eAbst discr
+      return eTypeAbst.instantiate1 motiveArg
+    -- Let's create something that’s a `Sort` and mentions `e`
+    -- (recall that `e` itself possibly isn't a type),
+    -- by writing `e = e`, so that we can use it as a motive
+    let eEq ← mkEq eAbst eAbst
+
+    let matcherLevels ← match matcherApp.uElimPos? with
+      | none     => pure matcherApp.matcherLevels
+      | some pos =>
+        pure <| matcherApp.matcherLevels.set! pos levelZero
+    let motive ← mkLambdaFVars motiveArgs eEq
+    let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params
+    let aux := mkApp aux motive
+    let aux := mkAppN aux matcherApp.discrs
+    unless (← isTypeCorrect aux) do
+      throwError "failed to transfer argument through matcher application, type error when constructing the new motive"
+    let auxType ← inferType aux
+    forallTelescope auxType fun altAuxs _ => do
+      let altAuxTys ← altAuxs.mapM (inferType ·)
+      (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do
+        forallTelescope altAuxTy fun fvs body => do
+          unless fvs.size = altNumParams do
+            throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments"
+          -- extract type from our synthetic equality
+          let body := body.getArg! 2
+          -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out
+          Expr.abstractM body fvs
+
+/-- A non-failing version of `MatcherApp.refineThrough` -/
+def MatcherApp.refineThrough? (matcherApp : MatcherApp) (e : Expr) :
+    MetaM (Option (Array Expr)) :=
+  try
+    return some (← matcherApp.refineThrough e)
+  catch _ =>
+    return none
+
 builtin_initialize
   registerTraceClass `Meta.Match.match
   registerTraceClass `Meta.Match.debug
diff --git a/tests/lean/guessLexFailures.lean b/tests/lean/guessLexFailures.lean
new file mode 100644
index 000000000000..28e7bff8d5cd
--- /dev/null
+++ b/tests/lean/guessLexFailures.lean
@@ -0,0 +1,34 @@
+/-!
+A few cases where guessing the lexicographic order fails, and
+where we want to keep tabs on the output.
+-/
+
+def nonTerminating : Nat → Nat
+  | 0 => 0
+  | n => nonTerminating (.succ n)
+
+-- Saying decreasing_by forces Lean to use structural recursion, which gives a different
+-- error message
+def nonTerminating2 : Nat → Nat
+  | 0 => 0
+  | n => nonTerminating2 (.succ n)
+decreasing_by decreasing_tactic
+
+
+-- The GuessLex code does not like eta-contracted motives in `casesOn`.
+-- At the time of writing, the error message is swallowed
+-- When guessing the lexicographic order becomes more verbose this will improve.
+def FinPlus1 n := Fin (n + 1)
+def badCasesOn (n : Nat) : Fin (n + 1) :=
+   Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn n))
+decreasing_by decreasing_tactic
+-- termination_by badCasesOn n => n
+
+
+-- Like above, but now with a `casesOn` alternative with insufficient lambdas
+def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) := fun n => Fin.succ (f n)
+def badCasesOn2 (n : Nat) : Fin (n + 1) :=
+   Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩)
+      (Fin_succ_comp (fun n => badCasesOn2 n))
+decreasing_by decreasing_tactic
+-- termination_by badCasesOn2 n => n
diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out
new file mode 100644
index 000000000000..d170019599cb
--- /dev/null
+++ b/tests/lean/guessLexFailures.lean.expected.out
@@ -0,0 +1,13 @@
+guessLexFailures.lean:8:9-8:33: error: fail to show termination for
+  nonTerminating
+with errors
+argument #1 was not used for structural recursion
+  failed to eliminate recursive application
+    nonTerminating (Nat.succ n)
+
+structural recursion cannot be used
+
+failed to prove termination, use `termination_by` to specify a well-founded relation
+guessLexFailures.lean:12:0-15:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation
+guessLexFailures.lean:22:0-24:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation
+guessLexFailures.lean:30:0-33:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation
diff --git a/tests/lean/run/guessLex.lean b/tests/lean/run/guessLex.lean
new file mode 100644
index 000000000000..993ccddc1b33
--- /dev/null
+++ b/tests/lean/run/guessLex.lean
@@ -0,0 +1,109 @@
+/-!
+This files tests Lean's ability to guess the right lexicographic order.
+
+TODO: Once lean spits out the guessed order (probably guarded by an
+option), turn this on and check the output.
+-/
+
+def ackermann (n m : Nat) := match n, m with
+  | 0, m => m + 1
+  | .succ n, 0 => ackermann n 1
+  | .succ n, .succ m => ackermann n (ackermann (n + 1) m)
+
+def ackermann2 (n m : Nat) := match n, m with
+  | m, 0 => m + 1
+  | 0, .succ n => ackermann2 1 n
+  | .succ m, .succ n => ackermann2 (ackermann2 m (n + 1)) n
+
+def ackermannList (n m : List Unit) := match n, m with
+  | [], m => () :: m
+  | ()::n, [] => ackermannList n [()]
+  | ()::n, ()::m => ackermannList n (ackermannList (()::n) m)
+
+def foo2 : Nat → Nat → Nat
+  | .succ n, 1 => foo2 n 1
+  | .succ n, 2 => foo2 (.succ n) 1
+  | n,       3 => foo2 (.succ n) 2
+  | .succ n, 4 => foo2 (if n > 10 then n else .succ n) 3
+  | n,       5 => foo2 (n - 1) 4
+  | n, .succ m => foo2 n m
+  | _, _ => 0
+
+mutual
+def even : Nat → Bool
+  | 0 => true
+  | .succ n => not (odd n)
+def odd : Nat → Bool
+  | 0 => false
+  | .succ n => not (even n)
+end
+
+mutual
+def evenWithFixed (m : String) : Nat → Bool
+  | 0 => true
+  | .succ n => not (oddWithFixed m n)
+def oddWithFixed (m : String) : Nat → Bool
+  | 0 => false
+  | .succ n => not (evenWithFixed m n)
+end
+
+def ping (n : Nat) := pong n
+   where pong : Nat → Nat
+  | 0 => 0
+  | .succ n => ping n
+
+def hasForbiddenArg (n : Nat) (_h : n = n) (m : Nat) : Nat :=
+  match n, m with
+  | 0, 0 => 0
+  | .succ m, n => hasForbiddenArg m rfl n
+  | m, .succ n => hasForbiddenArg (.succ m) rfl n
+
+/-!
+Example from “Finding Lexicographic Orders for Termination Proofs in
+Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow,
+10.1007/978-3-540-74591-4_5
+-/
+def blowup : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat
+  | 0, 0, 0, 0, 0, 0, 0, 0 => 0
+  | 0, 0, 0, 0, 0, 0, 0, .succ i => .succ (blowup i i i i i i i i)
+  | 0, 0, 0, 0, 0, 0, .succ h, i => .succ (blowup h h h h h h h i)
+  | 0, 0, 0, 0, 0, .succ g, h, i => .succ (blowup g g g g g g h i)
+  | 0, 0, 0, 0, .succ f, g, h, i => .succ (blowup f f f f f g h i)
+  | 0, 0, 0, .succ e, f, g, h, i => .succ (blowup e e e e f g h i)
+  | 0, 0, .succ d, e, f, g, h, i => .succ (blowup d d d e f g h i)
+  | 0, .succ c, d, e, f, g, h, i => .succ (blowup c c d e f g h i)
+  | .succ b, c, d, e, f, g, h, i => .succ (blowup b c d e f g h i)
+
+-- Let’s try to confuse the lexicographic guessing function's
+-- unpacking of packed n-ary arguments
+def confuseLex1 : Nat → @PSigma Nat (fun _ => Nat) → Nat
+  | 0, _p => 0
+  | .succ n, ⟨x,y⟩ => confuseLex1 n ⟨x,y⟩
+
+def confuseLex2 : @PSigma Nat (fun _ => Nat) → Nat
+  | ⟨_y,0⟩ => 0
+  | ⟨y,.succ n⟩ => confuseLex2 ⟨y,n⟩
+
+def dependent : (n : Nat) → (m : Fin n) → Nat
+ | 0, i => Fin.elim0 i
+ | .succ 0, 0 => 0
+ | .succ (.succ n), 0 => dependent (.succ n) ⟨n, n.lt_succ_self⟩
+ | .succ (.succ n), ⟨.succ m, h⟩ =>
+  dependent (.succ (.succ n)) ⟨m, Nat.lt_of_le_of_lt (Nat.le_succ _) h⟩
+
+
+-- An example based on a real world problem, condensed by Leo
+inductive Expr where
+  | add (a b : Expr)
+  | val (n : Nat)
+
+mutual
+def eval (a : Expr) : Nat :=
+  match a with
+  | .add x y => eval_add (x, y)
+  | .val n => n
+
+def eval_add (a : Expr × Expr) : Nat :=
+  match a with
+  | (x, y) => eval x + eval y
+end
diff --git a/tests/lean/run/guessLexTricky.lean b/tests/lean/run/guessLexTricky.lean
new file mode 100644
index 000000000000..b4f4298d0a09
--- /dev/null
+++ b/tests/lean/run/guessLexTricky.lean
@@ -0,0 +1,51 @@
+/-!
+A “tricky” example from “Finding Lexicographic Orders for Termination Proofs in
+Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow,
+10.1007/978-3-540-74591-4_5
+
+At the time of writing, Lean is able to find the lexicographic order
+just fine, but only if the tactic is powerful enough. In partiuclar,
+the default `decreasing_tactic` can only handle lexicographic descend when either
+the left gets smaller, or the left stays equal and the right gets smaller.
+But here we need to allow the general form, where the left is ≤ and the right
+gets smaller. This needs a backtracking proof search, it seems, which we build here
+(`search_lex`).
+-/
+
+macro_rules | `(tactic| decreasing_trivial) =>
+              `(tactic| apply Nat.le_refl)
+macro_rules | `(tactic| decreasing_trivial) =>
+              `(tactic| apply Nat.succ_lt_succ; decreasing_trivial)
+macro_rules | `(tactic| decreasing_trivial) =>
+              `(tactic| apply Nat.sub_le)
+macro_rules | `(tactic| decreasing_trivial) =>
+              `(tactic| apply Nat.div_le_self)
+
+syntax "search_lex " tacticSeq : tactic
+
+macro_rules | `(tactic|search_lex $ts:tacticSeq) => `(tactic| (
+    solve
+    | apply Prod.Lex.right'
+      · $ts
+      · search_lex $ts
+    | apply Prod.Lex.left
+      · $ts
+    | $ts
+    ))
+
+-- set_option trace.Elab.definition.wf true in
+mutual
+def prod (x y z : Nat) : Nat :=
+  if y % 2 = 0 then eprod x y z else oprod x y z
+def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
+def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
+end
+-- termination_by
+--   prod x y z => (y, 2)
+--   oprod x y z => (y, 1)
+--   eprod x y z => (y, 0)
+decreasing_by
+  simp_wf
+  search_lex solve
+    | decreasing_trivial
+    | apply Nat.bitwise_rec_lemma; assumption
diff --git a/tests/lean/run/guessLexTricky2.lean b/tests/lean/run/guessLexTricky2.lean
new file mode 100644
index 000000000000..54136a75ea4c
--- /dev/null
+++ b/tests/lean/run/guessLexTricky2.lean
@@ -0,0 +1,23 @@
+/-!
+Another “tricky” example from “Finding Lexicographic Orders for Termination Proofs in
+Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow,
+10.1007/978-3-540-74591-4_5.
+
+Works out of the box!
+-/
+
+mutual
+def pedal : Nat → Nat → Nat → Nat
+  | 0, _m, c => c
+  | _n, 0, c => c
+  | n+1, m+1, c =>
+    if n < m
+    then coast n m (c + m + 1)
+    else pedal n (m + 1) (c + m + 1)
+
+def coast : Nat → Nat → Nat → Nat
+  | n, m , c =>
+  if n < m
+  then coast n (m - 1) (c + n)
+  else pedal n m (c + n)
+end