diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean
index c4a2464181f5b..6aa782bb50739 100644
--- a/Archive/Wiedijk100Theorems/BallotProblem.lean
+++ b/Archive/Wiedijk100Theorems/BallotProblem.lean
@@ -167,7 +167,7 @@ theorem countedSequence_finite : ∀ p q : ℕ, (countedSequence p q).Finite
     rw [counted_succ_succ, Set.finite_union, Set.finite_image_iff (List.cons_injective.injOn _),
       Set.finite_image_iff (List.cons_injective.injOn _)]
     exact ⟨countedSequence_finite _ _, countedSequence_finite _ _⟩
-termination_by _ p q => p + q -- Porting note: Added `termination_by`
+termination_by p q => p + q -- Porting note: Added `termination_by`
 #align ballot.counted_sequence_finite Ballot.countedSequence_finite
 
 theorem countedSequence_nonempty : ∀ p q : ℕ, (countedSequence p q).Nonempty
@@ -211,7 +211,7 @@ theorem count_countedSequence : ∀ p q : ℕ, count (countedSequence p q) = (p
       count_injective_image List.cons_injective, count_countedSequence _ _]
     · norm_cast
       rw [add_assoc, add_comm 1 q, ← Nat.choose_succ_succ, Nat.succ_eq_add_one, add_right_comm]
-termination_by _ p q => p + q -- Porting note: Added `termination_by`
+termination_by p q => p + q -- Porting note: Added `termination_by`
 #align ballot.count_counted_sequence Ballot.count_countedSequence
 
 theorem first_vote_pos :
diff --git a/Mathlib/Algebra/EuclideanDomain/Defs.lean b/Mathlib/Algebra/EuclideanDomain/Defs.lean
index 2cfb9c7d7ce64..7d36ee585e6d8 100644
--- a/Mathlib/Algebra/EuclideanDomain/Defs.lean
+++ b/Mathlib/Algebra/EuclideanDomain/Defs.lean
@@ -186,7 +186,7 @@ theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x)
   else
     have _ := mod_lt b a0
     H1 _ _ a0 (GCD.induction (b % a) a H0 H1)
-termination_by _ => a
+termination_by => a
 #align euclidean_domain.gcd.induction EuclideanDomain.GCD.induction
 
 end
@@ -202,7 +202,7 @@ def gcd (a b : R) : R :=
   else
     have _ := mod_lt b a0
     gcd (b % a) a
-termination_by _ => a
+termination_by => a
 #align euclidean_domain.gcd EuclideanDomain.gcd
 
 @[simp]
