diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 3b4f722fc940..a86f99e5613e 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -276,8 +276,8 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α 
       map (i+1) (r.push (← f as[i]))
     else
       pure r
+  termination_by as.size - i
   map 0 (mkEmpty as.size)
-termination_by map => as.size - i
 
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
@@ -348,12 +348,12 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
           loop (j+1)
       else
         pure false
+      termination_by stop - j
     loop start
   if h : stop ≤ as.size then
     any stop h
   else
     any as.size (Nat.le_refl _)
-termination_by loop i j => stop - j
 
 @[inline]
 def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool :=
@@ -523,7 +523,7 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (
      p a[i] b[i] && isEqvAux a b hsz p (i+1)
   else
     true
-termination_by _ => a.size - i
+termination_by a.size - i
 
 @[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
   if h : a.size = b.size then
@@ -627,7 +627,7 @@ def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)
     if a.get idx == v then some idx
     else indexOfAux a v (i+1)
   else none
-termination_by _ => a.size - i
+termination_by a.size - i
 
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
@@ -659,7 +659,7 @@ where
       loop as (i+1) ⟨j-1, this⟩
     else
       as
-termination_by _ => j - i
+termination_by j - i
 
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
@@ -669,7 +669,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
       as
   else
     as
-termination_by popWhile as => as.size
+termination_by as.size
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec go (i : Nat) (r : Array α) : Array α :=
@@ -681,8 +681,8 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
         r
     else
       r
+    termination_by as.size - i
   go 0 #[]
-termination_by go i r => as.size - i
 
 def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
   if h : i < a.size then
@@ -692,7 +692,7 @@ def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
     eraseIdxAux (i+1) a'
   else
     a.pop
-termination_by _ => a.size - i
+termination_by a.size - i
 
 def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   eraseIdxAux (i.val + 1) a
@@ -707,7 +707,7 @@ def eraseIdxSzAux (a : Array α) (i : Nat) (r : Array α) (heq : r.size = a.size
     eraseIdxSzAux a (i+1) (r.swap idx idx1) ((size_swap r idx idx1).trans heq)
   else
     ⟨r.pop, (size_pop r).trans (heq ▸ rfl)⟩
-termination_by _ => r.size - i
+termination_by r.size - i
 
 def eraseIdx' (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
   eraseIdxSzAux a (i.val + 1) a rfl
@@ -726,10 +726,10 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
     else
       as
+    termination_by j.1
   let j := as.size
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
-termination_by loop j => j.1
 
 /-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/
 def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
@@ -779,7 +779,7 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
       false
   else
     true
-termination_by _ => as.size - i
+termination_by as.size - i
 
 /-- Return true iff `as` is a prefix of `bs`.
 That is, `bs = as ++ t` for some `t : List α`.-/
@@ -800,7 +800,7 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
     allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
   else
     true
-termination_by _ => as.size - i
+termination_by as.size - i
 
 def allDiff [BEq α] (as : Array α) : Bool :=
   allDiffAux as 0
@@ -815,7 +815,7 @@ def allDiff [BEq α] (as : Array α) : Bool :=
       cs
   else
     cs
-termination_by _ => as.size - i
+termination_by as.size - i
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
   zipWithAux f as bs 0 #[]
diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean
index 1f8285b4992f..5d490c7689bf 100644
--- a/src/Init/Data/Array/BasicAux.lean
+++ b/src/Init/Data/Array/BasicAux.lean
@@ -47,7 +47,7 @@ where
       have hlt : i < as.size := Nat.lt_of_le_of_ne hle h
       let b ← f as[i]
       go (i+1) ⟨acc.val.push b, by simp [acc.property]⟩ hlt
-termination_by go i _ _ => as.size - i
+  termination_by as.size - i
 
 @[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α → m α) : m (Array α) :=
   go 0 as
diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean
index fb6c1f50bccc..f7f1cdbecaa6 100644
--- a/src/Init/Data/Array/DecidableEq.lean
+++ b/src/Init/Data/Array/DecidableEq.lean
@@ -20,7 +20,7 @@ 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
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
@@ -36,7 +36,7 @@ theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux
   split
   case inl h => simp [h, isEqvAux_self a (i+1)]
   case inr h => simp [h]
-termination_by _ => a.size - i
+termination_by a.size - i
 
 theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]
diff --git a/src/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean
index 2d46546d68f9..69e3749ac742 100644
--- a/src/Init/Data/Array/QSort.lean
+++ b/src/Init/Data/Array/QSort.lean
@@ -26,8 +26,8 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
     else
       let as := as.swap! i hi
       (i, as)
+    termination_by hi - j
   loop as lo lo
-termination_by _ => hi - j
 
 @[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=
   let rec @[specialize] sort (as : Array α) (low high : Nat) :=
diff --git a/src/Init/Data/Nat/Power2.lean b/src/Init/Data/Nat/Power2.lean
index 5255c0436560..46b1b29599d0 100644
--- a/src/Init/Data/Nat/Power2.lean
+++ b/src/Init/Data/Nat/Power2.lean
@@ -21,8 +21,8 @@ where
       go (power * 2) (Nat.mul_pos h (by decide))
     else
       power
-termination_by go p h => n - p
-decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
+  termination_by n - power
+  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
 
 def isPowerOfTwo (n : Nat) := ∃ k, n = 2 ^ k
 
@@ -48,7 +48,7 @@ where
     split
     . exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂)
     . assumption
-termination_by isPowerOfTwo_go p _ _ => n - p
-decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
+  termination_by n - power
+  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
 
 end Nat
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 0446969012c4..0d0dd7dd1348 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -159,7 +159,7 @@ def posOfAux (s : String) (c : Char) (stopPos : Pos) (pos : Pos) : Pos :=
       have := Nat.sub_lt_sub_left h (lt_next s pos)
       posOfAux s c stopPos (s.next pos)
   else pos
-termination_by _ => stopPos.1 - pos.1
+termination_by stopPos.1 - pos.1
 
 @[inline] def posOf (s : String) (c : Char) : Pos :=
   posOfAux s c s.endPos 0
@@ -171,7 +171,7 @@ def revPosOfAux (s : String) (c : Char) (pos : Pos) : Option Pos :=
     let pos := s.prev pos
     if s.get pos == c then some pos
     else revPosOfAux s c pos
-termination_by _ => pos.1
+termination_by pos.1
 
 def revPosOf (s : String) (c : Char) : Option Pos :=
   revPosOfAux s c s.endPos
@@ -183,7 +183,7 @@ def findAux (s : String) (p : Char → Bool) (stopPos : Pos) (pos : Pos) : Pos :
       have := Nat.sub_lt_sub_left h (lt_next s pos)
       findAux s p stopPos (s.next pos)
   else pos
-termination_by _ => stopPos.1 - pos.1
+termination_by stopPos.1 - pos.1
 
 @[inline] def find (s : String) (p : Char → Bool) : Pos :=
   findAux s p s.endPos 0
@@ -195,7 +195,7 @@ def revFindAux (s : String) (p : Char → Bool) (pos : Pos) : Option Pos :=
     let pos := s.prev pos
     if p (s.get pos) then some pos
     else revFindAux s p pos
-termination_by _ => pos.1
+termination_by pos.1
 
 def revFind (s : String) (p : Char → Bool) : Option Pos :=
   revFindAux s p s.endPos
@@ -213,8 +213,8 @@ def firstDiffPos (a b : String) : Pos :=
         have := Nat.sub_lt_sub_left h (lt_next a i)
         loop (a.next i)
     else i
+    termination_by stopPos.1 - i.1
   loop 0
-termination_by loop => stopPos.1 - i.1
 
 @[extern "lean_string_utf8_extract"]
 def extract : (@& String) → (@& Pos) → (@& Pos) → String
@@ -240,7 +240,7 @@ where
       splitAux s p i' i' (s.extract b i :: r)
     else
       splitAux s p b (s.next i) r
-termination_by _ => s.endPos.1 - i.1
+termination_by s.endPos.1 - i.1
 
 @[specialize] def split (s : String) (p : Char → Bool) : List String :=
   splitAux s p 0 0 []
@@ -260,7 +260,7 @@ def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String)
         splitOnAux s sep b i j r
     else
       splitOnAux s sep b (s.next i) 0 r
