diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index a74030a724..0d89b6e5e8 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -207,6 +207,8 @@ def SavedLocalContext.run {α} (slc : SavedLocalContext) (k : MetaM α) :
 /-- 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
+  /-- Syntax location of reursive call -/
+  ref : Syntax
   /-- Function index of caller -/
   caller : Nat
   /-- Parameters of caller -/
@@ -218,9 +220,9 @@ structure RecCallWithContext where
   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) }
+def RecCallWithContext.create (ref : Syntax) (caller : Nat) (params : Array Expr) (callee : Nat)
+    (args : Array Expr) : MetaM RecCallWithContext := do
+  return { ref, 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.
@@ -273,18 +275,21 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti
       let arg := args[fixedPrefixSize]!
       let (caller, params) ← unpackArg arities param
       let (callee, args) ← unpackArg arities arg
-      RecCallWithContext.create caller params callee args
+      RecCallWithContext.create (← getRef) 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 : ToString GuessLexRel where
+  toString | .lt => "<"
+           | .eq => "="
+           | .le => "≤"
+           | .no_idea => "?"
+
 instance : ToFormat GuessLexRel where
-  format | .lt => "<"
-         | .eq => "="
-         | .le => "≤"
-         | .no_idea => "?"
+  format r := toString r
 
 /-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly. -/
 def GuessLexRel.toNatRel : GuessLexRel → Expr
@@ -370,16 +375,13 @@ def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLe
     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
+
+/-- Print a single cache entry as a string, without forcing it -/
+def RecCallCache.prettyEntry (rcc : RecCallCache) (paramIdx argIdx : Nat) : MetaM String := do
+  let cachedEntries ← rcc.cache.get
+  return match cachedEntries[paramIdx]![argIdx]! with
+  | .some rel => toString rel
+  | .none => "_"
 
 /-- The measures that we order lexicographically can be comparing arguments,
 or numbering the functions -/
@@ -551,6 +553,103 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
       }
   return .ext termByElements
 
+
+/--
+Given a matrix (row-major) of strings, arranges them in tabular form.
+First column is left-aligned, others right-aligned.
+Single space as column separator.
+-/
+def formatTable : Array (Array String) → String := fun xss => Id.run do
+  let mut colWidths := xss[0]!.map (fun _ => 0)
+  for i in [:xss.size] do
+    for j in [:xss[i]!.size] do
+      if xss[i]![j]!.length > colWidths[j]! then
+        colWidths := colWidths.set! j xss[i]![j]!.length
+  let mut str := ""
+  for i in [:xss.size] do
+    for j in [:xss[i]!.size] do
+      let s := xss[i]![j]!
+      if j > 0 then -- right-align
+        for _ in [:colWidths[j]! - s.length] do
+          str := str ++ " "
+      str := str ++ s
+      if j = 0 then -- left-align
+        for _ in [:colWidths[j]! - s.length] do
+          str := str ++ " "
+      if j + 1 < xss[i]!.size then
+        str := str ++ " "
+    if i + 1 < xss.size then
+      str := str ++ "\n"
+  return str
+
+/-- Concise textual representation of the source location of a recursive call  -/
+def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
+  let fileMap ← getFileMap
+  let .some pos := rcc.ref.getPos? | return ""
+  let position := fileMap.toPosition pos
+  let endPosStr := match rcc.ref.getTailPos? with
+  | some endPos =>
+    let endPosition := fileMap.toPosition endPos
+    if endPosition.line = position.line then
+      s!"-{endPosition.column}"
+    else
+      s!"-{endPosition.line}:{endPosition.column}"
+  | none        => ""
+  return s!"{position.line}:{position.column}{endPosStr}"
+
+
+/-- Explain what we found out about the recursive calls (non-mutual case) -/
+def explainNonMutualFailure (varNames : Array Name) (rcs : Array RecCallCache) : MetaM Format := do
+  let header := varNames.map (·.eraseMacroScopes.toString)
+  let mut table : Array (Array String) := #[#[""] ++ header]
+  for i in [:rcs.size], rc in rcs do
+    let mut row := #[s!"{i+1}) {← rc.rcc.posString}"]
+    for argIdx in [:varNames.size] do
+      row := row.push (← rc.prettyEntry argIdx argIdx)
+    table := table.push row
+
+  return formatTable table
+
+/-- Explain what we found out about the recursive calls (mutual case) -/
+def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name))
+    (rcs : Array RecCallCache) : MetaM Format := do
+  let mut r := Format.nil
+
+  for rc in rcs do
+    let caller := rc.rcc.caller
+    let callee := rc.rcc.callee
+    r := r ++ f!"Call from {declNames[caller]!} to {declNames[callee]!} " ++
+      f!"at {← rc.rcc.posString}:\n"
+
+    let header := varNamess[caller]!.map (·.eraseMacroScopes.toString)
+    let mut table : Array (Array String) := #[#[""] ++ header]
+    if caller = callee then
+      -- For self-calls, only the diagonal is interesting, so put it into one row
+      let mut row := #[""]
+      for argIdx in [:varNamess[caller]!.size] do
+        row := row.push (← rc.prettyEntry argIdx argIdx)
+      table := table.push row
+    else
+      for argIdx in [:varNamess[callee]!.size] do
+        let mut row := #[]
+        row := row.push varNamess[callee]![argIdx]!.eraseMacroScopes.toString
+        for paramIdx in [:varNamess[caller]!.size] do
+          row := row.push (← rc.prettyEntry paramIdx argIdx)
+        table := table.push row
+    r := r ++ formatTable table ++ "\n"
+
+  return r
+
+def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
+    (rcs : Array RecCallCache) : MetaM Format := do
+  let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++
+    "(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
+  if declNames.size = 1 then
+    r := r ++ (← explainNonMutualFailure varNamess[0]! rcs)
+  else
+    r := r ++ (← explainMutualFailure declNames varNamess rcs)
+  return r
+
 end Lean.Elab.WF.GuessLex
 
 namespace Lean.Elab.WF