@@ -226,7 +226,7 @@ def xgcdAux (r s t r' s' t' : R) : R × R × R :=
     let q := r' / r
     have _ := mod_lt r' _hr
     xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
-termination_by _ => r
+termination_by => r
 #align euclidean_domain.xgcd_aux EuclideanDomain.xgcdAux
 
 @[simp]
diff --git a/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean b/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
index fd4603f6783b3..a7a21ae35a89a 100644
--- a/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
+++ b/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
@@ -53,7 +53,7 @@ local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y
 and outputs a set of orthogonal vectors which have the same span. -/
 noncomputable def gramSchmidt [IsWellOrder ι (· < ·)] (f : ι → E) (n : ι) : E :=
   f n - ∑ i : Iio n, orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
-termination_by _ n => n
+termination_by n => n
 decreasing_by exact mem_Iio.1 i.2
 #align gram_schmidt gramSchmidt
 
@@ -152,7 +152,7 @@ theorem gramSchmidt_mem_span (f : ι → E) :
   let hkj : k < j := (Finset.mem_Iio.1 hk).trans_le hij
   exact smul_mem _ _
     (span_mono (image_subset f <| Iic_subset_Iic.2 hkj.le) <| gramSchmidt_mem_span _ le_rfl)
-termination_by _ => j
+termination_by => j
 decreasing_by exact hkj
 #align gram_schmidt_mem_span gramSchmidt_mem_span
 
diff --git a/Mathlib/Data/BinaryHeap.lean b/Mathlib/Data/BinaryHeap.lean
index 4b86e27cc2484..ec4bface8f11b 100644
--- a/Mathlib/Data/BinaryHeap.lean
+++ b/Mathlib/Data/BinaryHeap.lean
@@ -35,7 +35,7 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
       rw [a.size_swap i j]; exact Nat.sub_lt_sub_left i.2 <| Nat.lt_of_le_of_ne j.2 h
     let ⟨a₂, h₂⟩ := heapifyDown lt a' j'
     ⟨a₂, h₂.trans (a.size_swap i j)⟩
-termination_by _ => a.size - i
+termination_by => a.size - i
 decreasing_by assumption
 
 @[simp] theorem size_heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
@@ -69,7 +69,7 @@ if i0 : i.1 = 0 then ⟨a, rfl⟩ else
     let ⟨a₂, h₂⟩ := heapifyUp lt a' ⟨j.1, by rw [a.size_swap i j]; exact j.2⟩
     ⟨a₂, h₂.trans (a.size_swap i j)⟩
   else ⟨a, rfl⟩
-termination_by _ => i.1
+termination_by => i.1
 decreasing_by assumption
 
 @[simp] theorem size_heapifyUp (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
@@ -172,6 +172,6 @@ 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
diff --git a/Mathlib/Data/ByteArray.lean b/Mathlib/Data/ByteArray.lean
index 503831960c155..eaf213be3c164 100644
--- a/Mathlib/Data/ByteArray.lean
+++ b/Mathlib/Data/ByteArray.lean
@@ -58,7 +58,7 @@ def forIn.loop [Monad m] (f : UInt8 → β → m (ForInStep β))
     | ForInStep.done b => pure b
     | ForInStep.yield b => have := Nat.Up.next h; loop f arr off _end (i+1) b
   else pure b
-termination_by _ => _end - i
+termination_by => _end - i
 
 instance : ForIn m ByteSlice UInt8 :=
   ⟨fun ⟨arr, off, len⟩ b f ↦ forIn.loop f arr off (off + len) off b⟩
@@ -83,7 +83,7 @@ def String.toAsciiByteArray (s : String) : ByteArray :=
         (Nat.lt_add_of_pos_right (String.csize_pos _))
     loop (s.next p) (out.push c.toUInt8)
   loop 0 ByteArray.empty
-termination_by _ => utf8ByteSize s - p.byteIdx
+termination_by => utf8ByteSize s - p.byteIdx
 
 /-- Convert a byte slice into a string. This does not handle non-ASCII characters correctly:
 every byte will become a unicode character with codepoint < 256. -/
diff --git a/Mathlib/Data/Finset/LocallyFinite.lean b/Mathlib/Data/Finset/LocallyFinite.lean
index 9d9f6c0af93fe..b1e918e7f8d45 100644
--- a/Mathlib/Data/Finset/LocallyFinite.lean
+++ b/Mathlib/Data/Finset/LocallyFinite.lean
@@ -1215,7 +1215,7 @@ lemma transGen_wcovby_of_le [Preorder α] [LocallyFiniteOrder α] {x y : α} (hx
       refine ⟨(mem_Ico.mp z_mem).2.le, fun c hzc hcy ↦ hz c ?_ hzc⟩
       exact mem_Ico.mpr <| ⟨(mem_Ico.mp z_mem).1.trans hzc.le, hcy⟩
     exact .tail h₁ h₂
-termination_by _ => (Icc x y).card
+termination_by => (Icc x y).card
 
 /-- In a locally finite preorder, `≤` is the transitive closure of `⩿`. -/
 lemma le_iff_transGen_wcovby [Preorder α] [LocallyFiniteOrder α] {x y : α} :
@@ -1253,7 +1253,7 @@ lemma transGen_covby_of_lt [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy
   `x ≤ z`), and since `z ⋖ y` we conclude that `x ⋖ y` , then `Relation.TransGen.single`. -/
   · simp only [lt_iff_le_not_le, not_and, not_not] at hxz
     exact .single (hzy.of_le_of_lt (hxz (mem_Ico.mp z_mem).1) hxy)
-termination_by _ => (Ico x y).card
+termination_by => (Ico x y).card
 
 /-- In a locally finite preorder, `<` is the transitive closure of `⋖`. -/
 lemma lt_iff_transGen_covby [Preorder α] [LocallyFiniteOrder α] {x y : α} :
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
index f13b3ff8ff6af..c0ec87e20e8eb 100644
--- a/Mathlib/Data/List/Basic.lean
+++ b/Mathlib/Data/List/Basic.lean
@@ -956,7 +956,7 @@ def reverseRecOn {C : List α → Sort*} (l : List α) (H0 : C [])
     let ih := reverseRecOn (reverse tail) H0 H1
     rw [reverse_cons]
     exact H1 _ _ ih
-termination_by _ _ l _ _ => l.length
+termination_by _ l _ _ => l.length
 #align list.reverse_rec_on List.reverseRecOn
 
 /-- Bidirectional induction principle for lists: if a property holds for the empty list, the
@@ -973,7 +973,7 @@ def bidirectionalRec {C : List α → Sort*} (H0 : C []) (H1 : ∀ a : α, C [a]
     rw [← dropLast_append_getLast (cons_ne_nil b l)]
     have : C l' := bidirectionalRec H0 H1 Hn l'
     exact Hn a l' b' this
-termination_by _ l => l.length
+termination_by l => l.length
 #align list.bidirectional_rec List.bidirectionalRecₓ -- universe order
 
 /-- Like `bidirectionalRec`, but with the list parameter placed first. -/
diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean
index b318571705e5b..5e839afbb75dc 100644
--- a/Mathlib/Data/List/Defs.lean
+++ b/Mathlib/Data/List/Defs.lean
@@ -227,8 +227,8 @@ def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C []
   | [], is => H0 is
   | t :: ts, is =>
       H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
-  termination_by _ ts is => (length ts + length is, length ts)
-  decreasing_by simp_wf; simp [Nat.succ_add]; decreasing_tactic
+  termination_by ts is => (length ts + length is, length ts)
+  decreasing_by all_goals (simp_wf; simp [Nat.succ_add]; decreasing_tactic)
 #align list.permutations_aux.rec List.permutationsAux.rec
 
 /-- An auxiliary function for defining `permutations`. `permutationsAux ts is` is the set of all
diff --git a/Mathlib/Data/List/Sym.lean b/Mathlib/Data/List/Sym.lean
index c9122e6170a41..43e66a1f3b535 100644
--- a/Mathlib/Data/List/Sym.lean
+++ b/Mathlib/Data/List/Sym.lean
@@ -159,7 +159,7 @@ protected def sym : (n : ℕ) → List α → List (Sym α n)
   | 0, _ => [.nil]
   | _, [] => []
   | n + 1, x :: xs => ((x :: xs).sym n |>.map fun p => x ::ₛ p) ++ xs.sym (n + 1)
-  termination_by _ n xs => n + xs.length
+  termination_by n xs => n + xs.length
 
 variable {xs ys : List α} {n : ℕ}
 
@@ -187,7 +187,7 @@ theorem sym_map {β : Type*} (f : α → β) (n : ℕ) (xs : List α) :
     congr
     ext s
     simp only [Function.comp_apply, Sym.map_cons]
-  termination_by _ n xs => n + xs.length
+  termination_by n xs => n + xs.length
 
 protected theorem Sublist.sym (n : ℕ) {xs ys : List α} (h : xs <+ ys) : xs.sym n <+ ys.sym n :=
   match n, h with
@@ -202,7 +202,7 @@ protected theorem Sublist.sym (n : ℕ) {xs ys : List α} (h : xs <+ ys) : xs.sy
     apply Sublist.append
     · exact ((cons₂ a h).sym n).map _
     · exact h.sym (n + 1)
-  termination_by _ n xs ys h => n + xs.length + ys.length
+  termination_by n xs ys h => n + xs.length + ys.length
 
 theorem sym_sublist_sym_cons {a : α} : xs.sym n <+ (a :: xs).sym n :=
   (sublist_cons a xs).sym n
@@ -224,7 +224,7 @@ theorem mem_of_mem_of_mem_sym {n : ℕ} {xs : List α} {a : α} {z : Sym α n}
     · rw [mem_cons]
       right
       exact mem_of_mem_of_mem_sym ha hz
-  termination_by _ n xs _ _ _ _ => n + xs.length
+  termination_by n xs _ _ _ _ => n + xs.length
 
 theorem first_mem_of_cons_mem_sym {xs : List α} {n : ℕ} {a : α} {z : Sym α n}
     (h : a ::ₛ z ∈ xs.sym (n + 1)) : a ∈ xs :=
@@ -246,7 +246,7 @@ protected theorem Nodup.sym (n : ℕ) {xs : List α} (h : xs.Nodup) : (xs.sym n)
       obtain ⟨z, _hz, rfl⟩ := hz
       have := first_mem_of_cons_mem_sym hz'
       simp only [nodup_cons, this, not_true_eq_false, false_and] at h
-  termination_by _ n xs _ => n + xs.length
+  termination_by n xs _ => n + xs.length
 
 theorem length_sym {n : ℕ} {xs : List α} :
     (xs.sym n).length = Nat.multichoose xs.length n :=
@@ -257,7 +257,7 @@ theorem length_sym {n : ℕ} {xs : List α} :
     rw [List.sym, length_append, length_map, length_cons]
     rw [@length_sym n (x :: xs), @length_sym (n + 1) xs]
     rw [Nat.multichoose_succ_succ, length_cons, add_comm]
-  termination_by _ n xs => n + xs.length
+  termination_by n xs => n + xs.length
 
 end Sym
 
diff --git a/Mathlib/Data/Matroid/Basic.lean b/Mathlib/Data/Matroid/Basic.lean
index c7054c29dc0eb..7a4baefbbe6bb 100644
--- a/Mathlib/Data/Matroid/Basic.lean
+++ b/Mathlib/Data/Matroid/Basic.lean
@@ -270,7 +270,7 @@ theorem encard_diff_le_aux (exch : ExchangeProperty Base) (hB₁ : Base B₁) (h
 
   rw [← encard_diff_singleton_add_one he, ← encard_diff_singleton_add_one hf]
   exact add_le_add_right hencard 1
-termination_by _ => (B₂ \ B₁).encard
+termination_by => (B₂ \ B₁).encard
 
 /-- For any two sets `B₁`, `B₂` in a family with the exchange property, the differences `B₁ \ B₂`
 and `B₂ \ B₁` have the same `ℕ∞`-cardinality. -/
diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean
index 8d5c273a7e529..066d467503146 100644
--- a/Mathlib/Data/Multiset/Basic.lean
+++ b/Mathlib/Data/Multiset/Basic.lean
@@ -850,7 +850,7 @@ def strongInductionOn {p : Multiset α → Sort*} (s : Multiset α) (ih : ∀ s,
     p s :=
     (ih s) fun t _h =>
       strongInductionOn t ih
-termination_by _ => card s
+termination_by => card s
 decreasing_by exact card_lt_of_lt _h
 #align multiset.strong_induction_on Multiset.strongInductionOnₓ -- Porting note: reorderd universes
 
@@ -877,7 +877,7 @@ def strongDownwardInduction {p : Multiset α → Sort*} {n : ℕ}
     card s ≤ n → p s :=
   H s fun {t} ht _h =>
     strongDownwardInduction H t ht
-termination_by _ => n - card s
+termination_by => n - card s
 decreasing_by exact (tsub_lt_tsub_iff_left_of_le ht).2 (card_lt_of_lt _h)
 -- Porting note: reorderd universes
 #align multiset.strong_downward_induction Multiset.strongDownwardInductionₓ
diff --git a/Mathlib/Data/Nat/Cast/Defs.lean b/Mathlib/Data/Nat/Cast/Defs.lean
index 0ebe740d851d8..22deafaf48bd5 100644
--- a/Mathlib/Data/Nat/Cast/Defs.lean
+++ b/Mathlib/Data/Nat/Cast/Defs.lean
@@ -159,7 +159,7 @@ protected def binCast [Zero R] [One R] [Add R] : ℕ → R
   | n + 1 => if (n + 1) % 2 = 0
     then (Nat.binCast ((n + 1) / 2)) + (Nat.binCast ((n + 1) / 2))
     else (Nat.binCast ((n + 1) / 2)) + (Nat.binCast ((n + 1) / 2)) + 1
-decreasing_by (exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2))
+decreasing_by all_goals exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
 #align nat.bin_cast Nat.binCast
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Choose/Basic.lean b/Mathlib/Data/Nat/Choose/Basic.lean
index 5adc92bb73d49..16e1d022ba7bc 100644
--- a/Mathlib/Data/Nat/Choose/Basic.lean
+++ b/Mathlib/Data/Nat/Choose/Basic.lean
@@ -362,7 +362,7 @@ def multichoose : ℕ → ℕ → ℕ
   | 0, _ + 1 => 0
   | n + 1, k + 1 =>
     multichoose n (k + 1) + multichoose (n + 1) k
-  termination_by multichoose a b => (a, b)
+  termination_by a b => (a, b)
 #align nat.multichoose Nat.multichoose
 
 @[simp]
@@ -405,8 +405,8 @@ theorem multichoose_eq : ∀ n k : ℕ, multichoose n k = (n + k - 1).choose k
     have : (n + 1) + k < (n + 1) + (k + 1) := add_lt_add_left (Nat.lt_succ_self _) _
     erw [multichoose_succ_succ, add_comm, Nat.succ_add_sub_one, ← add_assoc, Nat.choose_succ_succ]
     simp [multichoose_eq n (k+1), multichoose_eq (n+1) k]
-  termination_by multichoose_eq a b => a + b
-  decreasing_by { assumption }
+  termination_by a b => a + b
+  decreasing_by all_goals assumption
 #align nat.multichoose_eq Nat.multichoose_eq
 
 end Nat
diff --git a/Mathlib/Data/Nat/Hyperoperation.lean b/Mathlib/Data/Nat/Hyperoperation.lean
index ad4daea7483e7..650b9ea88f566 100644
--- a/Mathlib/Data/Nat/Hyperoperation.lean
+++ b/Mathlib/Data/Nat/Hyperoperation.lean
@@ -39,7 +39,7 @@ def hyperoperation : ℕ → ℕ → ℕ → ℕ
   | 2, _, 0 => 0
   | _ + 3, _, 0 => 1
   | n + 1, m, k + 1 => hyperoperation n m (hyperoperation (n + 1) m k)
-  termination_by hyperoperation a b c => (a, b, c)
+  termination_by a b c => (a, b, c)
 #align hyperoperation hyperoperation
 
 -- Basic hyperoperation lemmas
diff --git a/Mathlib/Data/Nat/Order/Basic.lean b/Mathlib/Data/Nat/Order/Basic.lean
index bc4d65d56fde4..72024cf1970e5 100644
--- a/Mathlib/Data/Nat/Order/Basic.lean
+++ b/Mathlib/Data/Nat/Order/Basic.lean
@@ -350,8 +350,8 @@ theorem diag_induction (P : ℕ → ℕ → Prop) (ha : ∀ a, P (a + 1) (a + 1)
     have _ : a + (b + 1) < (a + 1) + (b + 1) := by simp
     apply diag_induction P ha hb hd a (b + 1)
     apply lt_of_le_of_lt (Nat.le_succ _) h
-  termination_by _ a b c => a + b
-  decreasing_by { assumption }
+  termination_by a b c => a + b
+  decreasing_by all_goals assumption
 #align nat.diag_induction Nat.diag_induction
 
 /-- A subset of `ℕ` containing `k : ℕ` and closed under `Nat.succ` contains every `n ≥ k`. -/
diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean
index bc3d5c3f5537d..83a5728bdff5b 100644
--- a/Mathlib/Data/Nat/Prime.lean
+++ b/Mathlib/Data/Nat/Prime.lean
@@ -255,7 +255,7 @@ def minFacAux (n : ℕ) : ℕ → ℕ
       else
         have := minFac_lemma n k h
         minFacAux n (k + 2)
-termination_by _ n k => sqrt n + 2 - k
+termination_by n k => sqrt n + 2 - k
 #align nat.min_fac_aux Nat.minFacAux
 
 /-- Returns the smallest prime factor of `n ≠ 1`. -/
@@ -306,7 +306,7 @@ theorem minFacAux_has_prop {n : ℕ} (n2 : 2 ≤ n) :
       have := a _ le_rfl (dvd_of_mul_right_dvd d')
       rw [e] at this
       exact absurd this (by contradiction)
-  termination_by _ n _ k => sqrt n + 2 - k
+  termination_by n _ k => sqrt n + 2 - k
 #align nat.min_fac_aux_has_prop Nat.minFacAux_has_prop
 
 theorem minFac_has_prop {n : ℕ} (n1 : n ≠ 1) : minFacProp n (minFac n) := by
diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean
index 24f6b53a0e8a3..ff464ca8cba16 100644
--- a/Mathlib/Data/Nat/Squarefree.lean
+++ b/Mathlib/Data/Nat/Squarefree.lean
@@ -127,7 +127,7 @@ def minSqFacAux : ℕ → ℕ → Option ℕ
         lt_of_le_of_lt (Nat.sub_le_sub_right (Nat.sqrt_le_sqrt <| Nat.div_le_self _ _) k) this
         if k ∣ n' then some k else minSqFacAux n' (k + 2)
       else minSqFacAux n (k + 2)
-termination_by _ n k => sqrt n + 2 - k
+termination_by n k => sqrt n + 2 - k
 #align nat.min_sq_fac_aux Nat.minSqFacAux
 
 /-- Returns the smallest prime factor `p` of `n` such that `p^2 ∣ n`, or `none` if there is no
@@ -202,7 +202,7 @@ theorem minSqFacAux_has_prop {n : ℕ} (k) (n0 : 0 < n) (i) (e : k = 2 * i + 3)
   · specialize IH (n / k) (div_dvd_of_dvd dk) dkk
     exact minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff dk).2 dkk) IH
   · exact IH n (dvd_refl _) dk
-termination_by _ => n.sqrt + 2 - k
+termination_by => n.sqrt + 2 - k
 #align nat.min_sq_fac_aux_has_prop Nat.minSqFacAux_has_prop
 
 theorem minSqFac_has_prop (n : ℕ) : MinSqFacProp n (minSqFac n) := by
diff --git a/Mathlib/Data/PNat/Defs.lean b/Mathlib/Data/PNat/Defs.lean
index 8ca1595b1193a..222606d2ecad7 100644
--- a/Mathlib/Data/PNat/Defs.lean
+++ b/Mathlib/Data/PNat/Defs.lean
@@ -207,7 +207,7 @@ instance : WellFoundedRelation ℕ+ :=
 /-- Strong induction on `ℕ+`. -/
 def strongInductionOn {p : ℕ+ → Sort*} (n : ℕ+) : (∀ k, (∀ m, m < k → p m) → p k) → p n
   | IH => IH _ fun a _ => strongInductionOn a IH
-termination_by _ => n.1
+termination_by => n.1
 #align pnat.strong_induction_on PNat.strongInductionOn
 
 /-- We define `m % k` and `m / k` in the same way as for `ℕ`
diff --git a/Mathlib/Data/Polynomial/Inductions.lean b/Mathlib/Data/Polynomial/Inductions.lean
index ef91eb3f944ee..31de6c6d5487e 100644
--- a/Mathlib/Data/Polynomial/Inductions.lean
+++ b/Mathlib/Data/Polynomial/Inductions.lean
@@ -163,7 +163,7 @@ noncomputable def recOnHorner {M : R[X] → Sort*} (p : R[X]) (M0 : M 0)
         MC _ _ (coeff_mul_X_zero _) hcp0
           (if hpX0 : divX p = 0 then show M (divX p * X) by rw [hpX0, zero_mul]; exact M0
           else MX (divX p) hpX0 (recOnHorner _ M0 MC MX))
-termination_by _ => p.degree
+termination_by => p.degree
 #align polynomial.rec_on_horner Polynomial.recOnHorner
 
 /-- A property holds for all polynomials of positive `degree` with coefficients in a semiring `R`
diff --git a/Mathlib/Data/Polynomial/RingDivision.lean b/Mathlib/Data/Polynomial/RingDivision.lean
index 0f8be5c6e7320..d31979f64d536 100644
--- a/Mathlib/Data/Polynomial/RingDivision.lean
+++ b/Mathlib/Data/Polynomial/RingDivision.lean
@@ -527,7 +527,7 @@ theorem exists_multiset_roots [DecidableEq R] :
       ⟨0, (degree_eq_natDegree hp).symm ▸ WithBot.coe_le_coe.2 (Nat.zero_le _), by
         intro a
         rw [count_zero, rootMultiplicity_eq_zero (not_exists.mp h a)]⟩
-termination_by _ p _ => natDegree p
+termination_by p _ => natDegree p
 decreasing_by {
   simp_wf
   apply (Nat.cast_lt (α := WithBot ℕ)).mp
diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index d61cf4bc106c3..68704471d3df5 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -437,7 +437,7 @@ theorem Finite.exists_injOn_of_encard_le [Nonempty β] {s : Set α} {t : Set β}
   refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
   · rintro x hx; split_ifs with h; assumption; exact (hf₀s x hx h).1
   exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_noteq])
-termination_by _ => encard s
+termination_by => encard s
 
 theorem Finite.exists_bijOn_of_encard_eq [Nonempty β] (hs : s.Finite) (h : s.encard = t.encard) :
     ∃ (f : α → β), BijOn f s t := by
diff --git a/Mathlib/Data/UnionFind.lean b/Mathlib/Data/UnionFind.lean
index a598cc0794698..319044dc0770c 100644
--- a/Mathlib/Data/UnionFind.lean
+++ b/Mathlib/Data/UnionFind.lean
@@ -241,7 +241,7 @@ def findAux (self : UnionFind α) (x : Fin self.size) :
       ⟨root.2, ?_⟩, le_of_lt this⟩
     have : x.1 ≠ root := mt (congrArg _) (ne_of_lt this); dsimp only at this
     simp [UFModel.setParent, this, hr]
-termination_by _ α self x => self.rankMax - self.rank x
+termination_by α self x => self.rankMax - self.rank x
 
 def find (self : UnionFind α) (x : Fin self.size) :
     (s : UnionFind α) × (root : Fin s.size) ×'
diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
index b0b0f7b1fc3a0..2c2a3a4ca60a1 100644
--- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
@@ -544,7 +544,7 @@ theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ f.support
           card_support_swap_mul hx.1
         rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]
         simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one]
-termination_by _ => f.support.card
+termination_by => f.support.card
 #align equiv.perm.is_cycle.sign Equiv.Perm.IsCycle.sign
 
 theorem IsCycle.of_pow {n : ℕ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) :
diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean
index f8b22f2e4d7cd..bb46c8447fbd8 100644
--- a/Mathlib/Order/RelClasses.lean
+++ b/Mathlib/Order/RelClasses.lean
@@ -289,7 +289,7 @@ instance WellFoundedRelation.isWellFounded [h : WellFoundedRelation α] :
 theorem WellFoundedRelation.asymmetric {α : Sort*} [WellFoundedRelation α] {a b : α} :
     WellFoundedRelation.rel a b → ¬ WellFoundedRelation.rel b a :=
   fun hab hba => WellFoundedRelation.asymmetric hba hab
-termination_by _ => a
+termination_by => a
 
 lemma WellFounded.prod_lex {ra : α → α → Prop} {rb : β → β → Prop} (ha : WellFounded ra)
     (hb : WellFounded rb) : WellFounded (Prod.Lex ra rb) :=
diff --git a/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean b/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
index d7ae21ff07f2c..7acf8dcdb705a 100644
--- a/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
+++ b/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
@@ -199,7 +199,7 @@ theorem coeff_hermite_explicit :
     · rw [coeff_hermite_explicit (n + 1) k]
     · rw [(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)), coeff_hermite_explicit n (k + 2)]
 -- porting note: Lean 3 worked this out automatically
-termination_by _ n k => (n, k)
+termination_by n k => (n, k)
 #align polynomial.coeff_hermite_explicit Polynomial.coeff_hermite_explicit
 
 theorem coeff_hermite_of_even_add {n k : ℕ} (hnk : Even (n + k)) :
diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean
index b37b2f078bd9e..847e41337ca43 100644
--- a/Mathlib/RingTheory/PowerSeries/Basic.lean
+++ b/Mathlib/RingTheory/PowerSeries/Basic.lean
@@ -850,7 +850,7 @@ protected noncomputable def inv.aux (a : R) (φ : MvPowerSeries σ R) : MvPowerS
     else
       -a *
         ∑ x in antidiagonal n, if _ : x.2 < n then coeff R x.1 φ * inv.aux a φ x.2 else 0
-termination_by _ n => n
+termination_by n => n
 #align mv_power_series.inv.aux MvPowerSeries.inv.aux
 
 theorem coeff_inv_aux [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) :
diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean
index 7df6126811ac3..0c6a76e581585 100644
--- a/Mathlib/SetTheory/Game/Basic.lean
+++ b/Mathlib/SetTheory/Game/Basic.lean
@@ -396,7 +396,7 @@ def mulCommRelabelling (x y : PGame.{u}) : x * y ≡r y * x :=
       exact ((addCommRelabelling _ _).trans <|
         (mulCommRelabelling _ _).addCongr (mulCommRelabelling _ _)).subCongr
         (mulCommRelabelling _ _) }