-termination_by _ => s.endPos.1 - i.1
+termination_by s.endPos.1 - i.1
 
 def splitOn (s : String) (sep : String := " ") : List String :=
   if sep == "" then [s] else splitOnAux s sep 0 0 0 []
@@ -369,7 +369,7 @@ def offsetOfPosAux (s : String) (pos : Pos) (i : Pos) (offset : Nat) : Nat :=
   else
     have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)
     offsetOfPosAux s pos (s.next i) (offset+1)
-termination_by _ => s.endPos.1 - i.1
+termination_by s.endPos.1 - i.1
 
 def offsetOfPos (s : String) (pos : Pos) : Nat :=
   offsetOfPosAux s pos 0 0
@@ -379,7 +379,7 @@ def offsetOfPos (s : String) (pos : Pos) : Nat :=
     have := Nat.sub_lt_sub_left h (lt_next s i)
     foldlAux f s stopPos (s.next i) (f a (s.get i))
   else a
-termination_by _ => stopPos.1 - i.1
+termination_by stopPos.1 - i.1
 
 @[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α :=
   foldlAux f s s.endPos 0 init
@@ -392,7 +392,7 @@ termination_by _ => stopPos.1 - i.1
     let a := f (s.get i) a
     foldrAux f a s i begPos
   else a
-termination_by _ => i.1
+termination_by i.1
 
 @[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α :=
   foldrAux f init s s.endPos 0
@@ -404,7 +404,7 @@ termination_by _ => i.1
       have := Nat.sub_lt_sub_left h (lt_next s i)
       anyAux s stopPos p (s.next i)
   else false
-termination_by _ => stopPos.1 - i.1
+termination_by stopPos.1 - i.1
 
 @[inline] def any (s : String) (p : Char → Bool) : Bool :=
   anyAux s s.endPos p 0
@@ -463,7 +463,7 @@ theorem mapAux_lemma (s : String) (i : Pos) (c : Char) (h : ¬s.atEnd i) :
     have := mapAux_lemma s i c h
     let s := s.set i c
     mapAux f (s.next i) s
-termination_by _ => s.endPos.1 - i.1
+termination_by s.endPos.1 - i.1
 
 @[inline] def map (f : Char → Char) (s : String) : String :=
   mapAux f 0 s
@@ -490,7 +490,7 @@ where
       have := Nat.sub_lt_sub_left h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
       c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
     else true
-termination_by loop => stop1.1 - off1.1
+  termination_by stop1.1 - off1.1
 
 /-- Return true iff `p` is a prefix of `s` -/
 def isPrefixOf (p : String) (s : String) : Bool :=
@@ -512,8 +512,8 @@ def replace (s pattern replacement : String) : String :=
         else
           have := Nat.sub_lt_sub_left this (lt_next s pos)
           loop acc accStop (s.next pos)
+      termination_by s.endPos.1 - pos.1
     loop "" 0 0
-termination_by loop => s.endPos.1 - pos.1
 
 end String
 
@@ -612,8 +612,8 @@ def splitOn (s : Substring) (sep : String := " ") : List Substring :=
         else
           s.extract b i :: r
         r.reverse
+      termination_by s.bsize - i.1
     loop 0 0 0 []
-termination_by loop => s.bsize - i.1
 
 @[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring) : α :=
   match s with
@@ -640,7 +640,7 @@ def contains (s : Substring) (c : Char) : Bool :=
       takeWhileAux s stopPos p (s.next i)
     else i
   else i
-termination_by _ => stopPos.1 - i.1
+termination_by stopPos.1 - i.1
 
 @[inline] def takeWhile : Substring → (Char → Bool) → Substring
   | ⟨s, b, e⟩, p =>
@@ -661,7 +661,7 @@ termination_by _ => stopPos.1 - i.1
     if !p c then i
     else takeRightWhileAux s begPos p i'
   else i
-termination_by _ => i.1
+termination_by i.1
 
 @[inline] def takeRightWhile : Substring → (Char → Bool) → Substring
   | ⟨s, b, e⟩, p =>
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 226d6b552a5f..9f01b280eb2f 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -1039,7 +1039,7 @@ where
       go (i+1) (args.push (quote xs[i]))
     else
       Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args
-termination_by go i _ => xs.size - i
+  termination_by xs.size - i
 
 instance [Quote α `term] : Quote (Array α) `term where
   quote := quoteArray
diff --git a/src/Lean/Compiler/LCNF/AlphaEqv.lean b/src/Lean/Compiler/LCNF/AlphaEqv.lean
index 476df24ebdf2..deb476b3d286 100644
--- a/src/Lean/Compiler/LCNF/AlphaEqv.lean
+++ b/src/Lean/Compiler/LCNF/AlphaEqv.lean
@@ -75,10 +75,10 @@ def eqvLetValue (e₁ e₂ : LetValue) : EqvM Bool := do
           go (i+1)
       else
         x
+      termination_by params₁.size - i
     go 0
   else
     return false
-termination_by go i => params₁.size - i
 
 def sortAlts (alts : Array Alt) : Array Alt :=
   alts.qsort fun
@@ -133,4 +133,4 @@ Return `true` if `c₁` and `c₂` are alpha equivalent.
 def Code.alphaEqv (c₁ c₂ : Code) : Bool :=
   AlphaEqv.eqv c₁ c₂ |>.run {}
 
-end Lean.Compiler.LCNF
\ No newline at end of file
+end Lean.Compiler.LCNF
diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean
index 1149e1ddea7b..c5208b30904c 100644
--- a/src/Lean/Compiler/LCNF/Specialize.lean
+++ b/src/Lean/Compiler/LCNF/Specialize.lean
@@ -181,8 +181,8 @@ def expandCodeDecls (decls : Array CodeDecl) (body : LetValue) : CompilerM Expr
       go (i+1) (subst.push value)
     else
       (body.toExpr.abstract xs).instantiateRev subst
+    termination_by values.size - i
   return go 0 #[]
-termination_by go => values.size - i
 
 /--
 Create the "key" that uniquely identifies a code specialization.
diff --git a/src/Lean/Compiler/LCNF/Types.lean b/src/Lean/Compiler/LCNF/Types.lean
index 612b0d84abaf..47e4a9f9de82 100644
--- a/src/Lean/Compiler/LCNF/Types.lean
+++ b/src/Lean/Compiler/LCNF/Types.lean
@@ -234,7 +234,7 @@ where
         throwError "invalid instantiateForall, too many parameters"
     else
       return type
-termination_by go i _ => ps.size - i
+  termination_by ps.size - i
 
 /--
 Return `true` if `type` is a predicate.
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index 99660540ba4b..59c5bd8c6b77 100644
--- a/src/Lean/Data/HashMap.lean
+++ b/src/Lean/Data/HashMap.lean
@@ -89,7 +89,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (targ
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target
-termination_by _ i source _ => source.size - i
+termination_by source.size - i
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let bucketsNew : HashMapBucket α β := ⟨
diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
index 43f77c721f58..7ddcb61ecfe3 100644
--- a/src/Lean/Data/HashSet.lean
+++ b/src/Lean/Data/HashSet.lean
@@ -80,7 +80,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : Has
      moveEntries (i+1) source target
   else
     target
-termination_by _ i source _ => source.size - i
+termination_by source.size - i
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let bucketsNew : HashSetBucket α := ⟨
diff --git a/src/Lean/Data/RBMap.lean b/src/Lean/Data/RBMap.lean
index 6b235c260ec7..3051c1734900 100644
--- a/src/Lean/Data/RBMap.lean
+++ b/src/Lean/Data/RBMap.lean
@@ -159,7 +159,7 @@ def appendTrees :  RBNode α β → RBNode α β → RBNode α β
      | bc                   => balLeft a kx vx (node black bc ky vy d)
    | a, node red b kx vx c   => node red (appendTrees a b) kx vx c
    | node red a kx vx b,   c => node red a kx vx (appendTrees b c)
-termination_by _ x y => x.size + y.size
+termination_by x y => x.size + y.size
 
 section Erase
 
diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean
index e77e76b27eb3..5bc5c76f0cbb 100644
--- a/src/Lean/DocString.lean
+++ b/src/Lean/DocString.lean
@@ -36,13 +36,12 @@ where
        if it.atEnd then r
        else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
        else saveLine it r
+  termination_by (it, 1)
   saveLine (it : String.Iterator) (r : String) : String :=
     if it.atEnd then r
     else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
     else saveLine it.next (r.push it.curr)
-termination_by
-  consumeSpaces n it r => (it, 1)
-  saveLine it r => (it, 0)
+  termination_by (it, 0)
 
 def removeLeadingSpaces (s : String) : String :=
   let n := findLeadingSpacesSize s
diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
index 66cafe32f6e7..adf1c1c4d4e6 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
@@ -91,9 +91,6 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
   -- 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
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index d931220cc193..94c6238b88e7 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -606,7 +606,7 @@ where
       let v' := v.getLevelOffset
       (u.getLevelOffset == v' || v'.isZero)
       && u.getOffset ≥ v.getOffset
-termination_by _ u v => (u, v)
+  termination_by (u, v)
 
 end Level
 
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index f206c9d33f86..40d79de27406 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -419,7 +419,7 @@ where
         loop (i+1)
     else
       vs.push v
-termination_by loop i => vs.size - i
+  termination_by vs.size - i
 
 private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
   | i, .node vs cs =>
diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index 06dfdaa85815..83f1ead54c80 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -171,6 +171,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
       else
         let (_, _, eType) ← forallMetaTelescopeReducing eType (some rangeNumArgs.start)
         throwApplyError mvarId eType targetType
+      termination_by rangeNumArgs.stop - i
     let (newMVars, binderInfos) ← go rangeNumArgs.start
     postprocessAppMVars `apply mvarId newMVars binderInfos cfg.synthAssignedInstances cfg.allowSynthFailures
     let e ← instantiateMVars e
@@ -182,7 +183,6 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
     let result := newMVarIds ++ otherMVarIds.toList
     result.forM (·.headBetaType)
     return result
-termination_by go i => rangeNumArgs.stop - i
 
 @[deprecated MVarId.apply]
 def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
diff --git a/src/Lean/Meta/Tactic/LinearArith/Solver.lean b/src/Lean/Meta/Tactic/LinearArith/Solver.lean
index 6b02bc1db133..adcf75f109e5 100644
--- a/src/Lean/Meta/Tactic/LinearArith/Solver.lean
+++ b/src/Lean/Meta/Tactic/LinearArith/Solver.lean
@@ -77,8 +77,8 @@ def Poly.add (e₁ e₂ : Poly) : Poly :=
         go i₁ (i₂+1) (r.push (e₂.get ⟨i₂, h₂⟩))
       else
         { val := r }
+    termination_by (e₁.size - i₁, e₂.size - i₂)
   go 0 0 #[]
-termination_by go i j _ => (e₁.size - i, e₂.size - j)
 
 def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
   let rec go (i₁ i₂ : Nat) (r : Array (Int × Var)) : Poly :=
@@ -104,8 +104,8 @@ def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
         go i₁ (i₂+1) (r.push (d₂*c₂, x₂))
       else
         { val := r }
+    termination_by (e₁.size - i₁, e₂.size - i₂)
   go 0 0 #[]
-termination_by go i j _ => (e₁.size - i, e₂.size - j)
 
 def Poly.eval? (e : Poly) (a : Assignment) : Option Rat := Id.run do
   let mut r := 0