diff --git a/RELEASES.md b/RELEASES.md
index 6ed853ec98..eb4c13e765 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -65,6 +65,133 @@ example : x + foo 2 = 12 + x := by
   simp_arith
 ```
 
+* The syntax of the `termination_by` and `decreasing_by` termination hints is overhauled:
+
+  * They are now placed directly after the function they apply to, instead of
+    after the whole `mutual` block.
+  * Therefore, the function name no longer has to be mentioned in the hint.
+  * If the function has a `where` clause, the `termination_by` and
+    `decreasing_by` for that function come before the `where`. The
+    functions in the `where` clause can have their own termination hints, each
+    following the corresponding definition.
+  * The `termination_by` clause can only bind “extra parameters”, that are not
+    already bound by the function header, but are bound in a lambda (`:= fun x
+    y z =>`) or in patterns (`| x, n + 1 => …`). These extra parameters used to
+    be understood as a suffix of the function parameters; now it is a prefix.
+
+  Migration guide: In simple cases just remove the function name, and any
+  variables already bound at the header.
+  ```diff
+   def foo : Nat → Nat → Nat := …
+  -termination_by foo a b => a - b
+  +termination_by a b => a - b
+  ```
+  or
+  ```diff
+   def foo : Nat → Nat → Nat := …
+  -termination_by _ a b => a - b
+  +termination_by a b => a - b
+  ```
+
+  If the parameters are bound in the function header (before the `:`), remove them as well:
+  ```diff
+   def foo (a b : Nat) : Nat := …
+  -termination_by foo a b => a - b
+  +termination_by a - b
+  ```
+
+  Else, if there are multiple extra parameters, make sure to refer to the right
+  ones; the bound variables are interpreted from left to right, no longer from
+  right to left:
+  ```diff
+   def foo : Nat → Nat → Nat → Nat
+     | a, b, c => …
+  -termination_by foo b c => b
+  +termination_by a b => b
+  ```
+
+  In the case of a `mutual` block, place the termination arguments (without the
+  function name) next to the function definition:
+  ```diff
+  -mutual
+  -def foo : Nat → Nat → Nat := …
+  -def bar : Nat → Nat := …
+  -end
+  -termination_by
+  -  foo a b => a - b
+  -  bar a => a
+  +mutual
+  +def foo : Nat → Nat → Nat := …
+  +termination_by a b => a - b
+  +def bar : Nat → Nat := …
+  +termination_by a => a
+  +end
+  ```
+
+  Similarly, if you have (mutual) recursion through `where` or `let rec`, the
+  termination hints are now placed directly after the function they apply to:
+  ```diff
+  -def foo (a b : Nat) : Nat := …
+  -  where bar (x : Nat) : Nat := …
+  -termination_by
+  -  foo a b => a - b
+  -  bar x => x
+  +def foo (a b : Nat) : Nat := …
+  +termination_by a - b
+  +  where
+  +    bar (x : Nat) : Nat := …
+  +    termination_by x
+
+  -def foo (a b : Nat) : Nat :=
+  -  let rec bar (x : Nat) :  Nat := …
+  -  …
+  -termination_by
+  -  foo a b => a - b
+  -  bar x => x
+  +def foo (a b : Nat) : Nat :=
+  +  let rec bar (x : Nat) : Nat := …
+  +    termination_by x
+  +  …
+  +termination_by a - b
+  ```
+
+  In cases where a single `decreasing_by` clause applied to multiple mutually
+  recursive functions before, the tactic now has to be duplicated.
+
+* The semantics of `decreasing_by` changed; the tactic is applied to all
+  termination proof goals together, not individually.
+
+  This helps when writing termination proofs interactively, as one can focus
+  each subgoal individually, for example using `·`. Previously, the given
+  tactic script had to work for _all_ goals, and one had to resort to tactic
+  combinators like `first`:
+
+  ```diff
+   def foo (n : Nat) := … foo e1 … foo e2 …
+  -decreasing_by
+  -simp_wf
+  -first | apply something_about_e1; …
+  -      | apply something_about_e2; …
+  +decreasing_by
+  +all_goals simp_wf
+  +· apply something_about_e1; …
+  +· apply something_about_e2; …
+  ```
+
+  To obtain the old behaviour of applying a tactic to each goal individually,
+  use `all_goals`:
+  ```diff
+   def foo (n : Nat) := …
+  -decreasing_by some_tactic
+  +decreasing_by all_goals some_tactic
+  ```
+
+  In the case of mutual recursion each `decreasing_by` now applies to just its
+  function. If some functions in a recursive group do not have their own
+  `decreasing_by`, the default `decreasing_tactic` is used. If the same tactic
+  ought to be applied to multiple functions, the `decreasing_by` clause has to
+  be repeated at each of these functions.
+
 
 v4.5.0
 ---------
@@ -88,7 +215,7 @@ v4.5.0
   Migration guide: Use `termination_by` instead, e.g.:
   ```diff
   -termination_by' measure (fun ⟨i, _⟩ => as.size - i)
-  +termination_by go i _ => as.size - i
+  +termination_by i _ => as.size - i
   ```
 
   If the well-founded relation you want to use is not the one that the
@@ -96,7 +223,7 @@ v4.5.0
   you can use `WellFounded.wrap` from the std libarary to explicitly give one:
   ```diff
   -termination_by' ⟨r, hwf⟩
-  +termination_by _ x => hwf.wrap x
+  +termination_by x => hwf.wrap x
   ```
 
 * Support snippet edits in LSP `TextEdit`s. See `Lean.Lsp.SnippetString` for more details.
diff --git a/doc/examples/palindromes.lean b/doc/examples/palindromes.lean
index 4d319d9395..59a9ac1a2f 100644
--- a/doc/examples/palindromes.lean
+++ b/doc/examples/palindromes.lean
@@ -82,7 +82,7 @@ theorem List.palindrome_ind (motive : List α → Prop)
     have ih := palindrome_ind motive h₁ h₂ h₃ (a₂::as').dropLast
     have : [a₁] ++ (a₂::as').dropLast ++ [(a₂::as').last (by simp)] = a₁::a₂::as' := by simp
     this ▸ h₃ _ _ _ ih
-termination_by _ as => as.length
+termination_by as.length
 
 /-!
 We use our new induction principle to prove that if `as.reverse = as`, then `Palindrome as` holds.
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 48d9f08c04..8895d18c87 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Elab.Quotation.Precheck
 import Lean.Elab.Term
 import Lean.Elab.BindersUtil
+import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab.Term
 open Meta
@@ -570,7 +571,8 @@ def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM
 -/
 def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
   let matchAlts     := matchAltsWhereDecls[0]
-  let whereDeclsOpt := matchAltsWhereDecls[1]
+  -- matchAltsWhereDecls[1] is the termination hints, collected elsewhere
+  let whereDeclsOpt := matchAltsWhereDecls[2]
   let rec loop (i : Nat) (discrs : Array Syntax) : MacroM Syntax :=
     match i with
     | 0   => do
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 31d7d3d7db..2a6d6ff6f9 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -187,15 +187,6 @@ def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Uni
   let v ← classInductiveSyntaxToView modifiers stx
   elabInductiveViews #[v]
 
-def getTerminationHints (stx : Syntax) : TerminationHints :=
-  let decl := stx[1]
-  let k := decl.getKind
-  if k == ``Parser.Command.def || k == ``Parser.Command.abbrev || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then
-    let args := decl.getArgs
-    { terminationBy? := args[args.size - 2]!.getOptional?, decreasingBy? := args[args.size - 1]!.getOptional? }
-  else
-    {}
-
 @[builtin_command_elab declaration]
 def elabDeclaration : CommandElab := fun stx => do
   match (← liftMacroM <| expandDeclNamespace? stx) with
@@ -219,7 +210,7 @@ def elabDeclaration : CommandElab := fun stx => do
       let modifiers ← elabModifiers stx[0]
       elabStructure modifiers decl
     else if isDefLike decl then
-      elabMutualDef #[stx] (getTerminationHints stx)
+      elabMutualDef #[stx]
     else
       throwError "unexpected declaration"
 
@@ -332,21 +323,10 @@ def expandMutualPreamble : Macro := fun stx =>
 
 @[builtin_command_elab «mutual»]
 def elabMutual : CommandElab := fun stx => do
-  let hints := { terminationBy? := stx[3].getOptional?, decreasingBy? := stx[4].getOptional? }
   if isMutualInductive stx then
-    if let some bad := hints.terminationBy? then
-      throwErrorAt bad "invalid 'termination_by' in mutually inductive datatype declaration"
-    if let some bad := hints.decreasingBy? then
-      throwErrorAt bad "invalid 'decreasing_by' in mutually inductive datatype declaration"
     elabMutualInductive stx[1].getArgs
   else if isMutualDef stx then
-    for arg in stx[1].getArgs do
-      let argHints := getTerminationHints arg
-      if let some bad := argHints.terminationBy? then
-        throwErrorAt bad "invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword"
-      if let some bad := argHints.decreasingBy? then
-        throwErrorAt bad "invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword"
-    elabMutualDef stx[1].getArgs hints
+    elabMutualDef stx[1].getArgs
   else
     throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs"
 
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index 5a24e0e0df..4d40561c95 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -124,7 +124,7 @@ def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefV
     | some val => pure val
     | none     =>
       let val ← if modifiers.isUnsafe then `(default_or_ofNonempty% unsafe) else `(default_or_ofNonempty%)
-      pure <| mkNode ``Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ]
+      `(Parser.Command.declValSimple| := $val)
   return {
     ref := stx, kind := DefKind.opaque, modifiers := modifiers,
     declId := stx[1], binders := binders, type? := some type, value := val
diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 73e49fe7df..a49b9e0f04 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -21,6 +21,7 @@ structure LetRecDeclView where
   type          : Expr
   mvar          : Expr -- auxiliary metavariable used to lift the 'let rec'
   valStx        : Syntax
+  termination   : WF.TerminationHints
 
 structure LetRecView where
   decls     : Array LetRecDeclView
@@ -59,7 +60,9 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
         pure decl[4]
       else
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
-      pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx : LetRecDeclView }
+      let termination ← WF.elabTerminationHints ⟨attrDeclStx[3]⟩
+      pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx,
+             termination : LetRecDeclView }
     else
       throwUnsupportedSyntax
   return { decls, body := letRec[3] }
@@ -91,18 +94,23 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
         throwError "'{view.declName}' has already been declared"
   let lctx ← getLCtx
   let localInstances ← getLocalInstances
-  let toLift := views.mapIdx fun i view => {
-    ref            := view.ref
-    fvarId         := fvars[i]!.fvarId!
-    attrs          := view.attrs
-    shortDeclName  := view.shortDeclName
-    declName       := view.declName
-    lctx
-    localInstances
-    type           := view.type
-    val            := values[i]!
-    mvarId         := view.mvar.mvarId!
-    : LetRecToLift }
+
+  let toLift ← views.mapIdxM fun i view => do
+    let value := values[i]!
+    let termination ← view.termination.checkVars view.binderIds.size value
+    pure {
+      ref            := view.ref
+      fvarId         := fvars[i]!.fvarId!
+      attrs          := view.attrs
+      shortDeclName  := view.shortDeclName
+      declName       := view.declName
+      lctx
+      localInstances
+      type           := view.type
+      val            := value
+      mvarId         := view.mvar.mvarId!
+      termination    := termination
+      : LetRecToLift }
   modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift }
 
 @[builtin_term_elab «letrec»] def elabLetRec : TermElab := fun stx expectedType? => do
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 5d9bdd5d44..b7c16d8e7a 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -13,6 +13,7 @@ import Lean.Elab.Match
 import Lean.Elab.DefView
 import Lean.Elab.Deriving.Basic
 import Lean.Elab.PreDefinition.Main
+import Lean.Elab.PreDefinition.WF.TerminationHint
 import Lean.Elab.DeclarationRange
 
 namespace Lean.Elab
@@ -221,14 +222,16 @@ private def expandWhereStructInst : Macro
 /-
 Recall that
 ```
-def declValSimple    := leading_parser " :=\n" >> termParser >> optional Term.whereDecls
+def declValSimple    := leading_parser " :=\n" >> termParser >> Termination.suffix >> optional Term.whereDecls
 def declValEqns      := leading_parser Term.matchAltsWhereDecls
 def declVal          := declValSimple <|> declValEqns <|> Term.whereDecls
 ```
+
+The `Termination.suffix` is ignored here, and extracted in `declValToTerminationHint`.
 -/
 private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal do
   if declVal.isOfKind ``Parser.Command.declValSimple then
-    expandWhereDeclsOpt declVal[2] declVal[1]
+    expandWhereDeclsOpt declVal[3] declVal[1]
   else if declVal.isOfKind ``Parser.Command.declValEqns then
     expandMatchAltsWhereDecls declVal[0]
   else if declVal.isOfKind ``Parser.Command.whereStructInst then
@@ -238,6 +241,15 @@ private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal
   else
     Macro.throwErrorAt declVal "unexpected declaration body"
 
+/-- Elaborates the termination hints in a `declVal` syntax. -/
+private def declValToTerminationHint (declVal : Syntax) : TermElabM WF.TerminationHints :=
+  if declVal.isOfKind ``Parser.Command.declValSimple then
+    WF.elabTerminationHints ⟨declVal[2]⟩
+  else if declVal.isOfKind ``Parser.Command.declValEqns then
+    WF.elabTerminationHints ⟨declVal[0][1]⟩
+  else
+    return .none
+
 private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
   headers.mapM fun header => withDeclName header.declName <| withLevelNames header.levelNames do
     let valStx ← liftMacroM <| declValToTerm header.valueStx
@@ -629,6 +641,8 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
     : TermElabM (Array PreDefinition) :=
   mainHeaders.size.foldM (init := preDefs) fun i preDefs => do
     let header := mainHeaders[i]!
+    let termination ← declValToTerminationHint header.valueStx
+    let termination ← termination.checkVars header.numParams mainVals[i]!
     let value ← mkLambdaFVars sectionVars mainVals[i]!
     let type ← mkForallFVars sectionVars header.type
     return preDefs.push {
@@ -637,7 +651,7 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
       declName    := header.declName
       levelParams := [], -- we set it later
       modifiers   := header.modifiers
-      type, value
+      type, value, termination
     }
 
 def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClosure) (kind : DefKind) (modifiers : Modifiers) : MetaM (Array PreDefinition) :=
@@ -655,7 +669,8 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
       declName    := c.toLift.declName
       levelParams := [] -- we set it later
       modifiers   := { modifiers with attrs := c.toLift.attrs }
-      kind, type, value
+      kind, type, value,
+      termination := c.toLift.termination
     }
 
 def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
@@ -766,7 +781,7 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs :
     for preDef in preDefs do
       checkPreDef preDef
 
-def elabMutualDef (vars : Array Expr) (views : Array DefView) (hints : TerminationHints) : TermElabM Unit :=
+def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
       -- save correct environment in info tree
@@ -805,7 +820,7 @@ where
         for preDef in preDefs do
           trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
         checkForHiddenUnivLevels allUserLevelNames preDefs
-        addPreDefinitions preDefs hints
+        addPreDefinitions preDefs
         processDeriving headers
 
   processDeriving (headers : Array DefViewElabHeader) := do
@@ -820,13 +835,13 @@ where
 end Term
 namespace Command
 
-def elabMutualDef (ds : Array Syntax) (hints : TerminationHints) : CommandElabM Unit := do
+def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
   let views ← ds.mapM fun d => do
     let modifiers ← elabModifiers d[0]
     if ds.size > 1 && modifiers.isNonrec then
       throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
     mkDefView modifiers d[1]
-  runTermElabM fun vars => Term.elabMutualDef vars views hints
+  runTermElabM fun vars => Term.elabMutualDef vars views
 
 end Command
 end Lean.Elab
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 02cab703f3..5fde43704a 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -8,11 +8,13 @@ import Lean.Util.CollectLevelParams
 import Lean.Meta.AbstractNestedProofs
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.DefView
+import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab
 open Meta
 open Term
 
+
 /--
   A (potentially recursive) definition.
   The elaborator converts it into Kernel definitions using many different strategies.
@@ -25,6 +27,7 @@ structure PreDefinition where
   declName    : Name
   type        : Expr
   value       : Expr
+  termination : WF.TerminationHints
   deriving Inhabited
 
 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index bc89dc993f..3d0bb8f6c9 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -13,11 +13,6 @@ namespace Lean.Elab
 open Meta
 open Term
 
-structure TerminationHints where
-  terminationBy? : Option Syntax := none
-  decreasingBy? : Option Syntax := none
-  deriving Inhabited
-
 private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := false) : TermElabM Unit := do
   for preDef in preDefs do
     trace[Elab.definition] "processing {preDef.declName}"
@@ -94,15 +89,12 @@ private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
-def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints) : TermElabM Unit := withLCtx {} {} do
+def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
   let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef
   let preDefs ← betaReduceLetRecApps preDefs
   let cliques := partitionPreDefs preDefs
-  let mut terminationBy ← liftMacroM <| WF.expandTerminationBy? hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
-  let mut decreasingBy  ← liftMacroM <| WF.expandDecreasingBy? hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
-  let mut hasErrors := false
   for preDefs in cliques do
     trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
     if preDefs.size == 1 && isNonRecursive preDefs[0]! then
@@ -116,35 +108,31 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
         addNonRec preDef
       else
         addAndCompileNonRec preDef