-  termination_by _ => (x, y)
+  termination_by => (x, y)
   decreasing_by pgame_wf_tac
 #align pgame.mul_comm_relabelling SetTheory.PGame.mulCommRelabelling
 
@@ -476,7 +476,7 @@ def negMulRelabelling (x y : PGame.{u}) : -x * y ≡r -(x * y) :=
         -- but if we just `change` it to look like the mathlib3 goal then we're fine!?
         change -(mk xl xr xL xR * _) ≡r _
         exact (negMulRelabelling _ _).symm
-  termination_by _ => (x, y)
+  termination_by => (x, y)
   decreasing_by pgame_wf_tac
 #align pgame.neg_mul_relabelling SetTheory.PGame.negMulRelabelling
 
@@ -590,7 +590,7 @@ theorem quot_left_distrib (x y z : PGame) : (⟦x * (y + z)⟧ : Game) = ⟦x *
         rw [quot_left_distrib (mk xl xr xL xR) (mk yl yr yL yR) (zL k)]
         rw [quot_left_distrib (xR i) (mk yl yr yL yR) (zL k)]
         abel
-  termination_by _ => (x, y, z)
+  termination_by => (x, y, z)
   decreasing_by pgame_wf_tac
 #align pgame.quot_left_distrib SetTheory.PGame.quot_left_distrib
 
