From 31d5ba794f6be25df1a96247fb05b810718d708a Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 11 Dec 2023 12:56:51 +0100
Subject: [PATCH] More test fixing and updating

---
 src/Lean/Elab/LetRec.lean                     |  3 +-
 tests/lean/1050.lean.expected.out             |  2 +-
 tests/lean/StxQuot.lean.expected.out          |  8 +-
 tests/lean/guessLexFailures.lean              |  8 +-
 tests/lean/guessLexTricky.lean                | 27 ++++--
 tests/lean/heapSort.lean                      |  4 +-
 tests/lean/interactive/hover.lean             |  2 +-
 tests/lean/letRecMissingAnnotation.lean       |  2 +-
 tests/lean/mutwf1.lean                        | 27 +++---
 tests/lean/mutwf1.lean.expected.out           |  2 +-
 tests/lean/run/1171.lean                      |  2 +-
 tests/lean/run/1848.lean                      |  4 +-
 tests/lean/run/2810.lean                      |  2 +-
 tests/lean/run/860.lean                       | 24 ++---
 tests/lean/run/879.lean                       |  8 +-
 tests/lean/run/955.lean                       | 10 ++-
 tests/lean/run/ack.lean                       |  2 +-
 .../run/addDecorationsWithoutPartial.lean     |  2 +-
 tests/lean/run/binrec.lean                    |  4 +-
 tests/lean/run/constProp.lean                 |  6 +-
 .../run/decreasingTacticUpdatedEnvIssue.lean  |  2 +-
 tests/lean/run/defaultEliminator.lean         |  4 +-
 tests/lean/run/eqnsAtSimp.lean                | 10 ++-
 tests/lean/run/eqnsAtSimp2.lean               |  4 +-
 tests/lean/run/issue2628.lean                 | 32 ++++---
 tests/lean/run/issue2883.lean                 |  5 +-
 tests/lean/run/issue2925.lean                 |  4 +-
 tests/lean/run/letrecWFIssue.lean             |  9 +-
 tests/lean/run/mut_ind_wf.lean                | 12 ++-
 tests/lean/run/mutwf1.lean                    |  7 +-
 tests/lean/run/mutwf2.lean                    |  3 +-
 tests/lean/run/mutwf3.lean                    | 33 +++----
 tests/lean/run/mutwf4.lean                    |  6 +-
 tests/lean/run/nestedIssueMatch.lean          |  2 +-
 tests/lean/run/nestedWF.lean                  | 15 ++--
 tests/lean/run/overAndPartialAppsAtWF.lean    |  3 +-
 tests/lean/run/psumAtWF.lean                  |  5 +-
 tests/lean/run/renameFixedPrefix.lean         |  2 +-
 tests/lean/run/robinson.lean                  |  7 +-
 tests/lean/run/splitIssue.lean                |  3 +-
 tests/lean/run/splitList.lean                 | 11 +--
 tests/lean/run/wfEqns1.lean                   | 10 ++-
 tests/lean/run/wfEqns2.lean                   | 21 +++--
 tests/lean/run/wfEqns4.lean                   | 26 +++---
 tests/lean/run/wfLean3Issue.lean              |  2 +-
 tests/lean/run/wfOverapplicationIssue.lean    |  2 +-
 tests/lean/run/wfSum.lean                     |  2 +-
 tests/lean/termination_by.lean                | 89 ++-----------------
 tests/lean/termination_by.lean.expected.out   | 12 +--
 tests/lean/treeMap.lean                       |  2 +-
 tests/lean/unfold1.lean                       |  3 +-
 tests/lean/wf2.lean                           |  2 +-
 52 files changed, 234 insertions(+), 265 deletions(-)

diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 322a7eb07313..5440e1c0e16b 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -60,7 +60,8 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
         pure decl[4]
       else
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
-      let termination := WF.elabTerminationHints ⟨decl[5]⟩
+      -- TODO: Is this right?
+      let termination := WF.elabTerminationHints ⟨attrDeclStx[3]⟩
       pure {
         ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx, termination : LetRecDeclView }
     else
