From f6f6eddb86b1e58d7401b7985cd7afc049c368b5 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 6 Dec 2023 10:36:27 +0100
Subject: [PATCH] feat: drop support for termination_by'
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

until around 7fe6881 the way to define well-founded recursions was to
specify a `WellFoundedRelation` on the argument explicitly. This was
rather low-level, for example one had to predict the packing of multiple
arguments into `PProd`s, the packing of mutual functions into `PSum`s,
and the cliques that were calculated.

Then the current `termination_by` syntax was introduced, where you
sepecify the termination argument at a higher level (one clause per
functions, unpacked arguments), and the `WellFoundedRelation` is found
using type class resolution.

The old syntax was kept around as `termination_by'`. But at the time of
writing, this is not used anywhere in the lean, std, mathlib or the
theroem-proving-in-lean repositories. Also, should be possible to
express anything that the old syntax supported also with the new one,
possibly requiring a helper type with a suitable instance, or a very
generic wrapper like

```
inductive WithWFRel {a : Type _} {rel : a → a → Prop} (h : WellFounded rel) where
  | mk : a -> WithWFRel h

instance : WellFoundedRelation (WithWFRel  h) := invImage (fun x => match x with | .mk x => x) ⟨_, h⟩
```

Since the old syntax is unused, has an unhelpful name and relies on
internals, this removes the support. Now is a good time before the
refactoring that's planned in #2921.

The test suite was updated without particular surprises.

The parametric `terminationHint` parser is gone, which means we can
match on syntax more easily now, in `expandDecreasingBy?`.
---
 src/Lean/Elab/PreDefinition/Main.lean         |   4 +-
 src/Lean/Elab/PreDefinition/WF/GuessLex.lean  |   3 +-
 src/Lean/Elab/PreDefinition/WF/Rel.lean       |  41 ++---
 .../PreDefinition/WF/TerminationHint.lean     | 161 ++++++++----------
 src/Lean/Parser/Command.lean                  |  25 ++-
 tests/lean/906.lean                           |   2 +-
 tests/lean/letRecMissingAnnotation.lean       |   2 +-
 tests/lean/mutwf1.lean                        |  10 +-
 tests/lean/mutwf1.lean.expected.out           |   4 +-
 tests/lean/run/860.lean                       |   3 +-
 tests/lean/run/955.lean                       |  13 --
 tests/lean/run/eqnsAtSimp.lean                |   3 -
 tests/lean/run/eqnsAtSimp2.lean               |   4 -
 tests/lean/run/mutwf1.lean                    |  31 +---
 tests/lean/run/mutwf2.lean                    |  17 +-
 tests/lean/run/mutwf3.lean                    |  43 +++--
 tests/lean/run/nestedIssueMatch.lean          |   1 -
 tests/lean/run/nestedWF.lean                  |   1 -
 tests/lean/run/robinson.lean                  |   4 +-
 tests/lean/run/wfEqns1.lean                   |   3 -
 tests/lean/run/wfEqns2.lean                   |   9 +-
 tests/lean/run/wfEqns3.lean                   |   1 -
 tests/lean/run/wfEqns4.lean                   |  11 +-
 tests/lean/run/wfSum.lean                     |   2 +-
 tests/lean/run/wfrecUnary.lean                |   1 -
 tests/lean/substBadMotive.lean                |   4 +-
 tests/lean/termination_by.lean                |  78 ++++++++-
 tests/lean/termination_by.lean.expected.out   |  12 +-
 tests/lean/termination_by2.lean               |  68 --------
 tests/lean/termination_by2.lean.expected.out  |   7 -
 tests/lean/unfold1.lean                       |   1 -
 tests/lean/wf2.lean                           |   2 +-
 tests/lean/wfrecUnusedLet.lean                |   1 -
 tests/lean/wfrecUnusedLet.lean.expected.out   |   2 +-
 34 files changed, 231 insertions(+), 343 deletions(-)
 delete mode 100644 tests/lean/termination_by2.lean
 delete mode 100644 tests/lean/termination_by2.lean.expected.out

diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 0e458ae908ce..bc89dc993f07 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -100,8 +100,8 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
   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.expandTerminationHint hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