@@ -815,7 +815,7 @@ theorem quot_mul_assoc (x y z : PGame) : (⟦x * y * z⟧ : Game) = ⟦x * (y *
         rw [quot_mul_assoc (mk xl xr xL xR) (yL j) (zL k)]
         rw [quot_mul_assoc (xR i) (yL j) (zL k)]
         abel
-  termination_by _ => (x, y, z)
+  termination_by => (x, y, z)
   decreasing_by pgame_wf_tac
 #align pgame.quot_mul_assoc SetTheory.PGame.quot_mul_assoc
 
diff --git a/Mathlib/SetTheory/Game/Impartial.lean b/Mathlib/SetTheory/Game/Impartial.lean
index 897054dc1185a..9c7de0f42eb61 100644
--- a/Mathlib/SetTheory/Game/Impartial.lean
+++ b/Mathlib/SetTheory/Game/Impartial.lean
@@ -29,7 +29,7 @@ namespace PGame
 /-- The definition for an impartial game, defined using Conway induction. -/
 def ImpartialAux : PGame → Prop
   | G => (G ≈ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j)
-termination_by _ G => G -- Porting note: Added `termination_by`
+termination_by G => G -- Porting note: Added `termination_by`
 decreasing_by pgame_wf_tac
 #align pgame.impartial_aux SetTheory.PGame.ImpartialAux
 
@@ -88,7 +88,7 @@ theorem impartial_congr : ∀ {G H : PGame} (_ : G ≡r H) [G.Impartial], H.Impa
     exact impartial_def.2
       ⟨Equiv.trans e.symm.equiv (Equiv.trans (neg_equiv_self G) (neg_equiv_neg_iff.2 e.equiv)),
         fun i => impartial_congr (e.moveLeftSymm i), fun j => impartial_congr (e.moveRightSymm j)⟩
-termination_by _ G H => (G, H)
+termination_by G H => (G, H)
 decreasing_by pgame_wf_tac
 #align pgame.impartial.impartial_congr SetTheory.PGame.Impartial.impartial_congr
 
@@ -105,7 +105,7 @@ instance impartial_add : ∀ (G H : PGame) [G.Impartial] [H.Impartial], (G + H).
       all_goals
         intro i; simp only [add_moveRight_inl, add_moveRight_inr]
         apply impartial_add
-termination_by _ G H _ _ => (G, H)
+termination_by G H _ _ => (G, H)
 decreasing_by pgame_wf_tac
 #align pgame.impartial.impartial_add SetTheory.PGame.Impartial.impartial_add
 
@@ -119,7 +119,7 @@ instance impartial_neg : ∀ (G : PGame) [G.Impartial], (-G).Impartial
       apply impartial_neg
     · rw [moveRight_neg']
       apply impartial_neg
-termination_by _ G _ => G
+termination_by G _ => G
 decreasing_by pgame_wf_tac
 #align pgame.impartial.impartial_neg SetTheory.PGame.Impartial.impartial_neg
 
diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean
index 948f843f6261d..019a3623d8faf 100644
--- a/Mathlib/SetTheory/Game/PGame.lean
+++ b/Mathlib/SetTheory/Game/PGame.lean
@@ -1124,7 +1124,7 @@ def moveRightSymm :
 @[refl]
 def refl (x : PGame) : x ≡r x :=
   ⟨Equiv.refl _, Equiv.refl _, fun i => refl _, fun j => refl _⟩
-termination_by _ => x
+termination_by => x
 #align pgame.relabelling.refl SetTheory.PGame.Relabelling.refl
 
 instance (x : PGame) : Inhabited (x ≡r x) :=
@@ -1140,7 +1140,7 @@ theorem le {x y : PGame} (r : x ≡r y) : x ≤ y :=
   le_def.2
     ⟨fun i => Or.inl ⟨_, (r.moveLeft i).le⟩, fun j =>
       Or.inr ⟨_, (r.moveRightSymm j).le⟩⟩
-termination_by _ => x
+termination_by => x
 #align pgame.relabelling.le SetTheory.PGame.Relabelling.le
 
 theorem ge {x y : PGame} (r : x ≡r y) : y ≤ x :=
@@ -1347,7 +1347,7 @@ private theorem neg_le_lf_neg_iff : ∀ {x y : PGame.{u}}, (-y ≤ -x ↔ x ≤
       apply and_congr <;> exact forall_congr' fun _ => neg_le_lf_neg_iff.2
     · rw [or_comm]
       apply or_congr <;> exact exists_congr fun _ => neg_le_lf_neg_iff.1
-termination_by _ x y => (x, y)
+termination_by x y => (x, y)
 
 @[simp]
 theorem neg_le_neg_iff {x y : PGame} : -y ≤ -x ↔ x ≤ y :=
@@ -1485,7 +1485,7 @@ def addZeroRelabelling : ∀ x : PGame.{u}, x + 0 ≡r x
   | ⟨xl, xr, xL, xR⟩ => by
     refine' ⟨Equiv.sumEmpty xl PEmpty, Equiv.sumEmpty xr PEmpty, _, _⟩ <;> rintro (⟨i⟩ | ⟨⟨⟩⟩) <;>
       apply addZeroRelabelling
-termination_by _ x => x
+termination_by x => x
 #align pgame.add_zero_relabelling SetTheory.PGame.addZeroRelabelling
 
 /-- `x + 0` is equivalent to `x`. -/
@@ -1627,7 +1627,7 @@ def Relabelling.addCongr : ∀ {w x y z : PGame.{u}}, w ≡r x → y ≡r z →
     · exact Hwx.addCongr (hL₂ j)
     · exact (hR₁ i).addCongr Hyz
     · exact Hwx.addCongr (hR₂ j)
-termination_by _ w x y z _ _ => (x, z)
+termination_by w x y z _ _ => (x, z)
 #align pgame.relabelling.add_congr SetTheory.PGame.Relabelling.addCongr
 
 instance : Sub PGame :=
@@ -1652,7 +1652,7 @@ def negAddRelabelling : ∀ x y : PGame, -(x + y) ≡r -x + -y
       exact fun j =>
         Sum.casesOn j (fun j => negAddRelabelling _ _) fun j =>
           negAddRelabelling ⟨xl, xr, xL, xR⟩ _
-termination_by _ x y => (x, y)
+termination_by x y => (x, y)
 #align pgame.neg_add_relabelling SetTheory.PGame.negAddRelabelling
 
 theorem neg_add_le {x y : PGame} : -(x + y) ≤ -x + -y :=
@@ -1665,7 +1665,7 @@ def addCommRelabelling : ∀ x y : PGame.{u}, x + y ≡r y + x
     refine' ⟨Equiv.sumComm _ _, Equiv.sumComm _ _, _, _⟩ <;> rintro (_ | _) <;>
       · dsimp [leftMoves_add, rightMoves_add]
         apply addCommRelabelling
-termination_by _ x y => (x, y)
+termination_by x y => (x, y)
 #align pgame.add_comm_relabelling SetTheory.PGame.addCommRelabelling
 
 theorem add_comm_le {x y : PGame} : x + y ≤ y + x :=
@@ -1688,7 +1688,7 @@ def addAssocRelabelling : ∀ x y z : PGame.{u}, x + y + z ≡r x + (y + z)
       · apply addAssocRelabelling
       · apply addAssocRelabelling ⟨xl, xr, xL, xR⟩ (yR i)
       · apply addAssocRelabelling ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ (zR i)
-termination_by _ x y z => (x, y, z)
+termination_by x y z => (x, y, z)
 #align pgame.add_assoc_relabelling SetTheory.PGame.addAssocRelabelling
 
 theorem add_assoc_equiv {x y z : PGame} : x + y + z ≈ x + (y + z) :=
@@ -1754,7 +1754,7 @@ private theorem add_le_add_right' : ∀ {x y z : PGame}, x ≤ y → x + z ≤ y
       · exact Or.inr ⟨toRightMovesAdd (Sum.inl j'), add_le_add_right' jh⟩
     · exact
         Or.inr ⟨@toRightMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), add_le_add_right' h⟩
-termination_by _ x y z => (x, y, z)
+termination_by x y z => (x, y, z)
 
 instance covariantClass_swap_add_le : CovariantClass PGame PGame (swap (· + ·)) (· ≤ ·) :=
   ⟨fun _ _ _ => add_le_add_right'⟩
diff --git a/Mathlib/SetTheory/Lists.lean b/Mathlib/SetTheory/Lists.lean
index 3b811c7d62078..2f5fd7c4942e4 100644
--- a/Mathlib/SetTheory/Lists.lean
+++ b/Mathlib/SetTheory/Lists.lean
@@ -402,6 +402,7 @@ mutual
           by decreasing_tactic
         Subset.decidable l₂ l₁
       exact decidable_of_iff' _ Equiv.antisymm_iff
+  termination_by x y => sizeOf x + sizeOf y
   instance Subset.decidable : ∀ l₁ l₂ : Lists' α true, Decidable (l₁ ⊆ l₂)
     | Lists'.nil, l₂ => isTrue Lists'.Subset.nil
     | @Lists'.cons' _ b a l₁, l₂ => by
@@ -414,6 +415,7 @@ mutual
           by decreasing_tactic
         Subset.decidable l₁ l₂
       exact decidable_of_iff' _ (@Lists'.cons_subset _ ⟨_, _⟩ _ _)
+  termination_by x y => sizeOf x + sizeOf y
   instance mem.decidable : ∀ (a : Lists α) (l : Lists' α true), Decidable (a ∈ l)
     | a, Lists'.nil => isFalse <| by rintro ⟨_, ⟨⟩, _⟩
     | a, Lists'.cons' b l₂ => by
@@ -428,11 +430,8 @@ mutual
         mem.decidable a l₂
       refine' decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) _
       rw [← Lists'.mem_cons]; rfl
+  termination_by x y => sizeOf x + sizeOf y
 end
-termination_by
-  Subset.decidable x y => sizeOf x + sizeOf y
-  Equiv.decidable x y => sizeOf x + sizeOf y
-  mem.decidable x y => sizeOf x + sizeOf y
 #align lists.equiv.decidable Lists.Equiv.decidable
 #align lists.subset.decidable Lists.Subset.decidable
 #align lists.mem.decidable Lists.mem.decidable
diff --git a/Mathlib/SetTheory/Ordinal/NaturalOps.lean b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
index 06f8498b63d63..90c640c590aad 100644
--- a/Mathlib/SetTheory/Ordinal/NaturalOps.lean
+++ b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
@@ -296,7 +296,7 @@ theorem nadd_assoc (a b c) : a ♯ b ♯ c = a ♯ (b ♯ c) := by
   · congr <;> ext (d hd) <;> apply nadd_assoc
   · exact fun _ _ h => nadd_le_nadd_left h a
   · exact fun _ _ h => nadd_le_nadd_right h c
-termination_by _ => (a, b, c)
+termination_by => (a, b, c)
 -- Porting note: above lines replaces
 -- decreasing_by solve_by_elim [PSigma.Lex.left, PSigma.Lex.right]
 #align ordinal.nadd_assoc Ordinal.nadd_assoc
diff --git a/Mathlib/SetTheory/Surreal/Basic.lean b/Mathlib/SetTheory/Surreal/Basic.lean
index 007650831d182..afa364d2cacab 100644
--- a/Mathlib/SetTheory/Surreal/Basic.lean
+++ b/Mathlib/SetTheory/Surreal/Basic.lean
@@ -250,7 +250,7 @@ theorem add : ∀ {x y : PGame} (_ : Numeric x) (_ : Numeric y), Numeric (x + y)
       · rintro (jx | jy)
         · apply (ox.moveRight jx).add oy
         · apply ox.add (oy.moveRight jy)⟩
-termination_by _ x y _ _ => (x, y) -- Porting note: Added `termination_by`
+termination_by x y _ _ => (x, y) -- Porting note: Added `termination_by`
 decreasing_by pgame_wf_tac
 #align pgame.numeric.add SetTheory.PGame.Numeric.add
 
diff --git a/Mathlib/SetTheory/ZFC/Basic.lean b/Mathlib/SetTheory/ZFC/Basic.lean
index 8bfc3b9f71fad..6a531d56a741f 100644
--- a/Mathlib/SetTheory/ZFC/Basic.lean
+++ b/Mathlib/SetTheory/ZFC/Basic.lean
@@ -1370,7 +1370,7 @@ theorem map_isFunc {f : ZFSet → ZFSet} [Definable 1 f] {x y : ZFSet} :
 members of `x` are all `Hereditarily p`. -/
 def Hereditarily (p : ZFSet → Prop) (x : ZFSet) : Prop :=
   p x ∧ ∀ y ∈ x, Hereditarily p y
-termination_by _ => x
+termination_by => x
 #align Set.hereditarily ZFSet.Hereditarily
 
 section Hereditarily
diff --git a/Mathlib/Tactic/Basic.lean b/Mathlib/Tactic/Basic.lean
index ed0d7527edb11..13b8a853502ea 100644
--- a/Mathlib/Tactic/Basic.lean
+++ b/Mathlib/Tactic/Basic.lean
@@ -22,11 +22,11 @@ syntax (name := «variables») "variables" (ppSpace bracketedBinder)* : command
 
 /-- `lemma` means the same as `theorem`. It is used to denote "less important" theorems -/
 syntax (name := lemma) declModifiers
-  group("lemma " declId ppIndent(declSig) declVal Parser.Command.terminationSuffix) : command
+  group("lemma " declId ppIndent(declSig) declVal) : command
 
 /-- Implementation of the `lemma` command, by macro expansion to `theorem`. -/
 @[macro «lemma»] def expandLemma : Macro := fun stx =>
-  -- FIXME: this should be a macro match, but terminationSuffix is not easy to bind correctly.
+  -- Not using a macro match, to be more resilient against changes to `lemma`.
   -- This implementation ensures that any future changes to `theorem` are reflected in `lemma`
   let stx := stx.modifyArg 1 fun stx =>
     let stx := stx.modifyArg 0 (mkAtomFrom · "theorem" (canonical := true))
diff --git a/Mathlib/Tactic/Core.lean b/Mathlib/Tactic/Core.lean
index d0b89a09f5755..e4a8e1921910c 100644
--- a/Mathlib/Tactic/Core.lean
+++ b/Mathlib/Tactic/Core.lean
@@ -61,7 +61,8 @@ def toPreDefinition (nm newNm : Name) (newType newValue : Expr) (newDoc : Option
     modifiers := mods
     declName := newNm
     type := newType
-    value := newValue }
+    value := newValue
+    termination := .none }
   return predef
 
 /-- Make `nm` protected. -/
diff --git a/Mathlib/Tactic/DeriveTraversable.lean b/Mathlib/Tactic/DeriveTraversable.lean
index 2bd7d81ad59f3..80df6e5c95c8a 100644
--- a/Mathlib/Tactic/DeriveTraversable.lean
+++ b/Mathlib/Tactic/DeriveTraversable.lean
@@ -179,7 +179,8 @@ def deriveFunctor (m : MVarId) : TermElabM Unit := do
                     stx := ← `(attr| specialize) }] }
           declName := n'
           type := t'
-          value := e' }] {}
+          value := e'
+          termination := .none }] {}
   m.assign (mkAppN (mkConst n' (levels.map Level.param)) vars.toArray)
 
 /-- Similar to `mkInstanceName`, but for a `Expr` type. -/
@@ -244,7 +245,8 @@ def mkOneInstance (n cls : Name) (tac : MVarId → TermElabM Unit)
                     stx := ← `(attr| instance) }] }
           declName := instN
           type := tgt