+      preDef.termination.ensureNone "not recursive"
     else if preDefs.any (·.modifiers.isUnsafe) then
       addAndCompileUnsafe preDefs
+      preDefs.forM (·.termination.ensureNone "unsafe")
     else if preDefs.any (·.modifiers.isPartial) then
       for preDef in preDefs do
         if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
           withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
       addAndCompilePartial preDefs
+      preDefs.forM (·.termination.ensureNone "partial")
     else
       try
-        let mut wf? := none
-        let mut decrTactic? := none
-        if let some wf := terminationBy.find? (preDefs.map (·.declName)) then
-          wf? := some wf
-          terminationBy := terminationBy.markAsUsed (preDefs.map (·.declName))
-        if let some { ref, value := decrTactic } := decreasingBy.find? (preDefs.map (·.declName)) then
-          decrTactic? := some (← withRef ref `(by $(⟨decrTactic⟩)))
-          decreasingBy := decreasingBy.markAsUsed (preDefs.map (·.declName))
-        if wf?.isSome || decrTactic?.isSome then
-          wfRecursion preDefs wf? decrTactic?
+        let hasHints := preDefs.any  fun preDef =>
+          preDef.termination.decreasing_by?.isSome || preDef.termination.termination_by?.isSome
+        if hasHints then
+          wfRecursion preDefs
         else
           withRef (preDefs[0]!.ref) <| mapError
             (orelseMergeErrors
               (structuralRecursion preDefs)
-              (wfRecursion preDefs none none))
+              (wfRecursion preDefs))
             (fun msg =>
               let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
               m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
       catch ex =>
-        hasErrors := true
         logException ex
         let s ← saveState
         try
@@ -159,9 +147,6 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
           else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
             addAsAxioms preDefs
         catch _ => s.restore
-  unless hasErrors do
-    liftMacroM <| terminationBy.ensureAllUsed
-    liftMacroM <| decreasingBy.ensureAllUsed
 
 builtin_initialize
   registerTraceClass `Elab.definition.body
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 7dd66d5d31..e52adb048f 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -13,6 +13,7 @@ import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.BRecOn
+import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Data.Array
 
 namespace Lean.Elab.WF
@@ -186,22 +187,48 @@ def assignSubsumed (mvars : Array MVarId) : MetaM (Array MVarId) :=
           return (false, true)
     return (true, true)
 
-def solveDecreasingGoals (decrTactic? : Option Syntax) (value : Expr) : MetaM Expr := do
+/--
+The subgoals, created by `mkDecreasingProof`, are of the form `[data _recApp: rel arg param]`, where
+`param` is the `PackMutual`'ed parameter of the current function, and thus we can peek at that to
+know which function is making the call.
+The close coupling with how arguments are packed and termination goals look like is not great,
+but it works for now.
+-/
+def groupGoalsByFunction (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
+  let mut r := mkArray numFuncs #[]
+  for goal in goals do
+    let (.mdata _ (.app _ param)) ← goal.getType
+        | throwError "MVar does not look like like a recursive call"
+    let (funidx, _) ← unpackMutualArg numFuncs param
+    r := r.modify funidx (·.push goal)
+  return r
+
+def solveDecreasingGoals (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do
   let goals ← getMVarsNoDelayed value
   let goals ← assignSubsumed goals
-  goals.forM fun goal => Lean.Elab.Term.TermElabM.run' <|
+  let goalss ← groupGoalsByFunction decrTactics.size goals
+  for goals in goalss, decrTactic? in decrTactics do
+    Lean.Elab.Term.TermElabM.run' do
     match decrTactic? with
     | none => do
-      let some ref := getRecAppSyntax? (← goal.getType)
-        | throwError "MVar does not look like like a recursive call"
+      for goal in goals do
+        let some ref := getRecAppSyntax? (← goal.getType)
+          | throwError "MVar does not look like like a recursive call"
         withRef ref <| applyDefaultDecrTactic goal
-    | some decrTactic => do
-      -- make info from `runTactic` available
-      pushInfoTree (.hole goal)
-      Term.runTactic goal decrTactic
+    | some decrTactic => withRef decrTactic.ref do
+      unless goals.isEmpty do -- unlikely to be empty
+        -- make info from `runTactic` available
+        goals.forM fun goal => pushInfoTree (.hole goal)
+        let remainingGoals ← Tactic.run goals[0]! do
+          Tactic.setGoals goals.toList
+          Tactic.withTacticInfoContext decrTactic.ref do
+            Tactic.evalTactic decrTactic.tactic
+        unless remainingGoals.isEmpty do
+          Term.reportUnsolvedGoals remainingGoals
   instantiateMVars value
 
-def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do
+def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr)
+    (decrTactics : Array (Option DecreasingBy)) : TermElabM Expr := do
   let type ← instantiateForall preDef.type prefixArgs
   let (wfFix, varName) ← forallBoundedTelescope type (some 1) fun x type => do
     let x := x[0]!
@@ -224,7 +251,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (dec
       let val := preDef.value.beta (prefixArgs.push x)
       let val ← processSumCasesOn x F val fun x F val => do
         processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size)
-      let val ← solveDecreasingGoals decrTactic? val
+      let val ← solveDecreasingGoals decrTactics val
       mkLambdaFVars prefixArgs (mkApp wfFix (← mkLambdaFVars #[x, F] val))
 
 end Lean.Elab.WF
diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index ea9c8e7042..4034f45193 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -72,27 +72,42 @@ register_builtin_option showInferredTerminationBy : Bool := {
   descr    := "In recursive definitions, show the inferred `termination_by` measure."
 }
 
+
 /--
-Given a predefinition, find good variable names for its parameters.
-Use user-given parameter names if present; use x1...xn otherwise.
+Given a predefinition, return the variabe names in the outermost lambdas.
+Includes the “fixed prefix”.
 
 The length of the returned array is also used to determine the arity
 of the function, so it should match what `packDomain` does.
+-/
+def originalVarNames (preDef : PreDefinition) : MetaM (Array Name) := do
+  lambdaTelescope preDef.value fun xs _ => xs.mapM (·.fvarId!.getUserName)
 
-The names ought to accessible (no macro scopes) and still fresh wrt to the current environment,
+/--
+Given the original paramter names from `originalVarNames`, remove the fixed prefix and find
+good variable names to be used when talking about termination arguments:
+Use user-given parameter names if present; use x1...xn otherwise.
+
+The names ought to accessible (no macro scopes) and new names  fresh wrt to the current environment,
 so that with `showInferredTerminationBy` we can print them to the user reliably.
 We do that by appending `'` as needed.
+
+It is possible (but unlikely without malice) that some of the user-given names
+shadow each other, and the guessed relation refers to the wrong one. In that
+case, the user gets to keep both pieces (and may have to rename variables).
 -/
 partial
-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 : Array Name := #[]
-    for h : i in [:xs.size] do
-      let n ← xs[i].fvarId!.getUserName
-      let n := if n.hasMacroScopes then .mkSimple s!"x{i+1}" else n
-      ns := ns.push (← freshen ns n)
-    return ns
+def naryVarNames (fixedPrefixSize : Nat) (xs : Array Name) : MetaM (Array Name) := do
+  let xs := xs.extract fixedPrefixSize xs.size
+  let mut ns : Array Name := #[]
+  for h : i in [:xs.size] do
+    let n := xs[i]
+    let n ← if n.hasMacroScopes then
+        freshen ns (.mkSimple s!"x{i+1}")
+      else
+        pure n
+    ns := ns.push n
+  return ns
   where
     freshen  (ns : Array Name) (n : Name): MetaM Name := do
       if !(ns.elem n) && (← resolveGlobalName n).isEmpty then
@@ -274,7 +289,6 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti
     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
@@ -318,7 +332,7 @@ def mkSizeOf (e : Expr) : MetaM Expr := do
 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) :
+def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) (paramIdx argIdx : Nat) :
     MetaM GuessLexRel := do
   rcc.ctxt.run do
     let param := rcc.params[paramIdx]!
@@ -334,25 +348,20 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallWithContext) (paramI
       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 ()
+          Lean.Elab.Term.TermElabM.run' do Term.withoutErrToSorry do
+            let remainingGoals ← Tactic.run mvarId do Tactic.withoutRecover do
+              let tacticStx : Syntax ←
+                match decrTactic? with
+                | none => pure (← `(tactic| decreasing_tactic)).raw
+                | some decrTactic =>
+                  trace[Elab.definition.wf] "Using tactic {decrTactic.tactic.raw}"
+                  pure decrTactic.tactic.raw
+              Tactic.evalTactic tacticStx
+            remainingGoals.forM fun _ => throwError "goal not solved"
         trace[Elab.definition.wf] "inspectRecCall: success!"
         return rel
       catch _e =>
@@ -362,13 +371,15 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallWithContext) (paramI
 
 /- A cache for `evalRecCall` -/
 structure RecCallCache where mk'' ::
-  decrTactic? : Option Syntax
+  decrTactic? : Option DecreasingBy
   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) :
+def RecCallCache.mk (decrTactics : Array (Option DecreasingBy))
+    (rcc : RecCallWithContext) :
     BaseIO RecCallCache := do
+  let decrTactic? := decrTactics[rcc.caller]!
   let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none)
   return { decrTactic?, rcc, cache }
 
@@ -536,29 +547,46 @@ def mkTupleSyntax : Array Term → MetaM Term
 
 /--
 Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic
-combination of these measures.
+combination of these measures. The parameters are
+
+* `originalVarNamess`: For each function in the clique, the original parameter names, _including_
+  the fixed prefix.  Used to determine if we need to fully qualify `sizeOf`.
+* `varNamess`: For each function in the clique, the parameter names to be used in the
+  termination relation. Excludes the fixed prefix. Includes names like `x1` for unnamed parameters.
+* `measures`: The measures to be used.
 -/
-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].map mkIdent
-    let body ← mkTupleSyntax (← measures.mapM fun
+def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Array Name))
+  (measures : Array MutualMeasure) : MetaM TerminationWF := do
+  varNamess.mapIdxM fun funIdx varNames => do
+    let idents := varNames.map mkIdent
+    let measureStxs ← measures.mapM fun
       | .args varIdxs => do
-          let v := vars.get! varIdxs[funIdx]!
-          let sizeOfIdent := mkIdent (← unresolveNameGlobal ``sizeOf)
+          let varIdx := varIdxs[funIdx]!
+          let v := idents[varIdx]!
+          -- Print `sizeOf` as such, unless it is shadowed.
+          -- Shadowing by a `def` in the current namespace is handled by `unresolveNameGlobal`.
+          -- But it could also be shadowed by an earlier parameter (including the fixed prefix),
+          -- so look for unqualified (single tick) occurrences in `originalVarNames`
+          let sizeOfIdent :=
+            if originalVarNamess[funIdx]!.any (· = `sizeOf) then
+              mkIdent ``sizeOf -- fully qualified
+            else
+              mkIdent (← unresolveNameGlobal ``sizeOf)
           `($sizeOfIdent $v)
       | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
-      )
-    let declName := declNames[funIdx]!
-
-    termByElements := termByElements.push
-      { ref := .missing
-        declName, vars, body,
-        implicit := true
-      }
-  return termByElements
+    let body ← mkTupleSyntax measureStxs
+    return { ref := .missing, vars := idents, body }
 
+/--
+The TerminationWF produced by GuessLex may mention more variables than allowed in the surface
+syntax (in case of unnamed or shadowed parameters). So how to print this to the user? Invalid
+syntax with more information, or valid syntax with (possibly) unresolved variable names?
+The latter works fine in many cases, and is still useful to the user in the tricky corner cases, so
+we do that.
+-/
+def trimTermWF (extraParams : Array Nat) (elems : TerminationWF) : TerminationWF :=
+  elems.mapIdx fun funIdx elem =>
+    { elem with vars := elem.vars[elem.vars.size - extraParams[funIdx]! : elem.vars.size] }
 
 /--
 Given a matrix (row-major) of strings, arranges them in tabular form.
@@ -668,10 +696,12 @@ 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) :
+def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
+    (fixedPrefixSize : Nat) :
     MetaM TerminationWF := do
-  let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
+  let extraParamss := preDefs.map (·.termination.extraParams)
+  let originalVarNamess ← preDefs.mapM originalVarNames
+  let varNamess ← originalVarNamess.mapM (naryVarNames fixedPrefixSize ·)
   let arities := varNamess.map (·.size)
   trace[Elab.definition.wf] "varNames is: {varNamess}"
 
@@ -684,24 +714,22 @@ def guessLex (preDefs : Array PreDefinition)  (unaryPreDef : PreDefinition)
 
   -- If there is only one plausible measure, use that
   if let #[solution] := measures then
-    return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution]
+    return ← buildTermWF originalVarNamess varNamess #[solution]
 
   -- Collect all recursive calls and extract their context
   let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
   let recCalls := filterSubsumed recCalls
-  let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·)
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasing_by?)) ·)
   let callMatrix := rcs.map (inspectCall ·)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
-    let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
-
-    let wfStx ← withoutModifyingState do
-      preDefs.forM (addAsAxiom ·)
-      wf.unexpand
+    let wf ← buildTermWF originalVarNamess varNamess solution
 
     if showInferredTerminationBy.get (← getOptions) then
-      logInfo m!"Inferred termination argument:{wfStx}"
+      let wf' := trimTermWF extraParamss wf
+      for preDef in preDefs, term in wf' do
+        logInfoAt preDef.ref m!"Inferred termination argument: {← term.unexpand}"
 
     return wf
   | .none =>
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index ea82f6baf3..6f69214c67 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -80,7 +80,7 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize :
   else
     return false
 
-def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (decrTactic? : Option Syntax) : TermElabM Unit := do
+def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   let preDefs ← preDefs.mapM fun preDef => return { preDef with value := (← preprocess preDef.value) }
   let (unaryPreDef, fixedPrefixSize) ← withoutModifyingEnv do
     for preDef in preDefs do
@@ -91,20 +91,29 @@ def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (de
     let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte
     return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
 
-  let wf ←
-    if let .some wf := wf? then
-      pure wf
+  let extraParamss := preDefs.map (·.termination.extraParams)
+  let wf ← do
+    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.termination_by?.isSome)
+    if preDefsWith.isEmpty then
+      -- No termination_by anywhere, so guess one
+      guessLex preDefs unaryPreDef fixedPrefixSize
+    else if preDefsWithout.isEmpty then
+      pure <| preDefsWith.map (·.termination.termination_by?.get!)
     else
-      guessLex preDefs unaryPreDef fixedPrefixSize decrTactic?
+      -- Some have, some do not, so report errors
+      preDefsWithout.forM fun preDef => do
+        logErrorAt preDef.ref (m!"Missing `termination_by`; this function is mutually " ++
+          m!"recursive with {preDefsWith[0]!.declName}, which has a `termination_by` clause.")
+      return
 
   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 extraParamss wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
-        let value ← mkFix unaryPreDef prefixArgs wfRel decrTactic?
+        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasing_by?))
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value
diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 23c428a6cf..23cfd97930 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -14,12 +14,6 @@ namespace Lean.Elab.WF
 open Meta
 open Term
 
-private def getRefFromElems (elems : Array TerminationByElement) : Syntax := Id.run do
-  for elem in elems do
-    if !elem.implicit then
-      return elem.ref
-  return elems[0]!.ref
-
 private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarId) (fvarId : FVarId) : TermElabM (Array (FVarId × MVarId)) := do
   let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) (result : Array (FVarId × MVarId)) : TermElabM (Array (FVarId × MVarId)) := do
     if i < preDefs.size - 1 then
@@ -29,7 +23,13 @@ private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarI
       return result.push (fvarId, mvarId)
   go 0 mvarId fvarId #[]
 
-private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId) (fvarId : FVarId) (element : TerminationByElement) : TermElabM MVarId := do
+private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId)
+    (fvarId : FVarId) (extraParams : Nat) (element : TerminationBy) : TermElabM MVarId := do
+  -- If elements.vars is ≤ extraParams, this is user-provided, and should be interpreted
+  -- as left to right. Else it is provided by GuessLex, and may rename non-extra paramters as well.
+  -- (Not pretty, but it works for now)
+  let implicit_underscores :=
+    if element.vars.size < extraParams then extraParams - element.vars.size else 0
   let varNames ← lambdaTelescope preDef.value fun xs _ => do
     let mut varNames ← xs.mapM fun x => x.fvarId!.getUserName
     if element.vars.size > varNames.size then
@@ -37,7 +37,8 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
     for h : i in [:element.vars.size] do
       let varStx := element.vars[i]
       if let `($ident:ident) := varStx then
-        varNames := varNames.set! (varNames.size - element.vars.size + i) ident.getId
+        let j := varNames.size - implicit_underscores - element.vars.size + i
+        varNames := varNames.set! j ident.getId
     return varNames
   let mut mvarId := mvarId
   for localDecl in (← Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
@@ -54,19 +55,19 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
   go 0 mvarId fvarId
 
 def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat)
-    (argType : Expr) (wf : TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do
+    (argType : Expr) (extraParamss : Array Nat) (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!}"
   withDeclName unaryPreDefName do
-  withRef (getRefFromElems wf) do
     let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
     let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
     let (d, fMVarId) ← fMVarId.intro1
     let subgoals ← unpackMutual preDefs fMVarId d
-    for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
-      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
+    for (d, mvarId) in subgoals, extraParams in extraParamss, element in wf, preDef in preDefs do
+      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d extraParams element
       mvarId.withContext do
         let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
         mvarId.assign value
diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
index b7d54f051c..66cafe32f6 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
@@ -1,213 +1,113 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Joachim Breitner
 -/
-import Lean.Parser.Command
+import Lean.Parser.Term
 
 set_option autoImplicit false
 
 namespace Lean.Elab.WF
 
-/-! # Support for `decreasing_by` -/
-
-structure DecreasingByTactic where
-  ref   : Syntax
-  value : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
-  deriving Inhabited
-
-inductive DecreasingBy where
-  | none
-  | one (val : DecreasingByTactic)
-  | many (map : NameMap DecreasingByTactic)
-  deriving Inhabited
-
-open Parser.Command in
-/--
-This function takes a user-specified `decreasing_by` clause (as `Sytnax`).
-If it is a `decreasingByMany` (a set of clauses guarded by the function name) then
-* checks that all mentioned names exist in the current declaration
-* check that at most one function from each clique is mentioned
-and sort the entries by function name.
--/
-def expandDecreasingBy? (decreasingBy? : Option Syntax) (cliques : Array (Array Name)) : MacroM DecreasingBy := do
-  let some decreasingBy := decreasingBy? | return DecreasingBy.none
-  let ref := decreasingBy
-  match decreasingBy with
-  | `(decreasingBy|decreasing_by $hint1:tacticSeq) =>
-    return DecreasingBy.one { ref, value := hint1 }
-  | `(decreasingBy|decreasing_by $hints:decreasingByMany) => do
-    let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg => do
-      let arg : TSyntax `decreasingByElement := ⟨arg⟩ -- cannot use syntax pattern match with lookahead
-      let `(decreasingByElement| $declId:ident => $tac:tacticSeq) := arg | Macro.throwUnsupported
-      let declName? := cliques.findSome? fun clique => clique.findSome? fun declName =>
-        if declId.getId.isSuffixOf declName then some declName else none
-      match declName? with
-      | none => Macro.throwErrorAt declId s!"function '{declId.getId}' not found in current declaration"
-      | some declName => return m.insert declName { ref := arg, value := tac }
-    for clique in cliques do
-      let mut found? := Option.none
-      for declName in clique do
-        if let some { ref, .. } := m.find? declName then
-          if let some found := found? then
-            Macro.throwErrorAt ref s!"invalid termination hint element, '{declName}' and '{found}' are in the same clique"
-          found? := some declName
-    return DecreasingBy.many m
-  | _ => Macro.throwUnsupported
-
-def DecreasingBy.markAsUsed (t : DecreasingBy) (clique : Array Name) : DecreasingBy :=
-  match t with
-  | DecreasingBy.none   => DecreasingBy.none
-  | DecreasingBy.one .. => DecreasingBy.none
-  | DecreasingBy.many m => Id.run do
-    for declName in clique do
-      if m.contains declName then
-        let m := m.erase declName
-        if m.isEmpty then
-          return DecreasingBy.none
-        else
-          return DecreasingBy.many m
-    return t
-
-def DecreasingBy.find? (t : DecreasingBy) (clique : Array Name) : Option DecreasingByTactic :=
-  match t with
-  | DecreasingBy.none   => Option.none
-  | DecreasingBy.one v  => some v
-  | DecreasingBy.many m => clique.findSome? m.find?
-
-def DecreasingBy.ensureAllUsed (t : DecreasingBy) : MacroM Unit := do
-  match t with
-  | DecreasingBy.one v   => Macro.throwErrorAt v.ref "unused termination hint element"
-  | DecreasingBy.many m  => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
-  | _ => pure ()
-
 /-! # Support for `termination_by` notation -/
 
 /-- A single `termination_by` clause -/
-structure TerminationByElement where
+structure TerminationBy where
   ref       : Syntax
-  declName  : Name
   vars      : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
   body      : Term
-  implicit  : Bool
   deriving Inhabited
 
-/-- `termination_by` clauses, grouped by clique -/
-structure TerminationByClique where
-  elements : Array TerminationByElement
-  used     : Bool := false
+open Parser.Termination in
+def TerminationBy.unexpand (wf : TerminationBy) : MetaM Syntax := do
+  -- TODO: Why can I not just use $wf.vars in the quotation below?
+  let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
+  if vars.isEmpty then
+    `(terminationBy|termination_by $wf.body)
+  else
+    `(terminationBy|termination_by $vars* => $wf.body)
 
-/--
-A `termination_by` hint, as specified by the user
--/
-structure TerminationBy where
-  cliques : Array TerminationByClique
+/-- A complete set of `termination_by` hints, as applicable to a single clique.  -/
+abbrev TerminationWF := Array TerminationBy
+
+/-- A single `decreasing_by` clause -/
+structure DecreasingBy where
+  ref       : Syntax
+  tactic    : TSyntax ``Lean.Parser.Tactic.tacticSeq
   deriving Inhabited
 
+/-- The termination annotations for a single function.
+For `decreasing_by`, we store the whole `decreasing_by tacticSeq` expression, as this
+is what `Term.runTactic` expects.
+ -/
+structure TerminationHints where
+  ref : Syntax
+  termination_by? : Option TerminationBy
+  decreasing_by?  : Option DecreasingBy
+  /-- Here we record the number of parameters past the `:`. This is
+  * `GuessLex` when there is no `termination_by` annotation, so that
+     we can print the guessed order in the right form.
+  * If there are fewer variables in the `termination_by` annotation than there are extra
+    parameters, we know which parameters they should apply to.
+
+  It it set in `TerminationHints.checkVars`, which is the place where we also check that the user
+  does not bind more extra parameters than present in the predefinition.
+  -/
+  extraParams : Nat
+  deriving Inhabited
+
+def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, 0⟩
+
+/-- Logs warnings when the `TerminationHints` are present.  -/
+def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): CoreM Unit := do
+  match hints.termination_by?, hints.decreasing_by? with
+  | .none, .none => pure ()
+  | .none, .some dec_by =>
+    logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
+  | .some term_by, .none =>
+    logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}"
+  | .some _, .some _ =>
+    logErrorAt hints.ref m!"unused termination hints, function is {reason}"
+
 /--
-A `termination_by` hint, as applicable to a single clique
+Checks that `termination_by` binds at most as many variables are present in the outermost
+lambda of `value`, and logs (without failing) appropriate errors.
+
+Also remembers `extraParams` for later use.
 -/
-abbrev TerminationWF := Array TerminationByElement
+def TerminationHints.checkVars (headerParams : Nat) (hints : TerminationHints) (value : Expr) :
+    MetaM TerminationHints := do
+  let extraParams := value.getNumHeadLambdas - headerParams
+  if let .some tb := hints.termination_by? then
+    if tb.vars.size > extraParams then
+      logErrorAt tb.ref <| m!"Too many extra parameters bound; the function definition only " ++
+        m!"has {extraParams} extra parameters."
+  return { hints with extraParams := extraParams }
 
-open Parser.Command in
-/--
-Expands the syntax for a `termination_by` clause, checking that
-* each function is mentioned once
-* each function mentioned actually occurs in the current declaration
-* if anything is specified, then all functions have a clause
-* the else-case (`_`) occurs only once, and only when needed
+open Parser.Termination
 
-NB:
-```
-def terminationByElement   := leading_parser ppLine >> (ident <|> hole) >> many (ident <|> hole) >> " => " >> termParser >> optional ";"
-def terminationBy          := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement
-```
--/
-def expandTerminationBy? (hint? : Option Syntax) (cliques : Array (Array Name)) :
-    MacroM TerminationBy := do
-  let some hint := hint?  | return { cliques := #[] }
-  let `(terminationBy|termination_by $elementStxs*) := hint | Macro.throwUnsupported
-  let mut alreadyFound : NameSet := {}
-  let mut elseElemStx? := none
-  for elementStx in elementStxs do
-    match elementStx with
-    | `(terminationByElement|$ident:ident $_* => $_) =>
-      let declSuffix := ident.getId
-      if alreadyFound.contains declSuffix then
-        withRef elementStx <| Macro.throwError s!"invalid `termination_by` syntax, `{declSuffix}` case has already been provided"
-      alreadyFound := alreadyFound.insert declSuffix
-      if cliques.all fun clique => clique.all fun declName => !declSuffix.isSuffixOf declName then
-        withRef elementStx <| Macro.throwError s!"function '{declSuffix}' not found in current declaration"
-    | `(terminationByElement|_ $_vars* => $_term) =>
-      if elseElemStx?.isSome then
-        withRef elementStx <| Macro.throwError "invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified"
-      else
-        elseElemStx? := some elementStx
-    | _ => Macro.throwUnsupported
-  let toElement (declName : Name) (elementStx : TSyntax ``terminationByElement) : TerminationByElement :=
-    match elementStx with
-    | `(terminationByElement|$ioh $vars* => $body:term) =>
-    let implicit := !ioh.raw.isIdent
-    { ref := elementStx, declName, vars, implicit, body }
-    | _ => unreachable!
-  let elementAppliesTo (declName : Name) : TSyntax ``terminationByElement → Bool
-    | `(terminationByElement|$ident:ident $_* => $_) => ident.getId.isSuffixOf declName
-    | _ => false
-  let mut result := #[]
-  let mut usedElse := false
-  for clique in cliques do
-    let mut elements := #[]
-    for declName in clique do
-      if let some elementStx := elementStxs.find? (elementAppliesTo declName) then
-        elements := elements.push (toElement declName elementStx)
-      else if let some elseElemStx := elseElemStx? then
-        elements := elements.push (toElement declName elseElemStx)
-        usedElse := true
-    unless elements.isEmpty do
-      if let some missing := clique.find? fun declName => elements.find? (·.declName == declName) |>.isNone then
-        withRef elements[0]!.ref <| Macro.throwError s!"invalid `termination_by` syntax, missing case for function '{missing}'"
-      result := result.push { elements }
-  if !usedElse && elseElemStx?.isSome then
-    withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case"
-  return ⟨result⟩
-
-open Parser.Command in
-def TerminationWF.unexpand (elements : TerminationWF) : MetaM Syntax := do
-  let elementStxs ← elements.mapM fun element => do
-    let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
-    `(terminationByElement|$fn $element.vars* => $element.body)
-  `(terminationBy|termination_by $elementStxs*)
-
-def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy :=
-  .mk <| t.cliques.map fun clique =>
-    if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
-      { clique with used := true }
-    else
-      clique
-
-def TerminationBy.find? (t : TerminationBy) (cliqueNames : Array Name) : Option TerminationWF :=
-  t.cliques.findSome? fun clique =>
-    if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
-      some <| clique.elements
-    else
-      none
-
-def TerminationByClique.allImplicit (c : TerminationByClique) : Bool :=
-  c.elements.all fun elem => elem.implicit
-
-def TerminationByClique.getExplicitElement? (c : TerminationByClique) : Option TerminationByElement :=
-  c.elements.find? (!·.implicit)
-
-def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit := do
-  let hasUsedAllImplicit := t.cliques.any fun c => c.allImplicit && c.used
-  let mut reportedAllImplicit := true
-  for clique in t.cliques do
-    unless clique.used do
-      if let some explicitElem := clique.getExplicitElement? then
-        Macro.throwErrorAt explicitElem.ref "unused termination hint element"
-      else if !hasUsedAllImplicit then
-        unless reportedAllImplicit do
-          reportedAllImplicit := true
-          Macro.throwErrorAt clique.elements[0]!.ref "unused termination hint element"
+/-- Takes apart a `Termination.suffix` syntax object -/
+def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) : m TerminationHints := do
+  -- Fail gracefully upon partial parses
+  if let .missing := stx.raw then
+    return { TerminationHints.none with ref := stx }
+  -- This can be removed after the next stage0 bump
+  if stx.raw.matchesNull 0 then
+    return { TerminationHints.none with ref := stx }
+  match stx with
+  | `(suffix| $[$t?:terminationBy]? $[$d?:decreasingBy]? ) => do
+    let termination_by? ← t?.mapM fun t => match t with
+      | `(terminationBy|termination_by $vars* => $body) =>
+        if vars.isEmpty then
+          throwErrorAt t "no extra parameters bounds, please omit the `=>`"
+        else
+          pure {ref := t, vars, body}
+      | `(terminationBy|termination_by $body:term) => pure {ref := t, vars := #[], body}
+      | _ => throwErrorAt t "unexpected `termination_by` syntax"
+    let decreasing_by? ← d?.mapM fun d => match d with
+      | `(decreasingBy|decreasing_by $tactic) => pure {ref := d, tactic}
+      | _ => throwErrorAt d "unexpected `decreasing_by` syntax"
+    return { ref := stx, termination_by?, decreasing_by?, extraParams := 0 }
+  | _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
 
 end Lean.Elab.WF
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 7a6e2e1447..236629875e 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -291,9 +291,10 @@ mutual
 
   /--
   Try to synthesize a term `val` using the tactic code `tacticCode`, and then assign `mvarId := val`.
+
+  The `tacticCode` syntax comprises the whole `by ...` expression.
   -/
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := withoutAutoBoundImplicit do
-    /- Recall, `tacticCode` is the whole `by ...` expression. -/
     let code := tacticCode[1]
     instantiateMVarDeclMVars mvarId
     /-
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 251329a37d..3ea0525af7 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -10,6 +10,7 @@ import Lean.Linter.Deprecated
 import Lean.Elab.Config
 import Lean.Elab.Level
 import Lean.Elab.DeclModifiers
+import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab
 
@@ -95,6 +96,7 @@ structure LetRecToLift where
   type           : Expr
   val            : Expr
   mvarId         : MVarId
+  termination    : WF.TerminationHints
   deriving Inhabited
 
 /--
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 4d2981dd80..28f6bea11b 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -28,27 +28,6 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
-/--
-A decreasing_by clause can either be a single tactic (for all functions), or
-a list of tactics labeled with the function they apply to.
--/
-def decreasingByElement := leading_parser
-  ppLine >> ppIndent (ident >> " => " >> Tactic.tacticSeq >> patternIgnore (optional ";"))
-def decreasingByMany := leading_parser
-  atomic (lookahead (ident >> " => ")) >> many1Indent decreasingByElement
-def decreasingBy1  := leading_parser Tactic.tacticSeq
-
-def decreasingBy := leading_parser
-  ppDedent ppLine >> "decreasing_by " >> (decreasingByMany <|> decreasingBy1)
-
-def terminationByElement   := leading_parser
-  ppLine >> (ident <|> Term.hole) >> many (ppSpace >> (ident <|> Term.hole)) >>
-  " => " >> termParser >> patternIgnore (optional ";")
-def terminationBy          := leading_parser
-  ppDedent ppLine >> "termination_by" >> many1Indent terminationByElement
-
-def terminationSuffix :=
-  optional terminationBy >> optional decreasingBy
 
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
@@ -96,7 +75,7 @@ def declSig          := leading_parser
 def optDeclSig       := leading_parser
   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
 def declValSimple    := leading_parser
-  " :=" >> ppHardLineUnlessUngrouped >> termParser >> optional Term.whereDecls
+  " :=" >> ppHardLineUnlessUngrouped >> termParser >> Termination.suffix >> optional Term.whereDecls
 def declValEqns      := leading_parser
   Term.matchAltsWhereDecls
 def whereStructField := leading_parser
@@ -116,20 +95,20 @@ def declVal          :=
   withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
     declValSimple <|> declValEqns <|> whereStructInst
 def «abbrev»         := leading_parser
-  "abbrev " >> declId >> ppIndent optDeclSig >> declVal >> terminationSuffix
+  "abbrev " >> declId >> ppIndent optDeclSig >> declVal
 def optDefDeriving   :=
   optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
 def «def»            := leading_parser
-  "def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
+  "def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving
 def «theorem»        := leading_parser
-  "theorem " >> declId >> ppIndent declSig >> declVal >> terminationSuffix
+  "theorem " >> declId >> ppIndent declSig >> declVal
 def «opaque»         := leading_parser
   "opaque " >> declId >> ppIndent declSig >> optional declValSimple
 /- As `declSig` starts with a space, "instance" does not need a trailing space
   if we put `ppSpace` in the optional fragments. -/
 def «instance»       := leading_parser
   Term.attrKind >> "instance" >> optNamedPrio >>
-  optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix
+  optional (ppSpace >> declId) >> ppIndent declSig >> declVal
 def «axiom»          := leading_parser
   "axiom " >> declId >> ppIndent declSig
 /- As `declSig` starts with a space, "example" does not need a trailing space. -/
@@ -269,7 +248,7 @@ def openDecl         :=
 
 @[builtin_command_parser] def «mutual» := leading_parser
   "mutual" >> many1 (ppLine >> notSymbol "end" >> commandParser) >>
-  ppDedent (ppLine >> "end") >> terminationSuffix
+  ppDedent (ppLine >> "end")
 def initializeKeyword := leading_parser
   "initialize " <|> "builtin_initialize "
 @[builtin_command_parser] def «initialize» := leading_parser
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 3349d34185..715b65643b 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -96,6 +96,52 @@ end Tactic
 def darrow : Parser := " => "
 def semicolonOrLinebreak := ";" <|> checkLinebreakBefore >> pushNone
 
+namespace Termination
+
+/-
+Termination suffix parsers, typically thought of as part of a command, but due to
+letrec we need them here already.
+-/
+
+/--
+Specify a termination argument for well-founded termination:
+```
+termination_by a - b
+```
+indicates that termination of the currently defined recursive function follows
+because the difference between the the arguments `a` and `b`.
+
+If the fuction takes further argument after the colon, you can name them as follows:
+```
+def example (a : Nat) : Nat → Nat → Nat :=
+termination_by b c => a - b
+```
+
+If omitted, a termination argument will be inferred.
+-/
+def terminationBy := leading_parser
+  ppDedent ppLine >>
+  "termination_by " >>
+  optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
+  termParser
+
+/--
+Manually prove that the termination argument (as specified with `termination_by` or inferred)
+decreases at each recursive call.
+
+By default, the tactic `decreasing_tactic` is used.
+-/
+def decreasingBy := leading_parser
+  ppDedent ppLine >> "decreasing_by " >> Tactic.tacticSeqIndentGt
+
+/--
+Termination hints are `termination_by` and `decreasing_by`, in that order.
+-/
+def suffix := leading_parser
+  optional terminationBy >> optional decreasingBy
+
+end Termination
+
 namespace Term
 
 /-! # Built-in parsers -/
@@ -533,7 +579,7 @@ def attributes       := leading_parser
 /-- `letRecDecl` matches the body of a let-rec declaration: a doc comment, attributes, and then
 a let declaration without the `let` keyword, such as `/-- foo -/ @[simp] bar := 1`. -/
 def letRecDecl       := leading_parser
-  optional Command.docComment >> optional «attributes» >> letDecl
+  optional Command.docComment >> optional «attributes» >> letDecl >> Termination.suffix
 /-- `letRecDecls` matches `letRecDecl,+`, a comma-separated list of let-rec declarations (see `letRecDecl`). -/
 def letRecDecls      := leading_parser
   sepBy1 letRecDecl ", "
@@ -548,7 +594,7 @@ def whereDecls := leading_parser
 
 @[run_builtin_parser_attribute_hooks]
 def matchAltsWhereDecls := leading_parser
-  matchAlts >> optional whereDecls
+  matchAlts >> Termination.suffix >> optional whereDecls
 
 @[builtin_term_parser] def noindex := leading_parser
   "no_index " >> termParser maxPrec
diff --git a/src/lake/Lake/DSL/DeclUtil.lean b/src/lake/Lake/DSL/DeclUtil.lean
index f7e688d161..d9183e7fc2 100644
--- a/src/lake/Lake/DSL/DeclUtil.lean
+++ b/src/lake/Lake/DSL/DeclUtil.lean
@@ -86,15 +86,15 @@ def mkConfigDecl (name? : Option Name)
 | `(structDeclSig| $id:ident) =>
   `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty :=
     {name := $(quote id.getId)})
-| `(structDeclSig| $id:ident where $fs;* $[$wds?]?) => do
+| `(structDeclSig| $id:ident where $fs;* $[$wds?:whereDecls]?) => do
   let fields ← fs.getElems.mapM expandDeclField
   let defn ← `({ name := $(quote id.getId), $fields,* })
-  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
+  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?:whereDecls]?)
 | `(structDeclSig| $id:ident $[: $ty?]? :=%$defTk $defn $[$wds?]?) => do
   let notice ← withRef defTk `(#eval IO.eprintln s!" warning: {__dir__}: `:=` syntax for configurations has been deprecated")
   `($notice $[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
-| `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
+| `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?:whereDecls]?) => do
   let fields ← fs.mapM expandDeclField
   let defn ← `({ name := $(quote id.getId), $fields,* })
-  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
+  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?:whereDecls]?)
 | stx => Macro.throwErrorAt stx "ill-formed configuration syntax"