+  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)}"
diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index a74030a72417..73e732f4030f 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -31,7 +31,6 @@ In addition to measures derived from `sizeOf xᵢ`, it also considers measures
 that assign an order to the functions themselves. This way we can support mutual
 function definitions where no arguments decrease from one function to another.
 
-
 The result of this module is a `TerminationWF`, which is then passed on to `wfRecursion`; this
 design is crucial so that whatever we infer in this module could also be written manually by the
 user. It would be bad if there are function definitions that can only be processed with the
@@ -549,7 +548,7 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
         declName, vars, body,
         implicit := true
       }
-  return .ext termByElements
+  return termByElements
 
 end Lean.Elab.WF.GuessLex
 
diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 6ca0bd16ea51..3b21f175ed54 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -34,10 +34,10 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
     let mut varNames ← xs.mapM fun x => x.fvarId!.getUserName
     if element.vars.size > varNames.size then
       throwErrorAt element.vars[varNames.size]! "too many variable names"
-    for i in [:element.vars.size] do
-      let varStx := element.vars[i]!
-      if varStx.isIdent then
-        varNames := varNames.set! (varNames.size - element.vars.size + i) varStx.getId
+    for h : i in [:element.vars.size] do
+      let varStx := element.vars[i]'h.2
+      if let `($ident:ident) := varStx then
+        varNames := varNames.set! (varNames.size - element.vars.size + i) ident.getId
     return varNames
   let mut mvarId := mvarId
   for localDecl in (← Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
@@ -60,25 +60,18 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPre
   let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
   trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
   withDeclName unaryPreDefName do
-  match wf with
-  | TerminationWF.core wfStx =>
-      let wfRel ← instantiateMVars (← withSynthesize <| elabTermEnsuringType wfStx expectedType)
-      let pendingMVarIds ← getMVars wfRel
-      discard <| logUnassignedUsingErrorInfos pendingMVarIds
-      k wfRel
-  | TerminationWF.ext elements =>
-    withRef (getRefFromElems elements) do
-      let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
-      let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
-      let (d, fMVarId) ← fMVarId.intro1
-      let subgoals ← unpackMutual preDefs fMVarId d
-      for (d, mvarId) in subgoals, element in elements, preDef in preDefs do
-        let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
-        mvarId.withContext do
-          let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
-          mvarId.assign value
-      let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
-      wfRelMVarId.assign wfRelVal
-      k (← instantiateMVars (mkMVar mainMVarId))
+  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
+      mvarId.withContext do
+        let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
+        mvarId.assign value
+    let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
+    wfRelMVarId.assign wfRelVal
+    k (← instantiateMVars (mkMVar mainMVarId))
 
 end Lean.Elab.WF
diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
index 1a41536a4b2a..acd541df3fb0 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
@@ -5,44 +5,46 @@ Authors: Leonardo de Moura
 -/
 import Lean.Parser.Command
 
+set_option autoImplicit false
+
 namespace Lean.Elab.WF
 
-/-! # Support for `decreasing_by` and `termination_by'` notations -/
+/-! # Support for `decreasing_by` -/
 
-structure TerminationHintValue where
+structure DecreasingByTactic where
   ref   : Syntax
-  value : Syntax
+  value : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
   deriving Inhabited
 
-inductive TerminationHint where
+inductive DecreasingBy where
   | none
-  | one (val : TerminationHintValue)
-  | many (map : NameMap TerminationHintValue)
+  | one (val : DecreasingByTactic)
+  | many (map : NameMap DecreasingByTactic)
   deriving Inhabited
 
 open Parser.Command in
 /--
-This function takes a user-specified `decreasing_by` or `termination_by'` clause (as `Sytnax`).
-If it is a `terminathionHintMany` (a set of clauses guarded by the function name) then
+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 expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationHint := do
-  let some terminationHint := terminationHint? | return TerminationHint.none
-  let ref := terminationHint
-  match terminationHint with
-  | `(terminationByCore|termination_by' $hint1:terminationHint1)
-  | `(decreasingBy|decreasing_by $hint1:terminationHint1) =>
-    return TerminationHint.one { ref, value := hint1.raw[0] }
-  | `(terminationByCore|termination_by' $hints:terminationHintMany)
-  | `(decreasingBy|decreasing_by $hints:terminationHintMany) => do
-    let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg =>
+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 arg[0].getId.isSuffixOf declName then some declName else none
+        if declId.getId.isSuffixOf declName then some declName else none
       match declName? with