-          value := val }] {}
+          value := val
+          termination := .none }] {}
 
 /-- Make the new deriving handler depends on other deriving handlers. -/
 def higherOrderDeriveHandler (cls : Name) (tac : MVarId → TermElabM Unit)
@@ -415,7 +417,8 @@ def deriveTraversable (m : MVarId) : TermElabM Unit := do
               visibility := .protected }
           declName := n'
           type := t'
-          value := e' }] {}
+          value := e'
+          termination := .none }] {}
   m.assign (mkAppN (mkConst n' (levels.map Level.param)) vars.toArray)
 
 /-- The deriving handler for `Traversable`. -/
diff --git a/Mathlib/Tactic/FailIfNoProgress.lean b/Mathlib/Tactic/FailIfNoProgress.lean
index 04e85daed6574..3a8d785de32f2 100644
--- a/Mathlib/Tactic/FailIfNoProgress.lean
+++ b/Mathlib/Tactic/FailIfNoProgress.lean
@@ -57,7 +57,7 @@ def lctxIsDefEq : (l₁ l₂ : List (Option LocalDecl)) → MetaM Bool
     lctxIsDefEq l₁ l₂
   | [], [] => return true
   | _, _ => return false
-termination_by _ l₁ l₂ => l₁.length + l₂.length
+termination_by l₁ l₂ => l₁.length + l₂.length
 
 /-- Run `tacs : TacticM Unit` on `goal`, and fail if no progress is made. -/
 def runAndFailIfNoProgress (goal : MVarId) (tacs : TacticM Unit) : TacticM (List MVarId) := do
diff --git a/Mathlib/Tactic/SuppressCompilation.lean b/Mathlib/Tactic/SuppressCompilation.lean
index b98e2101ea461..1ac08b6e15869 100644
--- a/Mathlib/Tactic/SuppressCompilation.lean
+++ b/Mathlib/Tactic/SuppressCompilation.lean
@@ -28,25 +28,25 @@ to disable the compiler in a given file or a given section.
 This is a hack to work around mathlib4#7103. -/
 def elabSuppressCompilationDecl : CommandElab := fun
 | `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)?
-    $(recKind?)? def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?) => do
+    $(recKind?)? def $id $sig:optDeclSig $val:declVal) => do
   elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)?
-    $(recKind?)? def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?)
+    $(recKind?)? def $id $sig:optDeclSig $val:declVal)
 | `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)?
-    $(recKind?)? def $id $sig:optDeclSig $val:declVal deriving $derivs,* $(term?)? $(decr?)?) => do
+    $(recKind?)? def $id $sig:optDeclSig $val:declVal deriving $derivs,*) => do
   elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)?
-    $(recKind?)? def $id $sig:optDeclSig $val:declVal deriving $derivs,* $(term?)? $(decr?)?)
+    $(recKind?)? def $id $sig:optDeclSig $val:declVal deriving $derivs,*)
 | `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)?
-    $(recKind?)? $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal $(term?)?) => do
+    $(recKind?)? $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal) => do
   elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)?
-    $(recKind?)? $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal $(term?)?)
+    $(recKind?)? $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal)
 | `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)?
     $(recKind?)? example $sig:optDeclSig $val:declVal) => do
   elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)?
     $(recKind?)? example $sig:optDeclSig $val:declVal)
 | `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)?
-    $(recKind?)? abbrev $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?) => do
+    $(recKind?)? abbrev $id $sig:optDeclSig $val:declVal) => do
   elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)?
-    $(recKind?)? abbrev $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?)
+    $(recKind?)? abbrev $id $sig:optDeclSig $val:declVal)
 | _ => throwUnsupportedSyntax
 
 /-- The command `unsuppress_compilation in def foo : ...` makes sure that the definition is