diff --git a/src/lake/Lake/DSL/Package.lean b/src/lake/Lake/DSL/Package.lean
index 6aead21854..7c1941ca7b 100644
--- a/src/lake/Lake/DSL/Package.lean
+++ b/src/lake/Lake/DSL/Package.lean
@@ -65,12 +65,12 @@ optional(docComment) optional(Term.attributes)
 "post_update " (ppSpace simpleBinder)? (declValSimple <|> declValDo) : command
 
 macro_rules
-| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?]?) =>
-  `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?]?)
-| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?]?) => do
+| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?:whereDecls]?) =>
+  `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?:whereDecls]?)
+| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?:whereDecls]?) => do
   let pkg ← expandOptSimpleBinder pkg?
   let pkgName := mkIdentFrom pkg `_package.name
   let attr ← withRef kw `(Term.attrInstance| «post_update»)
   let attrs := #[attr] ++ expandAttrs attrs?
   `($[$doc?]? @[$attrs,*] def postUpdateHook : PostUpdateHookDecl :=
-    {pkg := $pkgName, fn := fun $pkg => $defn} $[$wds?]?)
+    {pkg := $pkgName, fn := fun $pkg => $defn} $[$wds?:whereDecls]?)
diff --git a/src/lake/Lake/DSL/Script.lean b/src/lake/Lake/DSL/Script.lean
index f7a5b57176..681bfe9673 100644
--- a/src/lake/Lake/DSL/Script.lean
+++ b/src/lake/Lake/DSL/Script.lean
@@ -37,10 +37,10 @@ scoped syntax (name := scriptDecl)
 
 @[macro scriptDecl]
 def expandScriptDecl : Macro
-| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? do $seq $[$wds?]?) => do
-  `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := do $seq $[$wds?]?)
-| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := $defn $[$wds?]?) => do
+| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? do $seq $[$wds?:whereDecls]?) => do
+  `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := do $seq $[$wds?:whereDecls]?)
+| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := $defn $[$wds?:whereDecls]?) => do
   let args ← expandOptSimpleBinder args?
   let attrs := #[← `(Term.attrInstance| «script»)] ++ expandAttrs attrs?