@@ -566,33 +665,32 @@ 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}"
+  let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
+  let arities := varNamess.map (·.size)
+  trace[Elab.definition.wf] "varNames is: {varNamess}"
 
-    let forbiddenArgs ← preDefs.mapM fun preDef =>
-      getForbiddenByTrivialSizeOf fixedPrefixSize preDef
+  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
+  -- The list of measures, including the measures that order functions.
+  -- The function ordering measures come last
+  let measures ← generateMeasures forbiddenArgs arities
 
-    -- If there is only one plausible measure, use that
-    if let #[solution] := measures then
-      return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution]
+  -- If there is only one plausible measure, use that
+  if let #[solution] := measures then
+    return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution]
 
-    -- 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 ·)
+  -- 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 ·)
 
-    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"
+  match ← liftMetaM <| solve measures callMatrix with
+  | .some solution => do
+    let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
+    return wf
+  | .none =>
+    let explanation ← explainFailure (preDefs.map (·.declName)) varNamess rcs
+    Lean.throwError <| "Could not find a decreasing measure.\n" ++
+      explanation ++ "\n" ++
+      "Please use `termination_by` to specify a decreasing measure."
diff --git a/tests/lean/guessLexFailures.lean b/tests/lean/guessLexFailures.lean
index b7f745d019..384eb0e90c 100644
--- a/tests/lean/guessLexFailures.lean
+++ b/tests/lean/guessLexFailures.lean
@@ -17,21 +17,117 @@ def nonTerminating2 : Nat → Nat → Nat
   | n, m => nonTerminating2 (.succ n) (.succ m)
 decreasing_by decreasing_tactic
 
+def noArguments : Nat := noArguments
 
--- 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 noNonFixedArguments (n : Nat) : Nat := noNonFixedArguments n
+
+def Array.sum (xs : Array Nat) : Nat := xs.foldl (init := 0) Nat.add
+
+namespace InterestingMatrix
+def f : (n m l : Nat) → Nat
+  | n+1, m+1, l+1 => #[
+      f (n+1) (m+1) (l+1),
+      f (n+1) (m-1) (l),
+      f (n)   (m+1) (l) ].sum
+  | _, _, _ => 0
+decreasing_by decreasing_tactic
+end InterestingMatrix
+
+namespace InterestingMatrixWithForbiddenArguments
+def f : (n m : Nat) → (h : True) → Nat → Nat
+  | n+1, m+1, h, l+1 => #[
+      f (n+1) (m+1) h (l+1),
+      f (n+1) (m-1) h (l),
+      f (n)   (m+1) h (l) ].sum
+  | _, _, _, _ => 0
+decreasing_by decreasing_tactic
+end InterestingMatrixWithForbiddenArguments
+
+namespace InterestingMatrixWithNames
+-- Hopefully eventually lean will pick up names even with pattern match syntax
+def f (n m l : Nat) : Nat := match n, m, l with
+  | n+1, m+1, l+1 => #[
+      f (n+1) (m+1) (l+1),
+      f (n+1) (m-1) (l),
+      f (n)   (m+1) (l) ].sum
+  | _, _, _ => 0
+decreasing_by decreasing_tactic
+end InterestingMatrixWithNames
+
+namespace Mutual
+mutual
+  def f (fixed n m l : Nat) : Nat := match n, m, l with
+    | n+1, m+1, l+1 => #[
+        f fixed (n+1) (m+1) (l+1),
+        f fixed (n+1) (m-1) (l),
+        g fixed (n)   (m+1) trivial (l)].sum
+    | _, _, _ => 0
+
+  def g (fixed n m : Nat) (H : True) (l : Nat) : Nat := match n, m, l with
+    | n+1, m+1, l+1 => #[
+        g fixed (m+1) (n+1) H (l+1),
+        g fixed (m+1) (n-1) H (l),
+        h fixed (m)   (n+1)  ].sum
+    | _, _, _ => 0
+
+  def h (fixed : Nat) : (n m : Nat) -> Nat
+    | n+1, m+1 => #[
+        f fixed (n+1) (m+1) (n+1),
+        h fixed (n+1) (m-1),
+        h fixed (n)   (m+1) ].sum
+    | _, _ => 0
+end
+end Mutual
+
+
+namespace DuplicatedCall
+
+def dup (a : Nat) (b : Nat := a) := a + b
+
+def f : (n m : Nat) → Nat
+  | 0, m => m
+  | n+1, m => dup (f (n+2) (m+1))
+
+end DuplicatedCall
+
+namespace TrickyCode
+
+-- These tests run GuessLex on peculiar code that it once stumbled over, or might
+-- stumble over in the future.
+
+-- The GuessLex code at some point did not like eta-contracted motives in `casesOn`.
 def FinPlus1 n := Fin (n + 1)
 def badCasesOn (n m : Nat) : Fin (n + 1) :=
    Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn n (.succ m)))