diff --git a/tests/lean/1050.lean.expected.out b/tests/lean/1050.lean.expected.out
index 193b6a7dc29e..2e395a2ae229 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/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index eccd27305301..c3fee261790b 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\") [])\n  []\n  (Termination.suffix [] [])))"
+"[(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   (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\") [])\n   []\n   (Termination.suffix [] [])))]"
 "`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\") [])\n  []\n  (Termination.suffix [] [])))"
+"[(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   (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\") [])\n   []\n   (Termination.suffix [] [])))]"
 "0"
 0
 1
diff --git a/tests/lean/guessLexFailures.lean b/tests/lean/guessLexFailures.lean
index 384eb0e90c02..db4a9a4d6425 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 m => 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 m => 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 m => 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 m => n
 decreasing_by decreasing_tactic
 
 end TrickyCode
diff --git a/tests/lean/guessLexTricky.lean b/tests/lean/guessLexTricky.lean
index cf73d92e8f84..cc4ace496877 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)
+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
-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
+
+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/heapSort.lean b/tests/lean/heapSort.lean
index a92bcca95af2..94ca0857e5b9 100644
--- a/tests/lean/heapSort.lean
+++ b/tests/lean/heapSort.lean
@@ -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 2c06a3c5b5dd..008c0823b5c5 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 8cebbfa38872..d529a5621099 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 i _ => 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 82b74ff71865..3364099f3a8c 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 => (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 => (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 066ec9cf1a0c..e0f562e89e25 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/1171.lean b/tests/lean/run/1171.lean
index d8a90e5d6ca4..79e585f7c777 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/1848.lean b/tests/lean/run/1848.lean
index a59b1bdeb926..b51d5d03381d 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 59037eddc790..30bb5398f66e 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 => n
 
 -- Same with rewrite
 
diff --git a/tests/lean/run/860.lean b/tests/lean/run/860.lean
index 106c708b395b..323582b1516b 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 _ _ => 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 c7fbf89a024f..f24aaf586de0 100644
--- a/tests/lean/run/879.lean
+++ b/tests/lean/run/879.lean
@@ -5,13 +5,9 @@ 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
+  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
+  y _ => y
diff --git a/tests/lean/run/955.lean b/tests/lean/run/955.lean
index 16016899c867..92a2221a3b86 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 61dbaae4a5f8..e86cc92c8a7e 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 4c9910c72e88..3fce9f0fb9ab 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 6933b6473a04..cd925a24e2a7 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 => n
+decreasing_by all_goals exact Nat.div2_lt h₁
 
 theorem Nat.binind
     (motive : Nat → Prop)
diff --git a/tests/lean/run/constProp.lean b/tests/lean/run/constProp.lean
index 67ecfb8e57c8..5ece46b07ca3 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 76d829809f91..9e422f1c0f1f 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 => x
diff --git a/tests/lean/run/defaultEliminator.lean b/tests/lean/run/defaultEliminator.lean
index bcd279164f06..0f4024c5d58d 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 => (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 8a9e97a3dc6f..fde04b5d3714 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 646f12d499ec..9f2f33d2791c 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/issue2628.lean b/tests/lean/run/issue2628.lean
index d9c7e9f90d14..d63c766d5440 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 b7541f94ecc7..2b07da1dc3ad 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 851ad599675d..e7af477c7d30 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 17158fcdcacc..9d86c76b1191 100644
--- a/tests/lean/run/letrecWFIssue.lean
+++ b/tests/lean/run/letrecWFIssue.lean
@@ -16,7 +16,8 @@ def Tree.size : Tree α → Nat
       apply Nat.lt_succ_self
     sizeList l
   | Tree.leaf _ => 1
-where sizeList : TreeList α → Nat
+where
+  sizeList : TreeList α → Nat
   | TreeList.nil => 0
   | TreeList.cons t l =>
     have : sizeOf t < 1 + sizeOf t + sizeOf l := by
@@ -28,7 +29,7 @@ where sizeList : TreeList α → Nat
       apply Nat.lt_succ_of_le
       apply Nat.le_add_left
     t.size + sizeList l
+  termination_by l => sizeOf 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 t => sizeOf t
diff --git a/tests/lean/run/mut_ind_wf.lean b/tests/lean/run/mut_ind_wf.lean
index fb01c71a8fa2..69aea4245033 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 2e75be80be4e..db76e4ac6bb4 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 d0cf4a6555c1..25b023121e5d 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 596d1cf517a3..1c1fefa9a1cc 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 acb31573cc17..10f62e0ed4df 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 => (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 0e91aaf6ee77..5b0ac54b41af 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 c69d75515321..e7af3f3b118c 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 c x => 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 c t a b => 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 c x => 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 c757f5ae77c0..d854d819fb23 100644
--- a/tests/lean/run/overAndPartialAppsAtWF.lean
+++ b/tests/lean/run/overAndPartialAppsAtWF.lean
@@ -17,7 +17,6 @@ termination_by _ => a.size - i
     fun z => f (x - 1) (y + 1) z + 1
   else
     (· + y)
-termination_by
-  f x y => x
+termination_by x y => x
 
 #check f._eq_1
diff --git a/tests/lean/run/psumAtWF.lean b/tests/lean/run/psumAtWF.lean
index 398b1f03e33c..30e30ce7c421 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 => n
 
 def gn (f : α → α) (a b : α) (n : Nat) : α :=
   match n with
   | 0 => b
   | n+1 => fn f (f b) n
+termination_by n => n
 
 end
-termination_by
-  fn n => n
-  gn n => n
diff --git a/tests/lean/run/renameFixedPrefix.lean b/tests/lean/run/renameFixedPrefix.lean
index 6862e6c0063f..3fd796447c64 100644
--- a/tests/lean/run/renameFixedPrefix.lean
+++ b/tests/lean/run/renameFixedPrefix.lean
@@ -3,4 +3,4 @@ def f (as : Array Nat) (hsz : as.size > 0) (i : Nat) : Nat :=
     as.get ⟨i, h⟩ + f as hsz (i + 1)
   else
     0
-termination_by f a h i => a.size - i
+termination_by a h i => a.size - i
diff --git a/tests/lean/run/robinson.lean b/tests/lean/run/robinson.lean
index 8ccc15fb4522..85f015fd533b 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 => (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/splitIssue.lean b/tests/lean/run/splitIssue.lean
index dcae8155e5ba..d44e90fab62d 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 23fd5353cee4..bbe78ef9e03c 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]
@@ -78,10 +78,11 @@ def len : List α → Nat
       len fst + len snd
 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/wfEqns1.lean b/tests/lean/run/wfEqns1.lean
index 8daaab858e95..4c61043f1abf 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 8d8ead206987..c9190d7e3cea 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 => (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 => (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 865f0ed7e24c..d6549693aaa2 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/wfLean3Issue.lean b/tests/lean/run/wfLean3Issue.lean
index f65609d9b753..3a41bb8cb393 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 69687ee0f625..b13a6ac33569 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 j => 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 764195fb121a..eea622cece80 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 i s => as.size - i
diff --git a/tests/lean/termination_by.lean b/tests/lean/termination_by.lean
index 7e5ec0adca4d..ad286f6a007e 100644
--- a/tests/lean/termination_by.lean
+++ b/tests/lean/termination_by.lean
@@ -1,105 +1,34 @@
-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
-
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
- 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
+/-!
+This module tests various mis-uses of termination_by,
+in particular that all or none of a recursive group have it.
+-/
 
 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
+  termination_by x => x
 
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
+  def isOdd : Nat → Bool -- Error
     | 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 6374b804cec9..64a418c08dcd 100644
--- a/tests/lean/termination_by.lean.expected.out
+++ b/tests/lean/termination_by.lean.expected.out
@@ -1,10 +1,2 @@
-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:12:6-12:11: error: Missing `termination_by`; this function is mutually recursive with isEven, which has a `termination_by` clause.
+termination_by.lean:29:6-29:7: error: Missing `termination_by`; this function is mutually recursive with Test.f, which has a `termination_by` clause.
diff --git a/tests/lean/treeMap.lean b/tests/lean/treeMap.lean
index 5dce56f8ef7f..64f00c3facb7 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 => t
diff --git a/tests/lean/unfold1.lean b/tests/lean/unfold1.lean
index d153f3c6f0c6..d13a64c7e509 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 fee98b464d84..e60566c641a8 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 y => x