-  `($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?]?)
+  `($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?:whereDecls]?)
 | stx => Macro.throwErrorAt stx "ill-formed script declaration"
diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean
index 5de76c034a..dc00363f54 100644
--- a/src/lake/Lake/DSL/Targets.lean
+++ b/src/lake/Lake/DSL/Targets.lean
@@ -34,7 +34,7 @@ scoped macro (name := moduleFacetDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"module_facet " sig:buildDeclSig : command => do
   match sig with
-  | `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$wds?]?) =>
+  | `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$wds?:whereDecls]?) =>
     let attr ← withRef kw `(Term.attrInstance| module_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
@@ -45,7 +45,7 @@ kw:"module_facet " sig:buildDeclSig : command => do
         name := $name
         config := Lake.mkFacetJobConfig
           fun $mod => ($defn : IndexBuildM (BuildJob $ty))
-      } $[$wds?]?)
+      } $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed module facet declaration"
 
 /--
@@ -62,7 +62,7 @@ scoped macro (name := packageFacetDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"package_facet " sig:buildDeclSig : command => do
   match sig with
-  | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?]?) =>
+  | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) =>
     let attr ← withRef kw `(Term.attrInstance| package_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
@@ -73,7 +73,7 @@ kw:"package_facet " sig:buildDeclSig : command => do
         name := $name
         config := Lake.mkFacetJobConfig
           fun $pkg => ($defn : IndexBuildM (BuildJob $ty))
-      } $[$wds?]?)
+      } $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
 
 /--
@@ -90,7 +90,7 @@ scoped macro (name := libraryFacetDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"library_facet " sig:buildDeclSig : command => do
   match sig with
-  | `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?]?) =>
+  | `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?:whereDecls]?) =>
     let attr ← withRef kw `(Term.attrInstance| library_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
@@ -101,7 +101,7 @@ kw:"library_facet " sig:buildDeclSig : command => do
         name := $name
         config := Lake.mkFacetJobConfig
           fun $lib => ($defn : IndexBuildM (BuildJob $ty))
-      } $[$wds?]?)
+      } $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed library facet declaration"
 
 --------------------------------------------------------------------------------
@@ -124,7 +124,7 @@ scoped macro (name := targetDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"target " sig:buildDeclSig : command => do
   match sig with
-  | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?]?) =>
+  | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) =>
     let attr ← withRef kw `(Term.attrInstance| target)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
@@ -136,7 +136,7 @@ kw:"target " sig:buildDeclSig : command => do
         name := $name
         config := Lake.mkTargetJobConfig
           fun $pkg => ($defn : IndexBuildM (BuildJob $ty))
-      }  $[$wds?]?)
+      }  $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed target declaration"
 
 
@@ -208,13 +208,13 @@ scoped macro (name := externLibDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 "extern_lib " spec:externLibDeclSpec : command => do
   match spec with
-  | `(externLibDeclSpec| $id:ident $[$pkg?]? := $defn $[$wds?]?) =>
+  | `(externLibDeclSpec| $id:ident $[$pkg?]? := $defn $[$wds?:whereDecls]?) =>
     let attr ← `(Term.attrInstance| extern_lib)
     let attrs := #[attr] ++ expandAttrs attrs?
     let pkgName := mkIdentFrom id `_package.name
     let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static)
     let name := Name.quoteFrom id id.getId
-    `(target $targetId $[$pkg?]? : FilePath := $defn $[$wds?]?
+    `(target $targetId $[$pkg?]? : FilePath := $defn $[$wds?:whereDecls]?
       $[$doc?:docComment]? @[$attrs,*] def $id : ExternLibDecl := {
         pkg := $pkgName
         name := $name
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 0699845ba4..658ab0874e 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);
diff --git a/tests/lean/1026.lean b/tests/lean/1026.lean
index c9b15c96d6..afe792b156 100644
--- a/tests/lean/1026.lean
+++ b/tests/lean/1026.lean
@@ -3,7 +3,7 @@ def foo (n : Nat) : Nat :=
     let x := n - 1
     have := match () with | _ => trivial
     foo x
-termination_by _ n => n
+termination_by n
 decreasing_by sorry
 
 theorem ex : foo 0 = 0 := by
diff --git a/tests/lean/1050.lean b/tests/lean/1050.lean
index 25fc31940d..3a79935125 100644
--- a/tests/lean/1050.lean
+++ b/tests/lean/1050.lean
@@ -7,15 +7,15 @@ namespace Foo
   mutual
     def bar    : {as bs: Type u} → Foo.{u} as bs → bs :=
       bar_aux
+    termination_by _ _ => 0
+    decreasing_by sorry
 
     def bar_aux: {as bs: Type u} → Foo.{u} as bs → bs
       | as, bs, foo _ x => x.bar
+    termination_by _ _ _ => 0
+    decreasing_by sorry
 
   end
-  termination_by
-    bar     => 0
-    bar_aux => 0
-  decreasing_by sorry
 end Foo
 
 
@@ -23,15 +23,15 @@ namespace Foo
   mutual
     def bar1    : {as bs: Type u} → Foo.{u} as bs → bs
       | as, bs, x => bar_aux1 x
+    termination_by _ _ _ => 0
+    decreasing_by sorry
 
     def bar_aux1 : {as bs: Type u} → Foo.{u} as bs → bs
       | as, bs, foo _ x => x.bar1
+    termination_by _ _ _ => 0
+    decreasing_by sorry
 
   end
-  termination_by
-    bar1     => 0
-    bar_aux1 => 0
-  decreasing_by sorry
 end Foo
 
 
@@ -39,12 +39,11 @@ namespace Foo
   mutual
     def bar2    : Foo as bs → bs
       | x => bar_aux2 x
+  termination_by x => (sizeOf x, 1)
 
     def bar_aux2 : Foo as bs → bs
       | foo _ x => x.bar2
+  termination_by x => (sizeOf x, 0)
 
   end
-  termination_by
-    bar2     x => (sizeOf x, 1)
-    bar_aux2 x => (sizeOf x, 0)
 end Foo
diff --git a/tests/lean/1050.lean.expected.out b/tests/lean/1050.lean.expected.out
index 193b6a7dc2..2e395a2ae2 100644
--- a/tests/lean/1050.lean.expected.out
+++ b/tests/lean/1050.lean.expected.out
@@ -1,4 +1,4 @@
-1050.lean:7:2-18:21: error: invalid mutual definition, result types must be in the same universe level, resulting type for `Foo.bar` is
+1050.lean:7:2-18:5: error: invalid mutual definition, result types must be in the same universe level, resulting type for `Foo.bar` is
   Foo as bs → bs : Type (u + 1)
 and for `Foo.bar_aux` is
   bs : Type u
diff --git a/tests/lean/1363.lean b/tests/lean/1363.lean
index 8fe0cd2165..cb5f79a256 100644
--- a/tests/lean/1363.lean
+++ b/tests/lean/1363.lean
@@ -10,13 +10,13 @@ def f : Nat → Nat
 def g : Nat → Nat
   | 0 => 0
   | n + 1 => g n
-termination_by g x => x
+termination_by x => x
 
 @[macro_inline] -- Error
 def h : Nat → Nat → Nat
   | 0, _ => 0
   | n + 1, m => h n m
-termination_by h x y => x
+termination_by x y => x
 
 @[macro_inline] -- Error
 partial def skipMany (p : Parsec α) (it : String.Iterator) : Parsec PUnit := do
diff --git a/tests/lean/906.lean b/tests/lean/906.lean
index 4d8b56670a..821ab1a41d 100644
--- a/tests/lean/906.lean
+++ b/tests/lean/906.lean
@@ -3,7 +3,7 @@ def natPrintAux (n : Nat) (sink : List Char) : List Char :=
   if h0 : n < 10
   then (n.digitChar :: sink)
   else natPrintAux (n / 10) (Nat.digitChar (n % 10) :: sink)
-termination_by _ n => n
+termination_by n
 decreasing_by sorry
 
 set_option maxRecDepth 100  -- default takes ages in debug mode and triggers stack space threshold
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index eccd273053..a038be803a 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -8,8 +8,8 @@ StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
 "(«term_+_» (num \"1\") \"+\" (num \"1\"))"
 StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n  []))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n   []))]"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
@@ -18,8 +18,8 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
 "(«term_+_» (num \"2\") \"+\" (num \"1\"))"
 "(«term_+_» («term_+_» (num \"1\") \"+\" (num \"2\")) \"+\" (num \"1\"))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n  []))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n   []))]"
 "0"
 0
 1
diff --git a/tests/lean/decreasing_by.lean b/tests/lean/decreasing_by.lean
index 8cf1dde9ad..4d39cf2ba3 100644
--- a/tests/lean/decreasing_by.lean
+++ b/tests/lean/decreasing_by.lean
@@ -1,41 +1,138 @@
-mutual
-  inductive Even : Nat → Prop
-    | base : Even 0
-    | step : Odd n → Even (n+1)
-  inductive Odd : Nat → Prop
-    | step : Even n → Odd (n+1)
-end
-decreasing_by assumption
+/-!
+Various tests about `decreasing_by`.
+-/
 
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
- decreasing_by assumption
-end
+-- For concise recursive definition that need well-founded recursion
+-- and `decreasing_by` tactics that would fail if run on the subgoal
+opaque dec1 : Nat → Nat
+axiom dec1_lt (n : Nat) : dec1 n < n
+opaque dec2 : Nat → Nat
+axiom dec2_lt (n : Nat) : dec2 n < n
 
-def g' (n : Nat) :=
-  match n with
-  | 0 => 1
-  | n+1 => g' n * 3
+
+def simple (n : Nat) := n + simple (dec1 n)
+decreasing_by apply dec1_lt
+
+namespace Ex1
+
+-- Multiple goals, explicit termination_By
+def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
+termination_by (n, m)
 decreasing_by
-  h => assumption
+  · simp_wf
+    apply Prod.Lex.right
+    apply dec2_lt
+  · simp_wf
+    apply Prod.Lex.left
+    apply dec1_lt
 
-namespace Test
-mutual
-  def f : Nat → α → α → α
-    | 0, a, b => a
-    | n+1, a, b => g n a b |>.1
+end Ex1
 
-  def g : Nat → α → α → (α × α)
-    | 0, a, b => (a, b)
-    | n+1, a, b => (h n a b, a)
+namespace Ex2
 
-  def h : Nat → α → α → α
-    | 0, a, b => b
-    | n+1, a, b => f n a b
-end
+-- Multiple goals, no termination_By
+-- This does *not* work, because GuessLex does not pass multiple goals to the tactic.
+-- so this tactic script fails.
+def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
 decreasing_by
-  f => assumption
-  g => assumption
+  · simp_wf
+    apply Prod.Lex.right
+    apply dec2_lt
+  · simp_wf
+    apply Prod.Lex.left
+    apply dec1_lt
 