-      | none => Macro.throwErrorAt arg[0] s!"function '{arg[0].getId}' not found in current declaration"
-      | some declName => return m.insert declName { ref := arg, value := arg[2] }
+      | 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
@@ -50,69 +52,65 @@ def expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (A
           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 TerminationHint.many m
+    return DecreasingBy.many m
   | _ => Macro.throwUnsupported
 
-def TerminationHint.markAsUsed (t : TerminationHint) (clique : Array Name) : TerminationHint :=
+def DecreasingBy.markAsUsed (t : DecreasingBy) (clique : Array Name) : DecreasingBy :=
   match t with
-  | TerminationHint.none   => TerminationHint.none
-  | TerminationHint.one .. => TerminationHint.none
-  | TerminationHint.many m => Id.run do
+  | 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 TerminationHint.none
+          return DecreasingBy.none
         else
-          return TerminationHint.many m
+          return DecreasingBy.many m
     return t
 
-def TerminationHint.find? (t : TerminationHint) (clique : Array Name) : Option TerminationHintValue :=
+def DecreasingBy.find? (t : DecreasingBy) (clique : Array Name) : Option DecreasingByTactic :=
   match t with
-  | TerminationHint.none   => Option.none
-  | TerminationHint.one v  => some v
-  | TerminationHint.many m => clique.findSome? m.find?
+  | DecreasingBy.none   => Option.none
+  | DecreasingBy.one v  => some v
+  | DecreasingBy.many m => clique.findSome? m.find?
 
-def TerminationHint.ensureAllUsed (t : TerminationHint) : MacroM Unit := do
+def DecreasingBy.ensureAllUsed (t : DecreasingBy) : MacroM Unit := do
   match t with
-  | TerminationHint.one v   => Macro.throwErrorAt v.ref "unused termination hint element"
-  | TerminationHint.many m  => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
+  | 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` and `termination_by'` notation -/
+/-! # Support for `termination_by` notation -/
 
 /-- A single `termination_by` clause -/
 structure TerminationByElement where
   ref       : Syntax
   declName  : Name
-  vars      : Array Syntax
-  body      : Syntax
+  vars      : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
+  body      : Term
   implicit  : Bool
   deriving Inhabited
 
-/-- `terminatoin_by` clauses, grouped by clique -/
+/-- `termination_by` clauses, grouped by clique -/
 structure TerminationByClique where
   elements : Array TerminationByElement
   used     : Bool := false
 
 /--
-A `termination_by'` or `termination_by` hint, as specified by the user
+A `termination_by` hint, as specified by the user
 -/
-inductive TerminationBy where
-  /-- `termination_by'` -/
-  | core (hint : TerminationHint)
-  /-- `termination_by` -/
-  | ext  (cliques : Array TerminationByClique)
+structure TerminationBy where
+  cliques : Array TerminationByClique
   deriving Inhabited
 
 /--
-A `termination_by'` or `termination_by` hint, as applicable to a single clique
+A `termination_by` hint, as applicable to a single clique
 -/
-inductive TerminationWF where
-  | core (stx : Syntax)
-  | ext  (clique : Array TerminationByElement)
+abbrev TerminationWF := Array TerminationByElement
 
-/-
+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
@@ -125,8 +123,9 @@ def terminationByElement   := leading_parser ppLine >> (ident <|> hole) >> many
 def terminationBy          := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement
 ```
 -/
-open Parser.Command in
-private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy := do
+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
@@ -170,40 +169,21 @@ private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array N
       result := result.push { elements }
   if !usedElse && elseElemStx?.isSome then
     withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case"
-  return TerminationBy.ext result
-
-/--
-Expands the syntax for a `termination_by` or `termination_by'` clause, using the appropriate function
--/
-def expandTerminationBy (hint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy :=
-  if let some hint := hint? then
-    if hint.isOfKind ``Parser.Command.terminationByCore then
-      return TerminationBy.core (← expandTerminationHint hint? cliques)
-    else if hint.isOfKind ``Parser.Command.terminationBy then
-      expandTerminationByNonCore hint cliques
-    else
-      Macro.throwUnsupported
-  else
-      return TerminationBy.core TerminationHint.none
+  return ⟨result⟩
 
 def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy :=
-  match t with
-  | core hint   => core (hint.markAsUsed cliqueNames)
-  | ext cliques => ext <| cliques.map fun clique =>
+  .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 :=
-  match t with
-  | core hint => hint.find? cliqueNames |>.map fun v => TerminationWF.core v.value
-  | ext cliques =>
-    cliques.findSome? fun clique =>
-      if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
-        some <| TerminationWF.ext clique.elements
-      else
-        none
+  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
@@ -211,19 +191,16 @@ def TerminationByClique.allImplicit (c : TerminationByClique) : Bool :=
 def TerminationByClique.getExplicitElement? (c : TerminationByClique) : Option TerminationByElement :=
   c.elements.find? (!·.implicit)
 
-def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit :=
-  match t with
-  | core hint => hint.ensureAllUsed
-  | ext cliques => do
-    let hasUsedAllImplicit := cliques.any fun c => c.allImplicit && c.used
-    let mut reportedAllImplicit := true
-    for clique in 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"
+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"
 
 end Lean.Elab.WF
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 3b1c83272dbf..4d2981dd8012 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -28,23 +28,18 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
-/-
-A mutual block may be broken in different cliques,
-we identify them using an `ident` (an element of the clique).
-We provide two kinds of hints to the termination checker:
-1- A wellfounded relation (`p` is `termParser`)
-2- A tactic for proving the recursive applications are "decreasing" (`p` is `tacticSeq`)
+/--
+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 terminationHintMany (p : Parser) := leading_parser
-  atomic (lookahead (ident >> " => ")) >>
-  many1Indent (group (ppLine >> ppIndent (ident >> " => " >> p >> patternIgnore (optional ";"))))
-def terminationHint1 (p : Parser) := leading_parser p
-def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p
+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 terminationByCore := leading_parser
-  ppDedent ppLine >> "termination_by' " >> terminationHint termParser
 def decreasingBy := leading_parser
-  ppDedent ppLine >> "decreasing_by " >> terminationHint Tactic.tacticSeq
+  ppDedent ppLine >> "decreasing_by " >> (decreasingByMany <|> decreasingBy1)
 
 def terminationByElement   := leading_parser
   ppLine >> (ident <|> Term.hole) >> many (ppSpace >> (ident <|> Term.hole)) >>
@@ -53,7 +48,7 @@ def terminationBy          := leading_parser
   ppDedent ppLine >> "termination_by" >> many1Indent terminationByElement
 
 def terminationSuffix :=
-  optional (terminationBy <|> terminationByCore) >> optional decreasingBy
+  optional terminationBy >> optional decreasingBy
 
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
diff --git a/tests/lean/906.lean b/tests/lean/906.lean
index f92ab10552d0..4d8b56670acd 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' measure (fun ⟨n, _⟩ => n)
+termination_by _ n => n
 decreasing_by sorry
 
 set_option maxRecDepth 100  -- default takes ages in debug mode and triggers stack space threshold
diff --git a/tests/lean/letRecMissingAnnotation.lean b/tests/lean/letRecMissingAnnotation.lean
index f9e466efe2bb..8cebbfa38872 100644
--- a/tests/lean/letRecMissingAnnotation.lean
+++ b/tests/lean/letRecMissingAnnotation.lean
@@ -5,4 +5,4 @@ def sum (as : Array Nat) : Nat :=
     else
       s
   go 0 0
-termination_by' measure (fun ⟨i, _⟩ => as.size - i)
+termination_by go i _ => as.size - i
diff --git a/tests/lean/mutwf1.lean b/tests/lean/mutwf1.lean
index 16488d66589e..82b74ff71865 100644
--- a/tests/lean/mutwf1.lean
+++ b/tests/lean/mutwf1.lean
@@ -11,13 +11,9 @@ mutual
     else
       n
 end
-termination_by'
-  invImage
-    (fun
-     | PSum.inl ⟨n, true⟩ => (n, 2)
-     | PSum.inl ⟨n, false⟩ => (n, 1)
-     | PSum.inr n => (n, 0))
-  $ Prod.lex sizeOfWFRel sizeOfWFRel
+termination_by
+  f n b => (n, if b then 2 else 1)
+  g n => (n, 0)
 decreasing_by
   simp_wf
   first
diff --git a/tests/lean/mutwf1.lean.expected.out b/tests/lean/mutwf1.lean.expected.out
index b887ea8a0521..066ec9cf1a0c 100644
--- a/tests/lean/mutwf1.lean.expected.out
+++ b/tests/lean/mutwf1.lean.expected.out
@@ -1,9 +1,9 @@
-mutwf1.lean:28:2-28:6: error: unsolved goals
+mutwf1.lean:24:2-24:6: error: unsolved goals
 case h.a
 n : Nat
 h : n ≠ 0
 ⊢ Nat.sub n 0 ≠ 0
-mutwf1.lean:37:22-37:29: error: failed to prove termination, possible solutions:
+mutwf1.lean:33:22-33:29: error: failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
diff --git a/tests/lean/run/860.lean b/tests/lean/run/860.lean
index 07377b7a5547..106c708b395b 100644
--- a/tests/lean/run/860.lean
+++ b/tests/lean/run/860.lean
@@ -21,8 +21,7 @@ def pack (n: Nat) : List Nat :=
       | true => loop (next n) 0 (List.cons acc accs)
       | false => loop (next n) (acc+1) accs
   loop n 0 []
-termination_by'
-  invImage (fun ⟨n, _, _⟩ => n) Nat.lt_wfRel
+termination_by _ n _ _ => n
 decreasing_by
   simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
   apply pack_loop_terminates
diff --git a/tests/lean/run/955.lean b/tests/lean/run/955.lean
index 07d5711a9c23..16016899c867 100644
--- a/tests/lean/run/955.lean
+++ b/tests/lean/run/955.lean
@@ -11,16 +11,3 @@ termination_by _ n =>
   match n with
   | _ => n
 end Ex2
-
-
-namespace Ex3
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by' measure (fun n => match n with | PSum.inl n => n | PSum.inr n => n)
-end Ex3
diff --git a/tests/lean/run/eqnsAtSimp.lean b/tests/lean/run/eqnsAtSimp.lean
index a296c5f0f778..8a9e97a3dc6f 100644
--- a/tests/lean/run/eqnsAtSimp.lean
+++ b/tests/lean/run/eqnsAtSimp.lean
@@ -6,9 +6,6 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun
-  | PSum.inl n => n
-  | PSum.inr n => n
 decreasing_by
   simp [measure, invImage, InvImage, Nat.lt_wfRel]
   apply Nat.lt_succ_self
diff --git a/tests/lean/run/eqnsAtSimp2.lean b/tests/lean/run/eqnsAtSimp2.lean
index 8d7424a2af75..646f12d499ec 100644
--- a/tests/lean/run/eqnsAtSimp2.lean
+++ b/tests/lean/run/eqnsAtSimp2.lean
@@ -6,9 +6,6 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun
-  | PSum.inl n => n
-  | PSum.inr n => n
 decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
@@ -20,7 +17,6 @@ def f (x : Nat) : Nat :=
   match x with
   | 0 => 1
   | x + 1 => f x * 2
-termination_by' measure id
 decreasing_by apply Nat.lt_succ_self
 
 attribute [simp] f
diff --git a/tests/lean/run/mutwf1.lean b/tests/lean/run/mutwf1.lean
index 6a6f9e9cb7e8..2e75be80be4e 100644
--- a/tests/lean/run/mutwf1.lean
+++ b/tests/lean/run/mutwf1.lean
@@ -12,35 +12,6 @@ mutual
     | a, b, 0 => b
     | a, b, n+1 => f n a b
 end
-termination_by'
-  invImage
-    (fun
-      | PSum.inl ⟨n, _, _⟩ => (n, 2)
-      | PSum.inr <| PSum.inl ⟨_, n, _⟩ => (n, 1)
-      | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
-
-#print f
-#print g
-#print h
-
-#eval f 5 'a' 'b'
-end Ex1
-
-namespace Ex2
-mutual
-  def f : Nat → α → α → α
-    | 0, a, b => a
-    | n, a, b => g a n b |>.1
-
-  def g : α → Nat → α → (α × α)
-    | a, 0, b => (a, b)
-    | a, n, b => (h a b n, a)
-
-  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)
@@ -51,4 +22,4 @@ termination_by
 #print h
 
 #eval f 5 'a' 'b'
-end Ex2
+end Ex1
diff --git a/tests/lean/run/mutwf2.lean b/tests/lean/run/mutwf2.lean
index fa1d4645957b..d0cf4a6555c1 100644
--- a/tests/lean/run/mutwf2.lean
+++ b/tests/lean/run/mutwf2.lean
@@ -7,24 +7,9 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun
-  | PSum.inl n => n
-  | PSum.inr n => n
+termination_by _ n => n
 
 #print isEven
 #print isOdd
 #print isEven._mutual
 end Ex1
-
-
-namespace Ex2
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by _ n => n
-end Ex2
diff --git a/tests/lean/run/mutwf3.lean b/tests/lean/run/mutwf3.lean
index 05af6cdd4f77..596d1cf517a3 100644
--- a/tests/lean/run/mutwf3.lean
+++ b/tests/lean/run/mutwf3.lean
@@ -9,16 +9,13 @@ mutual
     | a, n, b => (h a b n, a)
 
   def h : α → α → Nat → α
-    | a, b, 0 => b
+    | _a, b, 0 => b
     | a, b, n+1 => f n a b
 end
-termination_by'
-  invImage
-    (fun
-      | PSum.inl ⟨n, _, _⟩ => (n, 2)
-      | PSum.inr <| PSum.inl ⟨_, n, _⟩ => (n, 1)
-      | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
+termination_by
+  f n _ _ => (n, 2)
+  g _ n _ => (n, 1)
+  h _ _ n => (n, 0)
 decreasing_by
   simp_wf
   first
@@ -48,14 +45,30 @@ mutual
     | a, b, 0 => b
     | a, b, n+1 => f n a b
 end
-termination_by'
-  invImage
-    (fun
-      | PSum.inl ⟨n, _, _⟩ => (n, 2)
-      | PSum.inr <| PSum.inl ⟨_, n, _⟩ => (n, 1)
-      | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
+termination_by
+  f n _ _ => (n, 2)
+  g _ n _ => (n, 1)
+  h _ _ n => (n, 0)
 
 #print f._unary._mutual
 
 end Ex2
+
+namespace Ex3
+mutual
+  def f : Nat → α → α → α
+    | 0, a, b => a
+    | n, a, b => g a n b |>.1
+
+  def g : α → Nat → α → (α × α)
+    | a, 0, b => (a, b)
+    | a, n, b => (h a b n, a)
+
+  def h : α → α → Nat → α
+    | a, b, 0 => b
+    | a, b, n+1 => f n a b
+end
+
+#print f._unary._mutual
+
+end Ex3
diff --git a/tests/lean/run/nestedIssueMatch.lean b/tests/lean/run/nestedIssueMatch.lean
index 8e945d809830..0e91aaf6ee77 100644
--- a/tests/lean/run/nestedIssueMatch.lean
+++ b/tests/lean/run/nestedIssueMatch.lean
@@ -5,7 +5,6 @@ def g (t : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g n
   | 0 => 0
-termination_by' sorry
 decreasing_by sorry
 
 attribute [simp] g
diff --git a/tests/lean/run/nestedWF.lean b/tests/lean/run/nestedWF.lean
index d0afa3933958..c69d75515321 100644
--- a/tests/lean/run/nestedWF.lean
+++ b/tests/lean/run/nestedWF.lean
@@ -43,7 +43,6 @@ def g (t : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g n
   | 0 => 0
-termination_by' sorry
 decreasing_by sorry
 
 theorem ex1 : g 0 = 0 := by
diff --git a/tests/lean/run/robinson.lean b/tests/lean/run/robinson.lean
index 97230e854fa2..8ccc15fb4522 100644
--- a/tests/lean/run/robinson.lean
+++ b/tests/lean/run/robinson.lean
@@ -18,7 +18,7 @@ abbrev P (c : Option Subst) u v := match c with
   | none => strangers u v
   | some f => act f u = act f v
 
-def rel : WellFoundedRelation (Term × Term) := measure (λ (u, v) => depth u + depth v)
+instance rel : WellFoundedRelation (Term × Term) := measure (λ (u, v) => depth u + depth v)
 
 theorem decr_left (l₁ r₁ l₂ r₂ : Term) :
   rel.rel (l₁, l₂) (Term.Cons l₁ r₁, Term.Cons l₂ r₂) := by
@@ -41,7 +41,7 @@ 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' invImage (λ ⟨ u, v ⟩ => (u, v)) rel
+termination_by _ u v => (u, v)
 decreasing_by
   first
     | apply decr_left _ _ _ _
diff --git a/tests/lean/run/wfEqns1.lean b/tests/lean/run/wfEqns1.lean
index 59c7de89b56e..8daaab858e95 100644
--- a/tests/lean/run/wfEqns1.lean
+++ b/tests/lean/run/wfEqns1.lean
@@ -13,9 +13,6 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun
-  | PSum.inl n => n
-  | PSum.inr n => n
 decreasing_by
   simp [measure, invImage, InvImage, Nat.lt_wfRel]
   apply Nat.lt_succ_self
diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean
index 80228ba9173c..8d8ead206987 100644
--- a/tests/lean/run/wfEqns2.lean
+++ b/tests/lean/run/wfEqns2.lean
@@ -16,12 +16,9 @@ def h (i j : Nat) : Nat :=
   | 0 => g i 0
   | Nat.succ j => g i j
 end
-termination_by'
- invImage
-    (fun
-      | PSum.inl n => (n, 0)
-      | PSum.inr n => (n, 1))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
+termination_by
+  g i j => (i + j, 0)
+  h i j => (i + j, 1)
 decreasing_by
   simp_wf
   first
diff --git a/tests/lean/run/wfEqns3.lean b/tests/lean/run/wfEqns3.lean
index d7c8c36943b5..850766036ead 100644
--- a/tests/lean/run/wfEqns3.lean
+++ b/tests/lean/run/wfEqns3.lean
@@ -10,7 +10,6 @@ def f (x : Nat) : Nat :=
     1
   else
    f (x - 1) * 2
-termination_by' measure id
 decreasing_by
   apply Nat.pred_lt
   exact h
diff --git a/tests/lean/run/wfEqns4.lean b/tests/lean/run/wfEqns4.lean
index 2e42ca81cfb3..865f0ed7e24c 100644
--- a/tests/lean/run/wfEqns4.lean
+++ b/tests/lean/run/wfEqns4.lean
@@ -18,13 +18,10 @@ mutual
     | a, b, 0 => b
     | a, b, n+1 => f n a b
 end
-termination_by'
-  invImage
-    (fun
-      | PSum.inl ⟨n, _, _⟩ => (n, 2)
-      | PSum.inr <| PSum.inl ⟨_, n, _⟩ => (n, 1)
-      | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
+termination_by
+  f n _ _ => (n, 2)
+  g _ n _ => (n, 1)
+  h _ _ n => (n, 0)
 decreasing_by
   simp_wf
   first
diff --git a/tests/lean/run/wfSum.lean b/tests/lean/run/wfSum.lean
index e825eae5640f..764195fb121a 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' measure (fun ⟨i, s⟩ => as.size - i)
+termination_by _ i s => as.size - i
diff --git a/tests/lean/run/wfrecUnary.lean b/tests/lean/run/wfrecUnary.lean
index a6c49a9bbe25..5f7e403db1a9 100644
--- a/tests/lean/run/wfrecUnary.lean
+++ b/tests/lean/run/wfrecUnary.lean
@@ -3,7 +3,6 @@ def f (n : Nat) : Nat :=
     1
   else
     2 * f (n-1)
-termination_by' measure id
 decreasing_by
   simp [measure, id, invImage, InvImage, Nat.lt_wfRel]
   apply Nat.pred_lt h
diff --git a/tests/lean/substBadMotive.lean b/tests/lean/substBadMotive.lean
index d3621cdc2f8e..11c69899dca5 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' measure fun i => i.1
+termination_by _ i => 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' measure fun ⟨a, i⟩ => a.size - i.1
+termination_by _ a i => a.size - i.1
 decreasing_by assumption
 end Ex4
diff --git a/tests/lean/termination_by.lean b/tests/lean/termination_by.lean
index b1c239a99cf3..7e5ec0adca4d 100644
--- a/tests/lean/termination_by.lean
+++ b/tests/lean/termination_by.lean
@@ -5,20 +5,84 @@ mutual
   inductive Odd : Nat → Prop
     | step : Even n → Odd (n+1)
 end
-termination_by' measure
+termination_by _ n => n -- Error
 
 mutual
  def f (n : Nat) :=
    if n == 0 then 0 else f (n / 2) + 1
- termination_by' measure
+ 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 => measure
+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
+    | 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
@@ -34,8 +98,8 @@ mutual
     | 0, a, b => b
     | n+1, a, b => f n a b
 end
-termination_by'
-  f => measure
-  g => measure
+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 7e2cf1eb5836..6374b804cec9 100644
--- a/tests/lean/termination_by.lean.expected.out
+++ b/tests/lean/termination_by.lean.expected.out
@@ -1,4 +1,10 @@
 termination_by.lean:8:0-8:23: error: invalid 'termination_by' in mutually inductive datatype declaration
-termination_by.lean:13:1-13:24: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
-termination_by.lean:21:2-21:3: error: function 'h' not found in current declaration
-termination_by.lean:39:2-39:14: error: invalid termination hint element, 'Test.g' and 'Test.f' are in the same clique
+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'
diff --git a/tests/lean/termination_by2.lean b/tests/lean/termination_by2.lean
deleted file mode 100644
index e26fbd71e7c3..000000000000
--- a/tests/lean/termination_by2.lean
+++ /dev/null
@@ -1,68 +0,0 @@
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
- termination_by _ => n
-end
-
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
-end
-termination_by n => n
-
-
-def g' (n : Nat) :=
-  match n with
-  | 0 => 1
-  | n+1 => g' n * 3
-termination_by
-  g' n => n
-  _ n => n
-
-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 -- 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
diff --git a/tests/lean/termination_by2.lean.expected.out b/tests/lean/termination_by2.lean.expected.out
deleted file mode 100644
index 32628cf565bb..000000000000
--- a/tests/lean/termination_by2.lean.expected.out
+++ /dev/null
@@ -1,7 +0,0 @@
-termination_by2.lean:4:1-4:22: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
-termination_by2.lean:11:15-11:21: error: function 'n' not found in current declaration
-termination_by2.lean:20:2-20:10: error: invalid `termination_by` syntax, unnecessary else-case
-termination_by2.lean:31:3-31:16: error: invalid `termination_by` syntax, missing case for function 'isOdd'
-termination_by2.lean:43:3-43:14: error: function 'isOd' not found in current declaration
-termination_by2.lean:55:3-55:16: error: invalid `termination_by` syntax, `isEven` case has already been provided
-termination_by2.lean:68:3-68:15: error: invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified
diff --git a/tests/lean/unfold1.lean b/tests/lean/unfold1.lean
index 6a77120289f3..d153f3c6f0c6 100644
--- a/tests/lean/unfold1.lean
+++ b/tests/lean/unfold1.lean
@@ -6,7 +6,6 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun | PSum.inl n => n | PSum.inr n => n
 decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
diff --git a/tests/lean/wf2.lean b/tests/lean/wf2.lean
index 94bc3a290726..fee98b464d84 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' measure (·.1)
+termination_by g x y => x
diff --git a/tests/lean/wfrecUnusedLet.lean b/tests/lean/wfrecUnusedLet.lean
index 2a9f9dd07a1d..0108141e465f 100644
--- a/tests/lean/wfrecUnusedLet.lean
+++ b/tests/lean/wfrecUnusedLet.lean
@@ -4,7 +4,6 @@ def f (n : Nat) : Nat :=
   else
     let y := 42
     2 * f (n-1)
-termination_by' measure id
 decreasing_by
   simp [measure, id, invImage, InvImage, Nat.lt_wfRel, WellFoundedRelation.rel]
   apply Nat.pred_lt h
diff --git a/tests/lean/wfrecUnusedLet.lean.expected.out b/tests/lean/wfrecUnusedLet.lean.expected.out
index 38c47c9012b0..40e1995eaf32 100644
--- a/tests/lean/wfrecUnusedLet.lean.expected.out
+++ b/tests/lean/wfrecUnusedLet.lean.expected.out
@@ -3,4 +3,4 @@ WellFounded.fix f.proof_1 fun n a =>
   if h : n = 0 then 1
   else
     let y := 42;
-    2 * a (n - 1) (_ : (measure id).1 (n - 1) n)
+    2 * a (n - 1) (_ : (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (n - 1) n)