+-- termination_by badCasesOn n m => 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)
+-- This actually also fails with an explicit termination_by, and could be fixed
+-- by eta-expanding the motive.
+-- TODO: Fix by using eta-expanding variant of lambdaTelescope, e.g.
+-- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Going.20under.20exactly.20one.20lambda/near/404278529
 def badCasesOn2 (n m : 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 (.succ m)))
+   Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn2 n (.succ m)))
+termination_by badCasesOn2 n m => n
 decreasing_by decreasing_tactic
--- termination_by badCasesOn2 n => n
+
+-- The GuessLex code at does not like `casesOn` alternative with insufficient lambdas
+-- TODO: Fix by using eta-expanding variant of lambdaTelescope, e.g.
+-- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Going.20under.20exactly.20one.20lambda/near/404278529
+def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) := fun n => Fin.succ (f n)
+def badCasesOn3 (n m : Nat) : Fin (n + 1) :=
+   Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩)
+      (Fin_succ_comp (fun n => badCasesOn3 n (.succ m)))
+-- termination_by badCasesOn3 n m => n
+decreasing_by decreasing_tactic
+
+
+-- Same test, explicit termination_by
+def badCasesOn4 (n m : Nat) : Fin (n + 1) :=
+   Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩)
+      (Fin_succ_comp (fun n => badCasesOn4 n (.succ m)))
+termination_by badCasesOn4 n m => n
+decreasing_by decreasing_tactic
+
+end TrickyCode
diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out
index 5890ef5bf3..f70c3d67b3 100644
--- a/tests/lean/guessLexFailures.lean.expected.out
+++ b/tests/lean/guessLexFailures.lean.expected.out
@@ -11,7 +11,140 @@ argument #2 was not used for structural recursion
 
 structural recursion cannot be used
 