-end Test
+end Ex2
+
+namespace Ex3
+-- Using `all_goals`, explicit termination_By
+def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
+termination_by (n, m)
+decreasing_by all_goals
+  simp_wf
+  first
+    | apply Prod.Lex.right
+      apply dec2_lt
+    | apply Prod.Lex.left
+      apply dec1_lt
+
+end Ex3
+
+namespace Ex4
+
+-- Multiple goals, no termination_By
+-- This does work, because the tactic is flexible enough
+-- (Not a recommended way; complex `decrasing_by` should go along with `termination_by`.)
+def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
+decreasing_by all_goals
+  simp_wf
+  first
+    | apply Prod.Lex.right
+      apply dec2_lt
+    | apply Prod.Lex.left
+      apply dec1_lt
+
+end Ex4
+
+namespace Ex5
+-- Empty proof. Produces parse error and unsolved goals.
+def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
+termination_by n m => (n, m)
+decreasing_by -- Error
+
+end Ex5
+
+namespace Ex6
+
+-- Incomplete tactic
+-- Unsolved goals reported
+def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
+termination_by (n, m)
+decreasing_by apply id -- Error
+
+end Ex6
+
+namespace Ex7
+
+-- Incomplete tactic, no termination_by
+-- Shows guess-lex matrix
+def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
+decreasing_by apply id
+
+end Ex7
+
+namespace Ex8
+
+-- tactic solving just one goal
+-- unsolved goals
+def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
+termination_by (n, m)
+decreasing_by -- Error
+  · simp_wf
+    apply Prod.Lex.right
+    apply dec2_lt
+
+end Ex8
+
+namespace Ex9
+
+-- Incomplete tactic, no termination_by
+-- Shows guess-lex matrix
+def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
+decreasing_by
+  · simp_wf
+    apply Prod.Lex.right
+    apply dec2_lt
+
+end Ex9
+
+namespace Ex10
+
+-- This checks that guess-lex does not run tactics in “recover” mode.
+-- (If it would it would produce the wrong termination order and then we should see errors)
+def foo (n m : Nat) : Nat := foo (n - 1) (dec2 m)
+decreasing_by all_goals
+  · simp_wf
+    apply dec2_lt
+
+end Ex10
diff --git a/tests/lean/decreasing_by.lean.expected.out b/tests/lean/decreasing_by.lean.expected.out
index 2f86a193e4..440f18e87b 100644
--- a/tests/lean/decreasing_by.lean.expected.out
+++ b/tests/lean/decreasing_by.lean.expected.out
@@ -1,4 +1,50 @@
-decreasing_by.lean:8:0-8:24: error: invalid 'decreasing_by' in mutually inductive datatype declaration
-decreasing_by.lean:13:1-13:25: error: invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword
-decreasing_by.lean:21:2-21:3: error: function 'h' not found in current declaration
-decreasing_by.lean:39:2-39:17: error: invalid termination hint element, 'Test.g' and 'Test.f' are in the same clique
+decreasing_by.lean:36:0-43:17: 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) 36:29-43 = ?
+2) 36:46-62 ? _
+Please use `termination_by` to specify a decreasing measure.
+decreasing_by.lean:66:0-73:19: 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) 66:29-43 = ?
+2) 66:46-62 ? _
+Please use `termination_by` to specify a decreasing measure.
+decreasing_by.lean:81:13-83:3: error: unexpected token 'end'; expected '{' or tactic
+decreasing_by.lean:81:0-81:13: error: unsolved goals
+n m : Nat
+⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+    { fst := n, snd := dec2 m } { fst := n, snd := m }
+
+n m : Nat
+⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+    { fst := dec1 n, snd := 100 } { fst := n, snd := m }
+decreasing_by.lean:91:0-91:22: error: unsolved goals
+case a
+n m : Nat
+⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+    { fst := n, snd := dec2 m } { fst := n, snd := m }
+
+n m : Nat
+⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+    { fst := dec1 n, snd := 100 } { fst := n, snd := m }
+decreasing_by.lean:99:0-100:22: 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) 99:29-43 = ?
+2) 99:46-62 ? _
+Please use `termination_by` to specify a decreasing measure.
+decreasing_by.lean:110:0-113:17: error: unsolved goals
+n m : Nat
+⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
+    { fst := dec1 n, snd := 100 } { fst := n, snd := m }
+decreasing_by.lean:121:0-125:17: 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:29-43 = ?
+2) 121:46-62 ? _
+Please use `termination_by` to specify a decreasing measure.
diff --git a/tests/lean/guessLex.lean b/tests/lean/guessLex.lean
index bca3cd7752..9fabe2b711 100644
--- a/tests/lean/guessLex.lean
+++ b/tests/lean/guessLex.lean
@@ -120,18 +120,27 @@ def shadow1 (x2 : Nat) : Nat → Nat
 decreasing_by decreasing_tactic
 
 
+-- This test is a bit moot since #3081, but lets keep it
 def some_n : Nat := 1
 def shadow2 (some_n : Nat) : Nat → Nat
   | 0 => 0
   | .succ n => shadow2 (some_n + 1) n
 decreasing_by decreasing_tactic
 
-def shadow3 (sizeOf : Nat) : Nat → Nat
+-- Shadowing `sizeOf`, as a varying paramter
+def shadowSizeOf1 (sizeOf : Nat) : Nat → Nat
   | 0 => 0
-  | .succ n => shadow3 (sizeOf + 1) n
+  | .succ n => shadowSizeOf1 (sizeOf + 1) n
 decreasing_by decreasing_tactic
 
-def sizeOf : Nat := 2 -- should cause sizeOf to be qualfied below
+-- Shadowing `sizeOf`, as a fixed paramter
+def shadowSizeOf2 (sizeOf : Nat) : Nat → Nat → Nat
+  | 0, m => m
+  | .succ n, m => shadowSizeOf2 sizeOf n m
+decreasing_by decreasing_tactic
+
+-- Shadowing `sizeOf`, as something in the environment
+def sizeOf : Nat := 2
 
 def qualifiedSizeOf (m : Nat) : Nat → Nat
   | 0 => 0
diff --git a/tests/lean/guessLex.lean.expected.out b/tests/lean/guessLex.lean.expected.out
index 5db3d33159..b3939d68e4 100644
--- a/tests/lean/guessLex.lean.expected.out
+++ b/tests/lean/guessLex.lean.expected.out
@@ -1,50 +1,41 @@
-Inferred termination argument:
-termination_by
-  ackermann n m => (sizeOf n, sizeOf m)
-Inferred termination argument:
-termination_by
-  ackermann2 n m => (sizeOf m, sizeOf n)
-Inferred termination argument:
-termination_by
-  ackermannList n m => (sizeOf n, sizeOf m)
-Inferred termination argument:
-termination_by
-  foo2 x1 x2 => (sizeOf x2, sizeOf x1)
-Inferred termination argument:
-termination_by
-  even x1 => sizeOf x1
-  odd x1 => sizeOf x1
-Inferred termination argument:
-termination_by
-  evenWithFixed x1 => sizeOf x1
-  oddWithFixed x1 => sizeOf x1
-Inferred termination argument:
-termination_by
-  ping.pong x1 => (sizeOf x1, 0)
-  ping n => (sizeOf n, 1)
-Inferred termination argument:
-termination_by
-  hasForbiddenArg n _h m => (sizeOf m, sizeOf n)
-Inferred termination argument:
-termination_by
-  blowup x1 x2 x3 x4 x5 x6 x7 x8 =>
+Inferred termination argument: 
+termination_by (sizeOf n, sizeOf m)
+Inferred termination argument: 
+termination_by (sizeOf m, sizeOf n)
+Inferred termination argument: 
+termination_by (sizeOf n, sizeOf m)
+Inferred termination argument: 
+termination_by x1 x2 => (sizeOf x2, sizeOf x1)
+Inferred termination argument: 
+termination_by x1 => sizeOf x1
+Inferred termination argument: 
+termination_by x1 => sizeOf x1
+Inferred termination argument: 
+termination_by x1 => sizeOf x1
+Inferred termination argument: 
+termination_by x1 => sizeOf x1
+Inferred termination argument: 
+termination_by x1 => (sizeOf x1, 0)
+Inferred termination argument: 
+termination_by (sizeOf n, 1)
+Inferred termination argument: 
+termination_by (sizeOf m, sizeOf n)
+Inferred termination argument: 
+termination_by x1 x2 x3 x4 x5 x6 x7 x8 =>
   (sizeOf x8, sizeOf x7, sizeOf x6, sizeOf x5, sizeOf x4, sizeOf x3, sizeOf x2, sizeOf x1)
-Inferred termination argument:
-termination_by
-  dependent x1 x2 => (sizeOf x1, sizeOf x2)
-Inferred termination argument:
-termination_by
-  eval a => (sizeOf a, 1)
-  eval_add a => (sizeOf a, 0)
-Inferred termination argument:
-termination_by
-  shadow1 x2 x2' => sizeOf x2'
-Inferred termination argument:
-termination_by
-  shadow2 some_n' x2 => sizeOf x2
-Inferred termination argument:
-termination_by
-  shadow3 sizeOf' x2 => sizeOf x2
-Inferred termination argument:
-termination_by
-  qualifiedSizeOf m x2 => SizeOf.sizeOf x2
+Inferred termination argument: 
+termination_by x1 x2 => (sizeOf x1, sizeOf x2)
+Inferred termination argument: 
+termination_by (sizeOf a, 1)
+Inferred termination argument: 
+termination_by (sizeOf a, 0)
+Inferred termination argument: 
+termination_by x2' => sizeOf x2'
+Inferred termination argument: 
+termination_by x2 => sizeOf x2
+Inferred termination argument: 
+termination_by x2 => SizeOf.sizeOf x2
+Inferred termination argument: 
+termination_by x1 x2 => SizeOf.sizeOf x1
+Inferred termination argument: 
+termination_by x2 => SizeOf.sizeOf x2
diff --git a/tests/lean/guessLexFailures.lean b/tests/lean/guessLexFailures.lean
index 384eb0e90c..667244671b 100644
--- a/tests/lean/guessLexFailures.lean
+++ b/tests/lean/guessLexFailures.lean
@@ -99,7 +99,7 @@ namespace TrickyCode
 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
+-- termination_by n
 decreasing_by decreasing_tactic
 
 
@@ -109,7 +109,7 @@ decreasing_by decreasing_tactic
 -- 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 := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn2 n (.succ m)))
-termination_by badCasesOn2 n m => n
+termination_by n
 decreasing_by decreasing_tactic
 
 -- The GuessLex code at does not like `casesOn` alternative with insufficient lambdas
@@ -119,7 +119,7 @@ def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) :=
 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
+-- termination_by n
 decreasing_by decreasing_tactic
 
 
@@ -127,7 +127,7 @@ decreasing_by decreasing_tactic
 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
+termination_by n
 decreasing_by decreasing_tactic
 
 end TrickyCode
diff --git a/tests/lean/guessLexTricky.lean b/tests/lean/guessLexTricky.lean
index cf73d92e8f..cc4ace4968 100644
--- a/tests/lean/guessLexTricky.lean
+++ b/tests/lean/guessLexTricky.lean
@@ -39,15 +39,32 @@ macro_rules | `(tactic|search_lex $ts:tacticSeq) => `(tactic| (
 mutual
 def prod (x y z : Nat) : Nat :=
   if y % 2 = 0 then eprod x y z else oprod x y z
+decreasing_by
+  -- TODO: Why does it not work to wrap it all in `all_goals`?
+  all_goals simp_wf
+  · search_lex solve
+      | decreasing_trivial
+      | apply Nat.bitwise_rec_lemma; assumption
+  · search_lex solve
+      | decreasing_trivial
+      | apply Nat.bitwise_rec_lemma; assumption
+
 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
+
+def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
+decreasing_by
+  simp_wf
+  search_lex solve
+    | decreasing_trivial
+    | apply Nat.bitwise_rec_lemma; assumption
+
+end
+-- termination_by
+--   prod x y z => (y, 2)
+--   oprod x y z => (y, 1)
+--   eprod x y z => (y, 0)
diff --git a/tests/lean/guessLexTricky.lean.expected.out b/tests/lean/guessLexTricky.lean.expected.out
index 2cbb92446e..389959b3e5 100644
--- a/tests/lean/guessLexTricky.lean.expected.out
+++ b/tests/lean/guessLexTricky.lean.expected.out
@@ -1,5 +1,6 @@
-Inferred termination argument:
-termination_by
-  prod x y z => (sizeOf y, 1, 0)
-  oprod x y z => (sizeOf y, 0, 1)
-  eprod x y z => (sizeOf y, 0, 0)
+Inferred termination argument: 
+termination_by (sizeOf y, 1, 0)
+Inferred termination argument: 
+termination_by (sizeOf y, 0, 1)
+Inferred termination argument: 
+termination_by (sizeOf y, 0, 0)
diff --git a/tests/lean/guessLexTricky2.lean.expected.out b/tests/lean/guessLexTricky2.lean.expected.out
index e33d62d488..758c630cb0 100644
--- a/tests/lean/guessLexTricky2.lean.expected.out
+++ b/tests/lean/guessLexTricky2.lean.expected.out
@@ -1,4 +1,4 @@
-Inferred termination argument:
-termination_by
-  pedal x1 x2 x3 => (sizeOf x1, sizeOf x2, 0)
-  coast x1 x2 x3 => (sizeOf x1, sizeOf x2, 1)
+Inferred termination argument: 
+termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 0)
+Inferred termination argument: 
+termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 1)
diff --git a/tests/lean/heapSort.lean b/tests/lean/heapSort.lean
index a92bcca95a..e56bb51e6f 100644
--- a/tests/lean/heapSort.lean
+++ b/tests/lean/heapSort.lean
@@ -32,7 +32,7 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
       rw [a.size_swap i j]; sorry
     let ⟨a₂, h₂⟩ := heapifyDown lt a' j'
     ⟨a₂, h₂.trans (a.size_swap i j)⟩
-termination_by _ => a.size - i
+termination_by a.size - i
 decreasing_by assumption
 
 @[simp] theorem size_heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
@@ -65,7 +65,7 @@ if i0 : i.1 = 0 then ⟨a, rfl⟩ else
     let ⟨a₂, h₂⟩ := heapifyUp lt a' ⟨j.1, by rw [a.size_swap i j]; exact j.2⟩
     ⟨a₂, h₂.trans (a.size_swap i j)⟩
   else ⟨a, rfl⟩
-termination_by _ => i.1
+termination_by i.1
 decreasing_by assumption
 
 @[simp] theorem size_heapifyUp (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
@@ -168,9 +168,9 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
       have : a.popMax.size < a.size := by
         simp; exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
       loop a.popMax (out.push x)
+    termination_by a.size
+    decreasing_by assumption
   loop (a.toBinaryHeap gt) #[]
-termination_by _ => a.size
-decreasing_by assumption
 
 attribute [simp] Array.heapSort.loop
 #check Array.heapSort.loop._eq_1
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 0bef6295f1..c2e271dd72 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -188,7 +188,7 @@ example : Nat → Nat → Nat := by
       --^ textDocument/hover
 
 def g (n : Nat) : Nat := g 0
-termination_by g n => n
+termination_by n => n
 decreasing_by have n' := n; admit
                        --^ textDocument/hover
 
diff --git a/tests/lean/letRecMissingAnnotation.lean b/tests/lean/letRecMissingAnnotation.lean
index 8cebbfa388..c298310ede 100644
--- a/tests/lean/letRecMissingAnnotation.lean
+++ b/tests/lean/letRecMissingAnnotation.lean
@@ -4,5 +4,5 @@ def sum (as : Array Nat) : Nat :=
       go (i+2) (s + as.get ⟨i, h⟩) -- Error
     else
       s
+    termination_by as.size - i
   go 0 0
-termination_by go i _ => as.size - i
diff --git a/tests/lean/mutwf1.lean b/tests/lean/mutwf1.lean
index 82b74ff718..a00c5f199f 100644
--- a/tests/lean/mutwf1.lean
+++ b/tests/lean/mutwf1.lean
@@ -4,24 +4,24 @@ mutual
     | n, true  => 2 * f n false
     | 0, false => 1
     | n, false => n + g n
+  termination_by n b => (n, if b then 2 else 1)
+  decreasing_by
+  all_goals simp_wf
+  · apply Prod.Lex.right; decide
+  · apply Prod.Lex.right; decide
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then
       f (n-1) true
     else
       n
-end
-termination_by
-  f n b => (n, if b then 2 else 1)
-  g n => (n, 0)
-decreasing_by
-  simp_wf
-  first
-  | apply Prod.Lex.left
-    apply Nat.pred_lt
-  | apply Prod.Lex.right
-    decide
+  termination_by (n, 0)
+  decreasing_by
+  all_goals simp_wf
+  apply Prod.Lex.left
+  apply Nat.pred_lt
   done -- should fail
+end
 end Ex1
 
 
@@ -31,14 +31,13 @@ mutual
     | n, true  => 2 * f n false
     | 0, false => 1
     | n, false => n + g (n+1) -- Error
+  termination_by n b => (n, if b then 2 else 1)
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then
       f (n-1) true
     else
       n
+  termination_by (n, 0)
 end
-termination_by
-  f n b => (n, if b then 2 else 1)
-  g n   => (n, 0)
 end Ex2
diff --git a/tests/lean/mutwf1.lean.expected.out b/tests/lean/mutwf1.lean.expected.out
index 066ec9cf1a..e0f562e89e 100644
--- a/tests/lean/mutwf1.lean.expected.out
+++ b/tests/lean/mutwf1.lean.expected.out
@@ -1,4 +1,4 @@
-mutwf1.lean:24:2-24:6: error: unsolved goals
+mutwf1.lean:23:2-23:6: error: unsolved goals
 case h.a
 n : Nat
 h : n ≠ 0
diff --git a/tests/lean/run/1017.lean b/tests/lean/run/1017.lean
index 544234472d..a01fd84fee 100644
--- a/tests/lean/run/1017.lean
+++ b/tests/lean/run/1017.lean
@@ -50,6 +50,6 @@ def mwe [Stream ρ τ] (acc : α) : {l : ρ // isFinite l} → α
     | some (x,xs) =>
       have h_next : hasNext l xs := by exists x
       mwe acc ⟨xs, by sorry⟩
-  termination_by _ l => l
+  termination_by l => l
 
 end Stream
diff --git a/tests/lean/run/1171.lean b/tests/lean/run/1171.lean
index d8a90e5d6c..79e585f7c7 100644
--- a/tests/lean/run/1171.lean
+++ b/tests/lean/run/1171.lean
@@ -6,7 +6,7 @@ def Nat.hasDecEq: (a: Nat) → (b: Nat) → Decidable (Eq a b)
   match h:hasDecEq n m with -- it works without `h:`
   | isTrue heq => isTrue  (heq ▸ rfl)
   | isFalse hne => isFalse (Nat.noConfusion · (λ heq  => absurd heq hne))
-termination_by _ a b => (a, b)
+termination_by a b => (a, b)
 
 set_option pp.proofs true
 #print Nat.hasDecEq
diff --git a/tests/lean/run/1228.lean b/tests/lean/run/1228.lean
index 45dd064b49..356e4a54ba 100644
--- a/tests/lean/run/1228.lean
+++ b/tests/lean/run/1228.lean
@@ -10,7 +10,7 @@ namespace Foo
       cases h₂ : n; sorry
       have: Bar s' := sorry
       exact ex₁ this
-  termination_by _ => sizeOf s
+  termination_by sizeOf s
 
   theorem ex₂
     {s: Foo n}
@@ -22,7 +22,7 @@ namespace Foo
       have: Bar s' := sorry
       have hterm: sizeOf s' < sizeOf s := by simp_all_arith
       exact ex₂ this
-  termination_by _ => sizeOf s
+  termination_by sizeOf s
 
   theorem ex₃ {s: Foo n} (H: s.Bar): True := by
     cases h₁ : s
@@ -32,7 +32,7 @@ namespace Foo
       | _ =>
         have: Bar s' := sorry
         exact ex₃ this
-  termination_by _ => sizeOf s
+  termination_by sizeOf s
 
   -- it works
   theorem ex₄ {s: Foo n} (H: s.Bar): True := by
@@ -43,4 +43,4 @@ namespace Foo
     | _ =>
       have: Bar s' := sorry
       exact ex₄ this
-  termination_by _ => sizeOf s
+  termination_by sizeOf s
diff --git a/tests/lean/run/1848.lean b/tests/lean/run/1848.lean
index a59b1bdeb9..b51d5d0338 100644
--- a/tests/lean/run/1848.lean
+++ b/tests/lean/run/1848.lean
@@ -1,11 +1,11 @@
 abbrev f : Nat → Nat
   | 0 => 0
   | n + 1 => f n
-termination_by _ n => n
+termination_by n => n
 
 mutual
 abbrev f1 : Nat → Nat
   | 0 => 0
   | n + 1 => f1 n
+termination_by n => n
 end
-termination_by _ n => n
diff --git a/tests/lean/run/2810.lean b/tests/lean/run/2810.lean
index 59037eddc7..0be282ac59 100644
--- a/tests/lean/run/2810.lean
+++ b/tests/lean/run/2810.lean
@@ -19,7 +19,7 @@ def f3 (n : Nat) : Nat :=
   match n with
   | 0 => 0
   | n + 1 => (f3) n
-termination_by f3 n => n
+termination_by n
 
 -- Same with rewrite
 
diff --git a/tests/lean/run/860.lean b/tests/lean/run/860.lean
index 106c708b39..2f63248af2 100644
--- a/tests/lean/run/860.lean
+++ b/tests/lean/run/860.lean
@@ -13,17 +13,19 @@ private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
     · apply Nat.zero_lt_succ
 
 def pack (n: Nat) : List Nat :=
-  let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
-    let next (n: Nat) := n / 2;
-    match n with
-    | Nat.zero => List.cons acc accs
-    | n+1 => match evenq n with
-      | true => loop (next n) 0 (List.cons acc accs)
-      | false => loop (next n) (acc+1) accs
+  let rec
+    loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
+      let next (n: Nat) := n / 2;
+      match n with
+      | Nat.zero => List.cons acc accs
+      | n+1 => match evenq n with
+        | true => loop (next n) 0 (List.cons acc accs)
+        | false => loop (next n) (acc+1) accs
+    termination_by n
+    decreasing_by all_goals
+      simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
+      apply pack_loop_terminates
+
   loop n 0 []
-termination_by _ n _ _ => n
-decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
-  apply pack_loop_terminates
 
 #eval pack 27
diff --git a/tests/lean/run/879.lean b/tests/lean/run/879.lean
index c7fbf89a02..162643e69e 100644
--- a/tests/lean/run/879.lean
+++ b/tests/lean/run/879.lean
@@ -1,17 +1,4 @@
 variable (a : Nat)
 
 def foo1 (b c : Nat) := if h : b = 0 then a + c else foo1 (b - 1) c
-termination_by _ => b
-
-def foo2 (b c : Nat) := if h : b = 0 then a + c else foo2 (b - 1) c
-termination_by
-  foo2 x y z => y
-
-def foo3 (b c : Nat) := if h : b = 0 then a + c else foo3 (b - 1) c
-termination_by
-  _ x y z => y
-
-def foo4 (b c : Nat) := if h : b = 0 then a + c else foo4 (b - 1) c
-termination_by
-  -- We can rename from right to left
-  foo4 y _ => y
+termination_by b
diff --git a/tests/lean/run/955.lean b/tests/lean/run/955.lean
index 16016899c8..92a2221a3b 100644
--- a/tests/lean/run/955.lean
+++ b/tests/lean/run/955.lean
@@ -3,11 +3,15 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  termination_by n =>
+    match n with
+    | _ => n
+
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  termination_by n =>
+    match n with
+    | _ => n
 end
-termination_by _ n =>
-  match n with
-  | _ => n
 end Ex2
diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean
index 61dbaae4a5..e86cc92c8a 100644
--- a/tests/lean/run/ack.lean
+++ b/tests/lean/run/ack.lean
@@ -2,4 +2,4 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by _ a b => (a, b)
+termination_by a b => (a, b)
diff --git a/tests/lean/run/addDecorationsWithoutPartial.lean b/tests/lean/run/addDecorationsWithoutPartial.lean
index 4c9910c72e..3fce9f0fb9 100644
--- a/tests/lean/run/addDecorationsWithoutPartial.lean
+++ b/tests/lean/run/addDecorationsWithoutPartial.lean
@@ -77,4 +77,4 @@ def addDecorations (e : Expr) : Expr :=
       let rest := Expr.forallE name newType newBody data
       some <| mkApp2 (mkConst `SlimCheck.NamedBinder) (mkStrLit n) rest
     | _ => none
-decreasing_by exact Nat.le_trans (by simp_arith) h
+decreasing_by all_goals exact Nat.le_trans (by simp_arith) h
diff --git a/tests/lean/run/binrec.lean b/tests/lean/run/binrec.lean
index 6933b6473a..ab329c80d6 100644
--- a/tests/lean/run/binrec.lean
+++ b/tests/lean/run/binrec.lean
@@ -44,8 +44,8 @@ def Nat.binrec
     bit_div_even h₂ ▸ ind false (n / 2) (fun _ => binrec motive base ind (n / 2))
   else
     bit_div_odd h₂ ▸ ind true  (n / 2) (fun _ => binrec motive base ind (n / 2))
-termination_by _ n => n
-decreasing_by exact Nat.div2_lt h₁
+termination_by n
+decreasing_by all_goals exact Nat.div2_lt h₁
 
 theorem Nat.binind
     (motive : Nat → Prop)
diff --git a/tests/lean/run/bubble.lean b/tests/lean/run/bubble.lean
index 497a904c93..19296830e5 100644
--- a/tests/lean/run/bubble.lean
+++ b/tests/lean/run/bubble.lean
@@ -11,4 +11,4 @@ def List.bubblesort [LT α] [DecidableRel (· < · : α → α → Prop)] (l : L
         ⟨y :: zs, by simp[h, ← he]⟩
       else
         ⟨x :: y :: ys, by simp[h]⟩
-termination_by _ => l.length
+termination_by l.length
diff --git a/tests/lean/run/byteSliceIssue.lean b/tests/lean/run/byteSliceIssue.lean
index fc00a3366f..76147a5c2f 100644
--- a/tests/lean/run/byteSliceIssue.lean
+++ b/tests/lean/run/byteSliceIssue.lean
@@ -39,7 +39,7 @@ def forIn.loop [Monad m] (f : UInt8 → β → m (ForInStep β))
     | ForInStep.done b => pure b
     | ForInStep.yield b => have := Nat.Up.next h; loop f arr off _end (i+1) b
   else pure b
-termination_by _ => _end - i
+termination_by _end - i
 
 attribute [simp] ByteSlice.forIn.loop
 #check @ByteSlice.forIn.loop._eq_1
diff --git a/tests/lean/run/constProp.lean b/tests/lean/run/constProp.lean
index 67ecfb8e57..28ed047673 100644
--- a/tests/lean/run/constProp.lean
+++ b/tests/lean/run/constProp.lean
@@ -397,7 +397,7 @@ def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.leng
     match σ₂.find? x with
     | some w => if v = w then (x, v) :: join σ₁' σ₂ else join σ₁' σ₂
     | none => join σ₁' σ₂
-termination_by _ σ₁ _ => σ₁.length
+termination_by σ₁.length
 
 local notation "⊥" => []
 
@@ -468,7 +468,7 @@ theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ :=
       next => apply cons_le_cons; apply le_trans ih (erase_le _)
       next => apply le_trans ih (erase_le_cons (le_refl _))
     next h => apply le_trans ih (erase_le_cons (le_refl _))
-termination_by _ σ₁ _ => σ₁.length
+termination_by σ₁.length
 
 theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ :=
   le_trans (join_le_left σ₁ σ₃) h
@@ -485,7 +485,7 @@ theorem State.join_le_right (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ :
       split <;> simp [*]
       next => apply cons_le_of_eq ih h
     next h => assumption
-termination_by _ σ₁ _ => σ₁.length
+termination_by σ₁.length
 
 theorem State.join_le_right_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₃.join σ₁ ≼ σ₂ :=
   le_trans (join_le_right σ₃ σ₁) h
diff --git a/tests/lean/run/decreasingTacticUpdatedEnvIssue.lean b/tests/lean/run/decreasingTacticUpdatedEnvIssue.lean
index 76d829809f..99ce246787 100644
--- a/tests/lean/run/decreasingTacticUpdatedEnvIssue.lean
+++ b/tests/lean/run/decreasingTacticUpdatedEnvIssue.lean
@@ -21,4 +21,4 @@ def f (x : Nat) : Nat :=
     1
   else
     f (g x (x > 0)) + 2
-termination_by f x => x
+termination_by x
diff --git a/tests/lean/run/defaultEliminator.lean b/tests/lean/run/defaultEliminator.lean
index bcd279164f..6a29dcebd4 100644
--- a/tests/lean/run/defaultEliminator.lean
+++ b/tests/lean/run/defaultEliminator.lean
@@ -9,8 +9,8 @@
     | x+1, 0   => succ_zero x (go x 0)
     | 0,   y+1 => zero_succ y (go 0 y)
     | x+1, y+1 => succ_succ x y (go x y)
+    termination_by x y => (x, y)
   go x y
-termination_by go x y => (x, y)
 
 def f (x y : Nat) :=
   match x, y with
@@ -18,7 +18,7 @@ def f (x y : Nat) :=
   | x+1, 0   => f x 0
   | 0,   y+1 => f 0 y
   | x+1, y+1 => f x y
-termination_by f x y => (x, y)
+termination_by (x, y)
 
 example (x y : Nat) : f x y > 0 := by
   induction x, y with
diff --git a/tests/lean/run/eqnsAtSimp.lean b/tests/lean/run/eqnsAtSimp.lean
index 8a9e97a3dc..fde04b5d37 100644
--- a/tests/lean/run/eqnsAtSimp.lean
+++ b/tests/lean/run/eqnsAtSimp.lean
@@ -2,13 +2,17 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
+
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
 end
-decreasing_by
-  simp [measure, invImage, InvImage, Nat.lt_wfRel]
-  apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with
diff --git a/tests/lean/run/eqnsAtSimp2.lean b/tests/lean/run/eqnsAtSimp2.lean
index 646f12d499..9f2f33d279 100644
--- a/tests/lean/run/eqnsAtSimp2.lean
+++ b/tests/lean/run/eqnsAtSimp2.lean
@@ -2,11 +2,13 @@ mutual
   @[simp] def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  decreasing_by apply Nat.lt_succ_self
+
   @[simp] def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  decreasing_by apply Nat.lt_succ_self
 end
-decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with
diff --git a/tests/lean/run/instanceIssues.lean b/tests/lean/run/instanceIssues.lean
index c0253b9124..360e71d0e1 100644
--- a/tests/lean/run/instanceIssues.lean
+++ b/tests/lean/run/instanceIssues.lean
@@ -5,5 +5,5 @@ inductive Vector (α : Type u) : Nat → Type u
 def test [Monad m] (xs : Vector α a) : m Unit :=
   match xs with
   | Vector.nil => return ()
-  | Vector.cons x xs => test xs
-termination_by test xs => sizeOf xs
+  | Vector.cons _ xs => test xs
+termination_by sizeOf xs
diff --git a/tests/lean/run/issue2628.lean b/tests/lean/run/issue2628.lean
index d9c7e9f90d..d63c766d54 100644
--- a/tests/lean/run/issue2628.lean
+++ b/tests/lean/run/issue2628.lean
@@ -8,12 +8,13 @@ mutual
 def foo : Nat → Nat
   | .zero => 0
   | .succ n => (id bar) n
+decreasing_by sorry
+
 def bar : Nat → Nat
   | .zero => 0
   | .succ n => foo n
-end
-termination_by foo n => n; bar n => n
 decreasing_by sorry
+end
 
 end Ex1
 
@@ -28,12 +29,15 @@ def foo : Nat → Nat → Nat
   | .zero, _m => 0
   | .succ n, .zero => (id' (bar n)) .zero
   | .succ n, m => (id' bar) n m
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
+
 def bar : Nat → Nat → Nat
   | .zero, _m => 0
   | .succ n, m => foo n m
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 end
-termination_by foo n m => (n,m); bar n m => (n,m)
-decreasing_by sorry
 
 end Ex2
 
@@ -44,12 +48,12 @@ mutual
 def foo : Nat → Nat → Nat
   | .zero => fun _ => 0
   | .succ n => fun m => (id bar) n m
+decreasing_by all_goals sorry
 def bar : Nat → Nat → Nat
   | .zero => fun _ => 0
   | .succ n => fun m => foo n m
+decreasing_by all_goals sorry
 end
-termination_by foo n => n; bar n => n
-decreasing_by sorry
 
 end Ex3
 
@@ -62,12 +66,14 @@ def foo : Nat → Nat → Nat → Nat
   | .zero, _m => fun _ => 0
   | .succ n, .zero => fun k => (id' (bar n)) .zero k
   | .succ n, m => fun k => (id' bar) n m k
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 def bar : Nat → Nat → Nat → Nat
   | .zero, _m => fun _ => 0
   | .succ n, m => fun k => foo n m k
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 end
-termination_by foo n m => (n,m); bar n m => (n,m)
-decreasing_by sorry
 
 end Ex4
 
@@ -80,12 +86,12 @@ mutual
 def foo : FunType
   | .zero => 0
   | .succ n => (id bar) n
+decreasing_by all_goals sorry
 def bar : Nat → Nat
   | .zero => 0
   | .succ n => foo n
+decreasing_by all_goals sorry
 end
-termination_by foo n => n; bar n => n
-decreasing_by sorry
 
 end Ex5
 
@@ -98,11 +104,13 @@ def foo : Nat → Nat → Nat → Nat
   | .zero, _m => fun _ => 0
   | .succ n, .zero => fun k => (id' (bar n)) .zero k
   | .succ n, m => fun k => (id' bar) n m k
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 def bar : Nat → Fun3Type
   | .zero, _m => fun _ => 0
   | .succ n, m => fun k => foo n m k
+termination_by n m => (n,m)
+decreasing_by all_goals sorry
 end
-termination_by foo n m => (n,m); bar n m => (n,m)
-decreasing_by sorry
 
 end Ex6
diff --git a/tests/lean/run/issue2883.lean b/tests/lean/run/issue2883.lean
index b7541f94ec..2b07da1dc3 100644
--- a/tests/lean/run/issue2883.lean
+++ b/tests/lean/run/issue2883.lean
@@ -15,11 +15,10 @@ end
 mutual
   def foo : B → Prop
   | .fromA a => bar a 0
+  termination_by x => sizeOf x
 
   def bar : A → Nat → Prop
   | .baseA   => (fun _ => True)
   | .fromB b => (fun (c : Nat) => ∃ (t : Nat), foo b)
+  termination_by x => sizeOf x
 end
-termination_by
-  foo x => sizeOf x
-  bar x => sizeOf x
diff --git a/tests/lean/run/issue2925.lean b/tests/lean/run/issue2925.lean
index 851ad59967..e7af477c7d 100644
--- a/tests/lean/run/issue2925.lean
+++ b/tests/lean/run/issue2925.lean
@@ -5,11 +5,13 @@ mutual
 def foo : FunType
   | .zero => 0
   | .succ n => bar n
+termination_by n => n
 def bar : Nat → Nat
   | .zero => 0
   | .succ n => baz n 0
+termination_by n => n
 def baz : Fun2Type
   | .zero, m => 0
   | .succ n, m => foo n
+termination_by n _ => n
 end
-termination_by foo n => n; bar n => n; baz n _ => n
diff --git a/tests/lean/run/letrecWFIssue.lean b/tests/lean/run/letrecWFIssue.lean
index 17158fcdca..99a5151289 100644
--- a/tests/lean/run/letrecWFIssue.lean
+++ b/tests/lean/run/letrecWFIssue.lean
@@ -16,7 +16,10 @@ def Tree.size : Tree α → Nat
       apply Nat.lt_succ_self
     sizeList l
   | Tree.leaf _ => 1
-where sizeList : TreeList α → Nat
+-- use automatically synthesized size function, which is not quite the number of leaves
+termination_by t => sizeOf t
+where
+  sizeList : TreeList α → Nat
   | TreeList.nil => 0
   | TreeList.cons t l =>
     have : sizeOf t < 1 + sizeOf t + sizeOf l := by
@@ -28,7 +31,4 @@ where sizeList : TreeList α → Nat
       apply Nat.lt_succ_of_le
       apply Nat.le_add_left
     t.size + sizeList l
--- use automatically synthesized size function, which is not quite the number of leaves
-termination_by
-  size t => sizeOf t
-  sizeList l => sizeOf l
+  termination_by l => sizeOf l
diff --git a/tests/lean/run/mergeSortCPDT.lean b/tests/lean/run/mergeSortCPDT.lean
index 92bf11914d..680f44d95a 100644
--- a/tests/lean/run/mergeSortCPDT.lean
+++ b/tests/lean/run/mergeSortCPDT.lean
@@ -47,4 +47,4 @@ def List.mergeSort (p : α → α → Bool) (as : List α) : List α :=
       merge p (mergeSort p as') (mergeSort p bs')
   else
     as
-termination_by _ as => as.length
+termination_by as.length
diff --git a/tests/lean/run/mut_ind_wf.lean b/tests/lean/run/mut_ind_wf.lean
index fb01c71a8f..69aea42450 100644
--- a/tests/lean/run/mut_ind_wf.lean
+++ b/tests/lean/run/mut_ind_wf.lean
@@ -19,6 +19,8 @@ def Tree.size : Tree α → Nat
       apply Nat.lt_succ_self
     sizeList l
   | Tree.leaf _ => 1
+-- use automatically synthesized size function, which is not quite the number of leaves
+termination_by t => sizeOf t
 
 def Tree.sizeList : TreeList α → Nat
   | TreeList.nil => 0
@@ -32,11 +34,8 @@ def Tree.sizeList : TreeList α → Nat
       apply Nat.lt_succ_of_le
       apply Nat.le_add_left
     t.size + sizeList l
+termination_by l => sizeOf l
 end
--- use automatically synthesized size function, which is not quite the number of leaves
-termination_by
-  size t => sizeOf t
-  sizeList l => sizeOf l
 
 end Mutual
 
@@ -54,6 +53,7 @@ def Tree.size : Tree α → Nat
       apply Nat.lt_succ_self
     sizeList l
   | Tree.leaf _ => 1
+termination_by t => sizeOf t
 
 def Tree.sizeList : List (Tree α) → Nat
   | [] => 0
@@ -67,9 +67,7 @@ def Tree.sizeList : List (Tree α) → Nat
       apply Nat.lt_succ_of_le
       apply Nat.le_add_left
     t.size + sizeList l
+termination_by l => sizeOf l
 end
-termination_by
-  size t => sizeOf t
-  sizeList l => sizeOf l
 
 end Nested
diff --git a/tests/lean/run/mutwf1.lean b/tests/lean/run/mutwf1.lean
index 2e75be80be..db76e4ac6b 100644
--- a/tests/lean/run/mutwf1.lean
+++ b/tests/lean/run/mutwf1.lean
@@ -3,19 +3,18 @@ mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n, a, b => g a n b |>.1
+  termination_by n _ _ => (n, 2)
 
   def g : α → Nat → α → (α × α)
     | a, 0, b => (a, b)
     | a, n, b => (h a b n, a)
+  termination_by _ n _ => (n, 1)
 
   def h : α → α → Nat → α
     | a, b, 0 => b
     | a, b, n+1 => f n a b
+  termination_by _ _ n => (n, 0)
 end
-termination_by
-  f n _ _ => (n, 2)
-  g _ n _ => (n, 1)
-  h _ _ n => (n, 0)
 
 #print f
 #print g
diff --git a/tests/lean/run/mutwf2.lean b/tests/lean/run/mutwf2.lean
index d0cf4a6555..25b023121e 100644
--- a/tests/lean/run/mutwf2.lean
+++ b/tests/lean/run/mutwf2.lean
@@ -3,11 +3,12 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  termination_by n => n
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  termination_by n => n
 end
-termination_by _ n => n
 
 #print isEven
 #print isOdd
diff --git a/tests/lean/run/mutwf3.lean b/tests/lean/run/mutwf3.lean
index 596d1cf517..1c1fefa9a1 100644
--- a/tests/lean/run/mutwf3.lean
+++ b/tests/lean/run/mutwf3.lean
@@ -3,26 +3,30 @@ mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n, a, b => g a n b |>.1
+  termination_by n _ _ => (n, 2)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.right
+    decide
 
   def g : α → Nat → α → (α × α)
     | a, 0, b => (a, b)
     | a, n, b => (h a b n, a)
+  termination_by _ n _ => (n, 1)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.right
+    decide
 
   def h : α → α → Nat → α
     | _a, b, 0 => b
     | a, b, n+1 => f n a b
-end
-termination_by
-  f n _ _ => (n, 2)
-  g _ n _ => (n, 1)
-  h _ _ n => (n, 0)
-decreasing_by
-  simp_wf
-  first
-  | apply Prod.Lex.left
+  termination_by _ _ n => (n, 0)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.left
     apply Nat.lt_succ_self
-  | apply Prod.Lex.right
-    decide
+end
 
 #eval f 5 'a' 'b'
 #print f
@@ -36,19 +40,18 @@ mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n, a, b => g a n b |>.1
+  termination_by n _ _ => (n, 2)
 
   def g : α → Nat → α → (α × α)
     | a, 0, b => (a, b)
     | a, n, b => (h a b n, a)
+  termination_by _ n _ => (n, 1)
 
   def h : α → α → Nat → α
     | a, b, 0 => b
     | a, b, n+1 => f n a b
+  termination_by _ _ n => (n, 0)
 end
-termination_by
-  f n _ _ => (n, 2)
-  g _ n _ => (n, 1)
-  h _ _ n => (n, 0)
 
 #print f._unary._mutual
 
diff --git a/tests/lean/run/mutwf4.lean b/tests/lean/run/mutwf4.lean
index acb31573cc..b49943ee22 100644
--- a/tests/lean/run/mutwf4.lean
+++ b/tests/lean/run/mutwf4.lean
@@ -1,19 +1,17 @@
-set_option trace.Elab.definition.wf true in
 mutual
   def f : Nat → Bool → Nat
     | n, true  => 2 * f n false
     | 0, false => 1
     | n, false => n + g n
+  termination_by n b => (n, if b then 2 else 1)
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then
       f (n-1) true
     else
       n
+  termination_by (n, 0)
 end
-termination_by
-  f n b => (n, if b then 2 else 1)
-  g n   => (n, 0)
 
 #print f
 #print g
diff --git a/tests/lean/run/nestedIssueMatch.lean b/tests/lean/run/nestedIssueMatch.lean
index 0e91aaf6ee..5b0ac54b41 100644
--- a/tests/lean/run/nestedIssueMatch.lean
+++ b/tests/lean/run/nestedIssueMatch.lean
@@ -5,7 +5,7 @@ def g (t : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g n
   | 0 => 0
-decreasing_by sorry
+decreasing_by all_goals sorry
 
 attribute [simp] g
 
diff --git a/tests/lean/run/nestedWF.lean b/tests/lean/run/nestedWF.lean
index c69d755153..8caabf2b7d 100644
--- a/tests/lean/run/nestedWF.lean
+++ b/tests/lean/run/nestedWF.lean
@@ -4,6 +4,9 @@ mutual
 def h (c : Nat) (x : Nat) := match g c x c c with
   | 0 => 1
   | r => r + 2
+termination_by 0
+decreasing_by all_goals sorry
+
 def g (c : Nat) (t : Nat) (a b : Nat) : Nat := match t with
   | (n+1) => match g c n a b with
     | 0 => 0
@@ -11,15 +14,15 @@ def g (c : Nat) (t : Nat) (a b : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g c m a b
   | 0 => f c 0
+termination_by 0
+decreasing_by all_goals sorry
+
 def f (c : Nat) (x : Nat) := match h c x with
   | 0 => 1
   | r => f c r
+termination_by 0
+decreasing_by all_goals sorry
 end
-termination_by
-  g x a b => 0
-  f c x => 0
-  h c x => 0
-decreasing_by sorry
 
 attribute [simp] g
 attribute [simp] h
@@ -43,7 +46,7 @@ def g (t : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g n
   | 0 => 0
-decreasing_by sorry
+decreasing_by all_goals sorry
 
 theorem ex1 : g 0 = 0 := by
   rw [g]
diff --git a/tests/lean/run/overAndPartialAppsAtWF.lean b/tests/lean/run/overAndPartialAppsAtWF.lean
index c757f5ae77..6ff6a3269a 100644
--- a/tests/lean/run/overAndPartialAppsAtWF.lean
+++ b/tests/lean/run/overAndPartialAppsAtWF.lean
@@ -10,14 +10,13 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
   · have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
     subst heq
     exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
-termination_by _ => a.size - i
+termination_by _ _ _ => a.size - i
 
 @[simp] def f (x y : Nat) : Nat → Nat :=
   if h : x > 0 then
     fun z => f (x - 1) (y + 1) z + 1
   else
     (· + y)
-termination_by
-  f x y => x
+termination_by x
 
 #check f._eq_1
diff --git a/tests/lean/run/psumAtWF.lean b/tests/lean/run/psumAtWF.lean
index 398b1f03e3..bb66c87252 100644
--- a/tests/lean/run/psumAtWF.lean
+++ b/tests/lean/run/psumAtWF.lean
@@ -4,13 +4,12 @@ def fn (f : α → α) (a : α) (n : Nat) : α :=
   match n with
   | 0 => a
   | n+1 => gn f (f (f a)) (f a) n
+termination_by n
 
 def gn (f : α → α) (a b : α) (n : Nat) : α :=
   match n with
   | 0 => b
   | n+1 => fn f (f b) n
+termination_by n
 
 end
-termination_by
-  fn n => n
-  gn n => n
diff --git a/tests/lean/run/renameFixedPrefix.lean b/tests/lean/run/renameFixedPrefix.lean
deleted file mode 100644
index 6862e6c006..0000000000
--- a/tests/lean/run/renameFixedPrefix.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-def f (as : Array Nat) (hsz : as.size > 0) (i : Nat) : Nat :=
-  if h : i < as.size then
-    as.get ⟨i, h⟩ + f as hsz (i + 1)
-  else
-    0
-termination_by f a h i => a.size - i
diff --git a/tests/lean/run/robinson.lean b/tests/lean/run/robinson.lean
index 8ccc15fb45..2327bbc088 100644
--- a/tests/lean/run/robinson.lean
+++ b/tests/lean/run/robinson.lean
@@ -41,11 +41,10 @@ def robinson (u v : Term) : { f : Option Subst // P f u v } := match u, v with
   | .Var i, .Var j =>
     if i = j then ⟨ some id, sorry ⟩
     else ⟨ some λ n => if n = i then j else n, sorry ⟩
-termination_by _ u v => (u, v)
+termination_by (u, v)
 decreasing_by
-  first
-    | apply decr_left _ _ _ _
-    | apply decr_right _ _ _ _ _
+  · apply decr_left _ _ _ _
+  · apply decr_right _ _ _ _ _
 
 attribute [simp] robinson
 
diff --git a/tests/lean/run/simproc_timeout.lean b/tests/lean/run/simproc_timeout.lean
index 27f9d39c81..25277dd997 100644
--- a/tests/lean/run/simproc_timeout.lean
+++ b/tests/lean/run/simproc_timeout.lean
@@ -15,7 +15,7 @@ where
       iter n next
     else
       guess
-termination_by iter guess => guess
+  termination_by guess
 
 end Std.Data.Nat.Basic
 
diff --git a/tests/lean/run/splitIssue.lean b/tests/lean/run/splitIssue.lean
index dcae8155e5..d44e90fab6 100644
--- a/tests/lean/run/splitIssue.lean
+++ b/tests/lean/run/splitIssue.lean
@@ -14,8 +14,9 @@ def len : List α → Nat
   | l =>
     match splitList l with
     | ListSplit.split fst snd => len fst + len snd
-termination_by _ l => l.length
+termination_by l => l.length
 decreasing_by
+  all_goals
   simp [measure, id, invImage, InvImage, Nat.lt_wfRel, WellFoundedRelation.rel, sizeOf] <;>
   first
     | apply Nat.lt_add_right
diff --git a/tests/lean/run/splitList.lean b/tests/lean/run/splitList.lean
index 23fd5353ce..239a791671 100644
--- a/tests/lean/run/splitList.lean
+++ b/tests/lean/run/splitList.lean
@@ -32,7 +32,7 @@ def len : List α → Nat
       have dec₁ : fst.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
       have dec₂ : snd.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
       len fst + len snd
-termination_by _ xs => xs.length
+termination_by xs => xs.length
 
 theorem len_nil : len ([] : List α) = 0 := by
  simp [len]
@@ -76,12 +76,13 @@ def len : List α → Nat
     match h₂ : l, h₃ : splitList l with
     | _, ListSplit.split fst snd =>
       len fst + len snd
-termination_by _ xs => xs.length
+termination_by xs => xs.length
 decreasing_by
-  simp_wf
-  have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
-  subst h₂
-  simp_arith [eq_of_heq h₃] at this |- ; simp [this]
+  all_goals
+    simp_wf
+    have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
+    subst h₂
+    simp_arith [eq_of_heq h₃] at this |- ; simp [this]
 
 theorem len_nil : len ([] : List α) = 0 := by
   simp [len]
diff --git a/tests/lean/run/unfoldr.lean b/tests/lean/run/unfoldr.lean
index ef252f84eb..9e57791d0d 100644
--- a/tests/lean/run/unfoldr.lean
+++ b/tests/lean/run/unfoldr.lean
@@ -27,7 +27,7 @@ def List.unfoldr' {α β : Type u} [w : WellFoundedRelation β] (f : (b : β) 
   match f b with
   | none => []
   | some (a, ⟨b', h⟩) => a :: unfoldr' f b'
-termination_by unfoldr' b => b
+termination_by b
 
 -- We need the `master` branch to test the following example
 
diff --git a/tests/lean/run/wfEqns1.lean b/tests/lean/run/wfEqns1.lean
index 8daaab858e..4c61043f1a 100644
--- a/tests/lean/run/wfEqns1.lean
+++ b/tests/lean/run/wfEqns1.lean
@@ -9,13 +9,17 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
+
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
 end
-decreasing_by
-  simp [measure, invImage, InvImage, Nat.lt_wfRel]
-  apply Nat.lt_succ_self
 
 #print isEven
 
diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean
index 8d8ead2069..aaf8670cb3 100644
--- a/tests/lean/run/wfEqns2.lean
+++ b/tests/lean/run/wfEqns2.lean
@@ -11,21 +11,24 @@ def g (i j : Nat) : Nat :=
   match j with
   | Nat.zero => 1
   | Nat.succ j => h i j
+termination_by (i + j, 0)
+decreasing_by
+  simp_wf
+  · apply Prod.Lex.left
+    apply Nat.lt_succ_self
+
 def h (i j : Nat) : Nat :=
   match j with
   | 0 => g i 0
   | Nat.succ j => g i j
-end
-termination_by
-  g i j => (i + j, 0)
-  h i j => (i + j, 1)
+termination_by (i + j, 1)
 decreasing_by
-  simp_wf
-  first
-  | apply Prod.Lex.left
-    apply Nat.lt_succ_self
-  | apply Prod.Lex.right
+  all_goals simp_wf
+  · apply Prod.Lex.right
     decide
+  · apply Prod.Lex.left
+    apply Nat.lt_succ_self
+end
 
 #eval tst ``g
 #check g._eq_1
diff --git a/tests/lean/run/wfEqns4.lean b/tests/lean/run/wfEqns4.lean
index 865f0ed7e2..d6549693aa 100644
--- a/tests/lean/run/wfEqns4.lean
+++ b/tests/lean/run/wfEqns4.lean
@@ -9,26 +9,30 @@ mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n, a, b => g a n b |>.1
+  termination_by n _ _ => (n, 2)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.right
+    decide
 
   def g : α → Nat → α → (α × α)
     | a, 0, b => (a, b)
     | a, n, b => (h a b n, a)
+  termination_by _ n _ => (n, 1)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.right
+    decide
 
   def h : α → α → Nat → α
     | a, b, 0 => b
     | a, b, n+1 => f n a b
-end
-termination_by
-  f n _ _ => (n, 2)
-  g _ n _ => (n, 1)
-  h _ _ n => (n, 0)
-decreasing_by
-  simp_wf
-  first
-  | apply Prod.Lex.left
+  termination_by _ _ n => (n, 0)
+  decreasing_by
+    simp_wf
+    apply Prod.Lex.left
     apply Nat.lt_succ_self
-  | apply Prod.Lex.right
-    decide
+end
 
 #eval f 5 'a' 'b'
 
diff --git a/tests/lean/run/wfEqnsIssue.lean b/tests/lean/run/wfEqnsIssue.lean
index 1f81042bec..14ede871e8 100644
--- a/tests/lean/run/wfEqnsIssue.lean
+++ b/tests/lean/run/wfEqnsIssue.lean
@@ -84,4 +84,4 @@ def Stmt.mapCtx (f : HList Γ' → HList Γ) : Stmt m ω Γ Δ b c β → Stmt m
   | sfor e body => sfor (e ∘ f) (body.mapCtx (fun | HList.cons a as => HList.cons a (f as)))
   | sbreak => sbreak
   | scont => scont
-termination_by mapCtx _ s => sizeOf s
+termination_by s => sizeOf s
diff --git a/tests/lean/run/wfLean3Issue.lean b/tests/lean/run/wfLean3Issue.lean
index f65609d9b7..3a41bb8cb3 100644
--- a/tests/lean/run/wfLean3Issue.lean
+++ b/tests/lean/run/wfLean3Issue.lean
@@ -3,4 +3,4 @@ def foo : Nat → Nat → Nat
   | s+1, 0   => foo s 0 + 1
   | 0,   b+1 => foo 0 b + 1
   | s+1, b+1 => foo (s+1) b + foo s (b+1)
-termination_by foo b s => (b, s)
+termination_by b s => (b, s)
diff --git a/tests/lean/run/wfOverapplicationIssue.lean b/tests/lean/run/wfOverapplicationIssue.lean
index 69687ee0f6..0636801242 100644
--- a/tests/lean/run/wfOverapplicationIssue.lean
+++ b/tests/lean/run/wfOverapplicationIssue.lean
@@ -8,5 +8,5 @@ theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h
       next he => subst a; apply sizeOf_get_lt
       next => have ih := aux (j+1) h; assumption
     · contradiction
+    termination_by as.size - j
   apply aux 0 h
-termination_by aux j => as.size - j
diff --git a/tests/lean/run/wfSum.lean b/tests/lean/run/wfSum.lean
index 764195fb12..db36df9519 100644
--- a/tests/lean/run/wfSum.lean
+++ b/tests/lean/run/wfSum.lean
@@ -6,4 +6,4 @@ where
       go (i+1) (s + as.get ⟨i, h⟩)
     else
       s
-termination_by _ i s => as.size - i
+  termination_by as.size - i
diff --git a/tests/lean/substBadMotive.lean b/tests/lean/substBadMotive.lean
index 11c69899dc..ccdbe2c3a3 100644
--- a/tests/lean/substBadMotive.lean
+++ b/tests/lean/substBadMotive.lean
@@ -13,7 +13,7 @@ namespace Ex3
 def heapifyDown (a : Array α) (i : Fin a.size) : Array α :=
   have : i < i := sorry
   heapifyDown a ⟨i.1, a.size_swap i i ▸ i.2⟩ -- Error, failed to compute motive, `subst` is not applicable here
-termination_by _ i => i.1
+termination_by i.1
 decreasing_by assumption
 end Ex3
 
@@ -34,6 +34,6 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) : Arra
     heapifyDown lt a' ⟨j.1.1, a.size_swap i j ▸ j.1.2⟩ -- Error, failed to compute motive, `subst` is not applicable here
   else
     a
-termination_by _ a i => a.size - i.1
+termination_by a.size - i.1
 decreasing_by assumption
 end Ex4
diff --git a/tests/lean/termination_by.lean b/tests/lean/termination_by.lean
index 7e5ec0adca..455088cd55 100644
--- a/tests/lean/termination_by.lean
+++ b/tests/lean/termination_by.lean
@@ -1,105 +1,85 @@
-mutual
-  inductive Even : Nat → Prop
-    | base : Even 0
-    | step : Odd n → Even (n+1)
-  inductive Odd : Nat → Prop
-    | step : Even n → Odd (n+1)
-end
-termination_by _ n => n -- Error
+/-!
+This module tests various mis-uses of termination_by and decreasing_by:
+* use in non-recursive functions
+* that all or none of a recursive group have termination_by.
+-/
+
+def nonRecursive1 (n : Nat) : Nat := n
+  termination_by n -- Error
+
+def nonRecursive2 (n : Nat) : Nat := n
+  decreasing_by sorry -- Error
+
+def nonRecursive3 (n : Nat) : Nat := n
+  termination_by n -- Error
+  decreasing_by sorry
+
+partial def partial1 (n : Nat) : Nat := partial1 n
+  termination_by n -- Error
+
+partial def partial2 (n : Nat) : Nat := partial2 n
+  decreasing_by sorry -- Error
+
+partial def partial3 (n : Nat) : Nat := partial3 n
+  termination_by n -- Error
+  decreasing_by sorry
+
+unsafe def unsafe1 (n : Nat) : Nat := unsafe1 n
+termination_by n -- Error
+
+unsafe def unsafe2 (n : Nat) : Nat := unsafe2 n
+  decreasing_by sorry -- Error
+
+unsafe def unsafe3 (n : Nat) : Nat := unsafe3 n
+  termination_by x -- Error
+  decreasing_by sorry
+
+unsafe def withWhere (n : Nat) : Nat := foo n
+  where foo (n : Nat) := n
+    termination_by n -- Error
+
+unsafe def withLetRec (n : Nat) : Nat :=
+  let rec foo (n : Nat) := n
+    termination_by n -- Error
+  foo n
 
 mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
- termination_by _ => n -- Error
+  def rec : Nat → Nat
+    | 0 => 0
+    | n+1 => rec n + notrec n
+  termination_by x => x
+
+  def notrec (n : Nat) : Nat := n
+  termination_by n -- Error
 end
 
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
-end
-termination_by n => n -- Error
-
-
-def g' (n : Nat) :=
-  match n with
-  | 0 => 1
-  | n+1 => g' n * 3
-termination_by
-  h' n => n -- Error
-
-def g' (n : Nat) :=
-  match n with
-  | 0 => 1
-  | n+1 => g' n * 3
-termination_by
-  g' n => n
-  _ n => n -- Error
 
 mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
-  def isOdd : Nat → Bool
+  termination_by x => x
+
+  def isOdd : Nat → Bool -- Error
     | 0 => false
     | n+1 => isEven n
 end
-termination_by
-   isEven x => x -- Error
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x
-   isOd x => x -- Error
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x
-   isEven y => y -- Error
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x
-   _ x => x
-   _ x => x + 1 -- Error
-
 
 namespace Test
 mutual
   def f : Nat → α → α → α
     | 0, a, b => a
     | n+1, a, b => g n a b |>.1
+  termination_by n _ _ => n
 
   def g : Nat → α → α → (α × α)
     | 0, a, b => (a, b)
     | n+1, a, b => (h n a b, a)
+  termination_by n _ _ => n
 
-  def h : Nat → α → α → α
+  def h : Nat → α → α → α -- Error
     | 0, a, b => b
     | n+1, a, b => f n a b
 end
-termination_by
-  f n => n -- Error
-  g n => n
 
 end Test
diff --git a/tests/lean/termination_by.lean.expected.out b/tests/lean/termination_by.lean.expected.out
index 6374b804ce..994524847d 100644
--- a/tests/lean/termination_by.lean.expected.out
+++ b/tests/lean/termination_by.lean.expected.out
@@ -1,10 +1,14 @@
-termination_by.lean:8:0-8:23: error: invalid 'termination_by' in mutually inductive datatype declaration
-termination_by.lean:13:1-13:22: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
-termination_by.lean:20:15-20:21: error: function 'n' not found in current declaration
-termination_by.lean:28:2-28:11: error: function 'h'' not found in current declaration
-termination_by.lean:36:2-36:10: error: invalid `termination_by` syntax, unnecessary else-case
-termination_by.lean:47:3-47:16: error: invalid `termination_by` syntax, missing case for function 'isOdd'
-termination_by.lean:59:3-59:14: error: function 'isOd' not found in current declaration
-termination_by.lean:71:3-71:16: error: invalid `termination_by` syntax, `isEven` case has already been provided
-termination_by.lean:84:3-84:15: error: invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified
-termination_by.lean:102:2-102:10: error: invalid `termination_by` syntax, missing case for function 'Test.h'
+termination_by.lean:8:2-8:18: error: unused `termination_by`, function is not recursive
+termination_by.lean:11:2-11:21: error: unused `decreasing_by`, function is not recursive
+termination_by.lean:14:2-15:21: error: unused termination hints, function is not recursive
+termination_by.lean:18:2-18:18: error: unused `termination_by`, function is partial
+termination_by.lean:21:2-21:21: error: unused `decreasing_by`, function is partial
+termination_by.lean:24:2-25:21: error: unused termination hints, function is partial
+termination_by.lean:28:0-28:16: error: unused `termination_by`, function is unsafe
+termination_by.lean:31:2-31:21: error: unused `decreasing_by`, function is unsafe
+termination_by.lean:34:2-35:21: error: unused termination hints, function is unsafe
+termination_by.lean:39:4-39:20: error: unused `termination_by`, function is not recursive
+termination_by.lean:43:4-43:20: error: unused `termination_by`, function is not recursive
+termination_by.lean:53:2-53:18: error: unused `termination_by`, function is not recursive
+termination_by.lean:63:6-63:11: error: Missing `termination_by`; this function is mutually recursive with isEven, which has a `termination_by` clause.
+termination_by.lean:80:6-80:7: error: Missing `termination_by`; this function is mutually recursive with Test.f, which has a `termination_by` clause.
diff --git a/tests/lean/termination_by_vars.lean b/tests/lean/termination_by_vars.lean
new file mode 100644
index 0000000000..7437b972e1
--- /dev/null
+++ b/tests/lean/termination_by_vars.lean
@@ -0,0 +1,119 @@
+/-!
+Here we test that lean correctly complains if `termination_by` has too many variables,
+and that it does the right thing if it has fewer variables.
+-/
+
+opaque dec1 : Nat → Nat
+axiom dec1_lt (n : Nat) : dec1 n < n
+opaque dec2 : Nat → Nat
+axiom dec2_lt (n : Nat) : dec2 n < n
+
+namespace Basic
+
+def tooManyVars (n : Nat) : Nat := tooManyVars (dec1 n)
+  termination_by x => x -- Error
+  decreasing_by apply dec1_lt
+
+def okVariables1 (n : Nat) : Nat := okVariables1 (dec1 n)
+  termination_by n
+  decreasing_by apply dec1_lt
+
+
+def blankArrow (n : Nat) : Nat := blankArrow (dec1 n)
+  termination_by => x -- Error
+  decreasing_by apply dec1_lt
+
+def fewerVariables1 (n : Nat) : Nat → Nat → Nat := fun a b => fewerVariables1 (dec2 n) a (dec1 b)
+  termination_by n -- Not an error
+  decreasing_by apply dec2_lt
+
+def fewerVariables2 (n : Nat) : Nat → Nat → Nat := fun a b => fewerVariables2 n (dec1 a) (dec2 b)
+  termination_by a => a
+  decreasing_by apply dec1_lt -- NB: dec2_lt would no work
+
+def okVariables2 (n : Nat) : Nat → Nat → Nat := fun a b => okVariables2 n (dec1 a) (dec2 b)
+  termination_by a b => b
+  decreasing_by apply dec2_lt
+
+def tooManyVariables2 (n : Nat) : Nat → Nat → Nat := fun a b => tooManyVariables2 n (dec1 a) (dec2 b)
+  termination_by a b c => b
+  decreasing_by apply dec1_lt
+
+end Basic
+
+namespace WithVariable
+
+variable (v : Nat)
+
+def tooManyVars (n : Nat) : Nat := tooManyVars (dec1 n) + v
+  termination_by x => x -- Error
+  decreasing_by apply dec1_lt
+
+def okVariables1 (n : Nat) : Nat := okVariables1 (dec1 n) + v
+  termination_by n
+  decreasing_by apply dec1_lt
+
+
+def blankArrow (n : Nat) : Nat := blankArrow (dec1 n) + v
+  termination_by => x -- Error
+  decreasing_by apply dec1_lt
+
+def fewerVariables1 (n : Nat) : Nat → Nat → Nat := fun a b =>
+    fewerVariables1 (dec2 n) a (dec1 b) + v
+  termination_by n
+  decreasing_by apply dec2_lt
+
+def fewerVariables2 (n : Nat) : Nat → Nat → Nat := fun a b =>
+    fewerVariables2 n (dec1 a) (dec2 b) + v
+  termination_by a => a
+  decreasing_by apply dec1_lt
+
+def okVariables2 (n : Nat) : Nat → Nat → Nat := fun a b =>
+    okVariables2 n a (dec1 b) + v
+  termination_by a b => b
+  decreasing_by apply dec1_lt
+
+end WithVariable
+
+namespace InLetRec
+
+def foo1 (v : Nat) := 5
+  where
+  tooManyVars (n : Nat) : Nat := tooManyVars (dec1 n) + v
+    termination_by x => x -- Error
+    decreasing_by apply dec1_lt
+
+def foo2 (v : Nat) := 5
+  where
+  okVariables1 (n : Nat) : Nat := okVariables1 (dec1 n) + v
+    termination_by n
+    decreasing_by apply dec1_lt
+
+def foo3 (v : Nat) := 5
+  where
+  blankArrow (n : Nat) : Nat := blankArrow (dec1 n) + v
+    termination_by => x -- Error
+    decreasing_by apply dec1_lt
+
+def foo4 (v : Nat) := 5
+  where
+  fewerVariables1 (n : Nat) : Nat → Nat → Nat := fun a b =>
+      fewerVariables1 (dec2 n) a (dec1 b) + v
+    termination_by n
+    decreasing_by apply dec2_lt
+
+def foo5 (v : Nat) := 5
+  where
+  fewerVariables2 (n : Nat) : Nat → Nat → Nat := fun a b =>
+      fewerVariables2 n (dec1 a) (dec2 b) + v
+    termination_by a => a
+    decreasing_by apply dec1_lt
+
+def foo6 (v : Nat) := 5
+  where
+  okVariables2 (n : Nat) : Nat → Nat → Nat := fun a b =>
+      okVariables2 n a (dec1 b) + v
+    termination_by a b => b
+    decreasing_by apply dec1_lt
+
+end InLetRec
diff --git a/tests/lean/termination_by_vars.lean.expected.out b/tests/lean/termination_by_vars.lean.expected.out
new file mode 100644
index 0000000000..96ed29e651
--- /dev/null
+++ b/tests/lean/termination_by_vars.lean.expected.out
@@ -0,0 +1,7 @@
+termination_by_vars.lean:14:2-14:23: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
+termination_by_vars.lean:23:2-23:21: error: no extra parameters bounds, please omit the `=>`
+termination_by_vars.lean:39:2-39:27: error: Too many extra parameters bound; the function definition only has 2 extra parameters.
+termination_by_vars.lean:49:2-49:23: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
+termination_by_vars.lean:58:2-58:21: error: no extra parameters bounds, please omit the `=>`
+termination_by_vars.lean:83:4-83:25: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
+termination_by_vars.lean:95:4-95:23: error: no extra parameters bounds, please omit the `=>`
diff --git a/tests/lean/termination_by_where.lean b/tests/lean/termination_by_where.lean
new file mode 100644
index 0000000000..5567e152a7
--- /dev/null
+++ b/tests/lean/termination_by_where.lean
@@ -0,0 +1,16 @@
+/-!
+This module systematically tests the relative placement of `decreasing_by` and `where`.
+-/
+
+-- For concise recursive definition that need well-founded recursion
+-- and `decreasing_by` tactics that would fail if run on the wrong function
+opaque dec1 : Nat → Nat
+axiom dec1_lt (n : Nat) : dec1 n < n
+opaque dec2 : Nat → Nat
+axiom dec2_lt (n : Nat) : dec2 n < n
+
+def foo (n : Nat) := foo (dec1 n) + bar n
+decreasing_by apply dec1_lt
+where
+bar (m : Nat) : Nat := bar (dec2 m)
+decreasing_by apply dec2_lt
diff --git a/tests/lean/termination_by_where.lean.expected.out b/tests/lean/termination_by_where.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tests/lean/treeMap.lean b/tests/lean/treeMap.lean
index 5dce56f8ef..c18f36b4c8 100644
--- a/tests/lean/treeMap.lean
+++ b/tests/lean/treeMap.lean
@@ -6,4 +6,4 @@ open TreeNode in def treeToList (t : TreeNode) : List String :=
  match t with
  | mkLeaf name => [name]
  | mkNode name children => name :: List.join (children.map treeToList)
-termination_by _ t => t
+termination_by t
diff --git a/tests/lean/unfold1.lean b/tests/lean/unfold1.lean
index d153f3c6f0..d13a64c7e5 100644
--- a/tests/lean/unfold1.lean
+++ b/tests/lean/unfold1.lean
@@ -2,11 +2,12 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  decreasing_by apply Nat.lt_succ_self
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  decreasing_by apply Nat.lt_succ_self
 end
-decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with
diff --git a/tests/lean/wf2.lean b/tests/lean/wf2.lean
index fee98b464d..19b909d76c 100644
--- a/tests/lean/wf2.lean
+++ b/tests/lean/wf2.lean
@@ -3,4 +3,4 @@ def g (x : Nat) (y : Nat) : Nat :=
     2 * g (x-1) y -- Error here
   else
     0
-termination_by g x y => x
+termination_by x