-failed to prove termination, use `termination_by` to specify a well-founded relation
-guessLexFailures.lean:15:0-18:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation
-guessLexFailures.lean:25:0-27:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation
-guessLexFailures.lean:33:0-36:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation
+Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+            x1 x2
+1) 11:12-46  ?  ?
+Please use `termination_by` to specify a decreasing measure.
+guessLexFailures.lean:15:0-18:31: error: Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+            x1 x2
+1) 17:12-47  ?  ?
+Please use `termination_by` to specify a decreasing measure.
+guessLexFailures.lean:20:4-20:15: error: fail to show termination for
+  noArguments
+with errors
+structural recursion cannot be used
+
+well-founded recursion cannot be used, 'noArguments' does not take any (non-fixed) arguments
+guessLexFailures.lean:22:4-22:23: error: fail to show termination for
+  noNonFixedArguments
+with errors
+structural recursion cannot be used
+
+well-founded recursion cannot be used, 'noNonFixedArguments' does not take any (non-fixed) arguments
+guessLexFailures.lean:27:0-33:31: error: Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+           x1 x2 x3
+1) 29:6-25  =  =  =
+2) 30:6-23  =  ?  <
+3) 31:6-23  <  _  _
+Please use `termination_by` to specify a decreasing measure.
+guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+           x1 x2 x3 x4
+1) 39:6-27  =  =  _  =
+2) 40:6-25  =  ?  _  <
+3) 41:6-25  <  _  _  _
+Please use `termination_by` to specify a decreasing measure.
+guessLexFailures.lean:48:0-54:31: error: Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+           n m l
+1) 50:6-25 = = =
+2) 51:6-23 = ? <
+3) 52:6-23 < _ _
+Please use `termination_by` to specify a decreasing measure.
+guessLexFailures.lean:59:6-59:7: error: fail to show termination for
+  Mutual.f
+  Mutual.g
+  Mutual.h
+with errors
+structural recursion does not handle mutually recursive functions
+
+Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+Call from Mutual.f to Mutual.f at 61:8-33:
+ n m l
+ = = =
+Call from Mutual.f to Mutual.f at 62:8-31:
+ n m l
+ = ? <
+Call from Mutual.f to Mutual.g at 63:8-39:
+  n m l
+n < _ ?
+m ? _ ?
+H _ _ _
+l ? _ <
+Call from Mutual.g to Mutual.g at 68:8-35:
+ n m H l
+ ? _ _ =
+Call from Mutual.g to Mutual.g at 69:8-33:
+ n m H l
+ _ _ _ <
+Call from Mutual.g to Mutual.h at 70:8-27:
+   n m H l
+x1 _ _ _ ?
+x2 _ _ _ ?
+Call from Mutual.h to Mutual.f at 75:8-33:
+  x1 x2
+n  _  _
+m  _  _
+l  _  _
+Call from Mutual.h to Mutual.h at 76:8-27:
+ x1 x2
+  _  _
+Call from Mutual.h to Mutual.h at 77:8-27:
+ x1 x2
+  _  _
+
+Please use `termination_by` to specify a decreasing measure.
+guessLexFailures.lean:89:19-89:32: error: fail to show termination for
+  DuplicatedCall.f
+with errors
+argument #1 was not used for structural recursion
+  failed to eliminate recursive application
+    DuplicatedCall.f (n + 2) (m + 1)
+
+argument #2 was not used for structural recursion
+  failed to eliminate recursive application
+    DuplicatedCall.f (n + 2) (m + 1)
+
+structural recursion cannot be used
+
+Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+            x1 x2
+1) 89:19-32  ?  ?
+2) 89:19-32  _  _
+Please use `termination_by` to specify a decreasing measure.
+guessLexFailures.lean:100:0-103:31: error: Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+              n m
+1) 101:83-105 ? ?
+Please use `termination_by` to specify a decreasing measure.
+guessLexFailures.lean:113:14-113:31: error: failed to prove termination, possible solutions:
+  - Use `have`-expressions to prove the remaining goals
+  - Use `termination_by` to specify a different well-founded relation
+  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
+n✝ m n : Nat
+⊢ n < n✝
+guessLexFailures.lean:119:0-123:31: error: Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+             n m
+1) 121:31-54 ? ?
+Please use `termination_by` to specify a decreasing measure.
+guessLexFailures.lean:131:14-131:31: error: failed to prove termination, possible solutions:
+  - Use `have`-expressions to prove the remaining goals
+  - Use `termination_by` to specify a different well-founded relation
+  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
+m n✝ n : Nat
+⊢ n < Nat.succ n✝
diff --git a/tests/lean/terminationFailure.lean.expected.out b/tests/lean/terminationFailure.lean.expected.out
index dae6521399..e2951ec50d 100644
--- a/tests/lean/terminationFailure.lean.expected.out
+++ b/tests/lean/terminationFailure.lean.expected.out
@@ -4,7 +4,17 @@ terminationFailure.lean:7:2-7:3: error: fail to show termination for
 with errors
 structural recursion does not handle mutually recursive functions
 
-failed to prove termination, use `termination_by` to specify a well-founded relation
+Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+Call from f.g to f at 9:9-12:
+  x1
+x  =
+Call from f to f.g at 3:4-7:
+   x
+x1 =
+
+Please use `termination_by` to specify a decreasing measure.
 f (x : Nat) : Nat
 f.g (a✝ : Nat) : Nat
 1
diff --git a/tests/lean/wf1.lean.expected.out b/tests/lean/wf1.lean.expected.out
index 761deed9fb..6d61955c30 100644
--- a/tests/lean/wf1.lean.expected.out
+++ b/tests/lean/wf1.lean.expected.out
@@ -11,4 +11,9 @@ argument #2 was not used for structural recursion
 
 structural recursion cannot be used
 
-failed to prove termination, use `termination_by` to specify a well-founded relation
+Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+           x y
+1) 3:12-19 ? ?
+Please use `termination_by` to specify a decreasing measure.