diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean
index 3a5c09ec5346f..dbb0ff14bddcc 100644
--- a/Archive/Wiedijk100Theorems/BallotProblem.lean
+++ b/Archive/Wiedijk100Theorems/BallotProblem.lean
@@ -171,7 +171,6 @@ 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`
 #align ballot.counted_sequence_finite Ballot.countedSequence_finite
 
 theorem countedSequence_nonempty : ∀ p q : ℕ, (countedSequence p q).Nonempty
@@ -215,7 +214,6 @@ 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`
 #align ballot.count_counted_sequence Ballot.count_countedSequence
 
 theorem first_vote_pos :
diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean
index a5529d9d8c89e..eddc5154b183b 100644
--- a/Mathlib/Analysis/Analytic/Inverse.lean
+++ b/Mathlib/Analysis/Analytic/Inverse.lean
@@ -62,7 +62,6 @@ noncomputable def leftInv (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[
     -∑ c : { c : Composition (n + 2) // c.length < n + 2 },
         (leftInv p i (c : Composition (n + 2)).length).compAlongComposition
           (p.compContinuousLinearMap i.symm) c
-  decreasing_by exact c.2
 #align formal_multilinear_series.left_inv FormalMultilinearSeries.leftInv
 
 @[simp]
diff --git a/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean b/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
index 9c83fc3ff22a1..17af84fddcf18 100644
--- a/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
+++ b/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
@@ -153,7 +153,6 @@ theorem gramSchmidt_mem_span (f : ι → E) :
   exact smul_mem _ _
     (span_mono (image_subset f <| Iic_subset_Iic.2 hkj.le) <| gramSchmidt_mem_span _ le_rfl)
 termination_by j => j
-decreasing_by exact hkj
 #align gram_schmidt_mem_span gramSchmidt_mem_span
 
 theorem span_gramSchmidt_Iic (f : ι → E) (c : ι) :
diff --git a/Mathlib/Computability/Ackermann.lean b/Mathlib/Computability/Ackermann.lean
index e0e4be045f901..8db134ecce020 100644
--- a/Mathlib/Computability/Ackermann.lean
+++ b/Mathlib/Computability/Ackermann.lean
@@ -65,7 +65,6 @@ def ack : ℕ → ℕ → ℕ
   | 0, n => n + 1
   | m + 1, 0 => ack m 1
   | m + 1, n + 1 => ack m (ack (m + 1) n)
-  termination_by m n => (m, n)
 #align ack ack
 
 @[simp]
@@ -145,7 +144,6 @@ theorem ack_strictMono_right : ∀ m, StrictMono (ack m)
     rw [ack_succ_succ, ack_succ_succ]
     apply ack_strictMono_right _ (ack_strictMono_right _ _)
     rwa [add_lt_add_iff_right] at h
-  termination_by m x => (m, x)
 #align ack_strict_mono_right ack_strictMono_right
 
 theorem ack_mono_right (m : ℕ) : Monotone (ack m) :=
@@ -186,7 +184,6 @@ theorem add_lt_ack : ∀ m n, m + n < ack m n
         ack_mono_right m <| le_of_eq_of_le (by rw [succ_eq_add_one]; ring_nf)
         <| succ_le_of_lt <| add_lt_ack (m + 1) n
       _ = ack (m + 1) (n + 1) := (ack_succ_succ m n).symm
-  termination_by m n => (m, n)
 #align add_lt_ack add_lt_ack
 
 theorem add_add_one_le_ack (m n : ℕ) : m + n + 1 ≤ ack m n :=
@@ -216,7 +213,6 @@ private theorem ack_strict_mono_left' : ∀ {m₁ m₂} (n), m₁ < m₂ → ack
     exact
       (ack_strict_mono_left' _ <| (add_lt_add_iff_right 1).1 h).trans
         (ack_strictMono_right _ <| ack_strict_mono_left' n h)
-  termination_by _ m n => (m, n)
 
 theorem ack_strictMono_left (n : ℕ) : StrictMono fun m => ack m n := fun _m₁ _m₂ =>
   ack_strict_mono_left' n
diff --git a/Mathlib/Computability/PartrecCode.lean b/Mathlib/Computability/PartrecCode.lean
index 78a9d071d08eb..803f18fcaac20 100644
--- a/Mathlib/Computability/PartrecCode.lean
+++ b/Mathlib/Computability/PartrecCode.lean
@@ -643,8 +643,6 @@ def evaln : ℕ → Code → ℕ → Option ℕ
         pure m
       else
         evaln k (rfind' cf) (Nat.pair a (m + 1))
-  termination_by k c => (k, c)
-  decreasing_by all_goals { decreasing_with (dsimp; omega) }
 #align nat.partrec.code.evaln Nat.Partrec.Code.evaln
 
 theorem evaln_bound : ∀ {k c n x}, x ∈ evaln k c n → n < k
diff --git a/Mathlib/Computability/RegularExpressions.lean b/Mathlib/Computability/RegularExpressions.lean
index 652a87a483ac5..6db4c57d67fb9 100644
--- a/Mathlib/Computability/RegularExpressions.lean
+++ b/Mathlib/Computability/RegularExpressions.lean
@@ -349,7 +349,7 @@ theorem star_rmatch_iff (P : RegularExpression α) :
             refine' ⟨U, rfl, fun t h => helem t _⟩
             right
             assumption
-  termination_by t => (P,t.length)
+  termination_by t => (P, t.length)
 #align regular_expression.star_rmatch_iff RegularExpression.star_rmatch_iff
 
 @[simp]
diff --git a/Mathlib/Data/BinaryHeap.lean b/Mathlib/Data/BinaryHeap.lean
index 81b0dbfe5433e..6931c8fdf263c 100644
--- a/Mathlib/Data/BinaryHeap.lean
+++ b/Mathlib/Data/BinaryHeap.lean
@@ -36,7 +36,6 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
     let ⟨a₂, h₂⟩ := heapifyDown lt a' j'
     ⟨a₂, h₂.trans (a.size_swap i j)⟩
 termination_by a.size - i
-decreasing_by assumption
 
 @[simp] theorem size_heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
   (heapifyDown lt a i).1.size = a.size := (heapifyDown lt a i).2
@@ -69,8 +68,6 @@ 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
-decreasing_by assumption
 
 @[simp] theorem size_heapifyUp (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
   (heapifyUp lt a i).1.size = a.size := (heapifyUp lt a i).2
@@ -173,5 +170,4 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
         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) #[]
diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean
index 9add70dde542b..0bd9a304aacfc 100644
--- a/Mathlib/Data/Fintype/Basic.lean
+++ b/Mathlib/Data/Fintype/Basic.lean
@@ -1274,7 +1274,6 @@ noncomputable def seqOfForallFinsetExistsAux {α : Type*} [DecidableEq α] (P :
       (h
         (Finset.image (fun i : Fin n => seqOfForallFinsetExistsAux P r h i)
           (Finset.univ : Finset (Fin n))))
-  decreasing_by all_goals exact i.2
 #align seq_of_forall_finset_exists_aux seqOfForallFinsetExistsAux
 
 /-- Induction principle to build a sequence, by adding one point at a time satisfying a given
diff --git a/Mathlib/Data/List/Infix.lean b/Mathlib/Data/List/Infix.lean
index 509a7d44aa0c3..9ae7ee37b1923 100644
--- a/Mathlib/Data/List/Infix.lean
+++ b/Mathlib/Data/List/Infix.lean
@@ -233,7 +233,6 @@ instance decidableSuffix [DecidableEq α] : ∀ l₁ l₂ : List α, Decidable (
     @decidable_of_decidable_of_iff _ _
       (@instDecidableOr _ _ _ (l₁.decidableSuffix l₂))
       suffix_cons_iff.symm
-termination_by l₁ l₂ => (l₁, l₂)
 #align list.decidable_suffix List.decidableSuffix
 
 instance decidableInfix [DecidableEq α] : ∀ l₁ l₂ : List α, Decidable (l₁ <:+: l₂)
@@ -243,7 +242,6 @@ instance decidableInfix [DecidableEq α] : ∀ l₁ l₂ : List α, Decidable (l
     @decidable_of_decidable_of_iff _ _
       (@instDecidableOr _ _ (l₁.decidablePrefix (b :: l₂)) (l₁.decidableInfix l₂))
       infix_cons_iff.symm
-termination_by l₁ l₂ => (l₁, l₂)
 #align list.decidable_infix List.decidableInfix
 
 theorem prefix_take_le_iff {L : List (List (Option α))} (hm : m < L.length) :
diff --git a/Mathlib/Data/List/Sort.lean b/Mathlib/Data/List/Sort.lean
index 0585d702ec4db..8895a14da8bc2 100644
--- a/Mathlib/Data/List/Sort.lean
+++ b/Mathlib/Data/List/Sort.lean
@@ -487,7 +487,6 @@ theorem Sorted.merge : ∀ {l l' : List α}, Sorted r l → Sorted r l' → Sort
         assumption
       · exact _root_.trans ba (rel_of_sorted_cons h₁ _ bl)
       · exact rel_of_sorted_cons h₂ _ bl'
-  termination_by l₁ l₂ => length l₁ + length l₂
 #align list.sorted.merge List.Sorted.merge
 
 variable (r)
diff --git a/Mathlib/Data/List/Sym.lean b/Mathlib/Data/List/Sym.lean
index 6bc6081fa7efa..943060b59bfe6 100644
--- a/Mathlib/Data/List/Sym.lean
+++ b/Mathlib/Data/List/Sym.lean
@@ -159,7 +159,6 @@ 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
 
 variable {xs ys : List α} {n : ℕ}
 
@@ -187,7 +186,6 @@ theorem sym_map {β : Type*} (f : α → β) (n : ℕ) (xs : List α) :
     congr
     ext s
     simp only [Function.comp_apply, Sym.map_cons]
-  termination_by 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 +200,6 @@ 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.length + ys.length
 
 theorem sym_sublist_sym_cons {a : α} : xs.sym n <+ (a :: xs).sym n :=
   (sublist_cons a xs).sym n
@@ -224,7 +221,6 @@ 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.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 +242,6 @@ 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.length
 
 theorem length_sym {n : ℕ} {xs : List α} :
     (xs.sym n).length = Nat.multichoose xs.length n :=
@@ -257,7 +252,6 @@ 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.length
 
 end Sym
 
diff --git a/Mathlib/Data/Nat/Cast/Defs.lean b/Mathlib/Data/Nat/Cast/Defs.lean
index 1c732e42657d8..4971077036f52 100644
--- a/Mathlib/Data/Nat/Cast/Defs.lean
+++ b/Mathlib/Data/Nat/Cast/Defs.lean
@@ -162,7 +162,6 @@ 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 all_goals { simp_wf; omega }
 #align nat.bin_cast Nat.binCast
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Choose/Basic.lean b/Mathlib/Data/Nat/Choose/Basic.lean
index 6c65d87df4435..560e1676522d2 100644
--- a/Mathlib/Data/Nat/Choose/Basic.lean
+++ b/Mathlib/Data/Nat/Choose/Basic.lean
@@ -372,7 +372,6 @@ where `choose` is the generalized binomial coefficient.
 
 -/
 
--- Porting note: `termination_by` required here where it wasn't before
 /--
 `multichoose n k` is the number of multisets of cardinality `k` from a type of cardinality `n`. -/
 def multichoose : ℕ → ℕ → ℕ
@@ -380,7 +379,6 @@ def multichoose : ℕ → ℕ → ℕ
   | 0, _ + 1 => 0
   | n + 1, k + 1 =>
     multichoose n (k + 1) + multichoose (n + 1) k
-  termination_by a b => (a, b)
 #align nat.multichoose Nat.multichoose
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean
index 8927ce4d89a0f..cb3e06ceb1ea4 100644
--- a/Mathlib/Data/Nat/Defs.lean
+++ b/Mathlib/Data/Nat/Defs.lean
@@ -550,7 +550,6 @@ def pincerRecursion {P : ℕ → ℕ → Sort*} (Ha0 : ∀ m : ℕ, P m 0) (H0b
   | m, 0 => Ha0 m
   | 0, n => H0b n
   | Nat.succ m, Nat.succ n => H _ _ (pincerRecursion Ha0 H0b H _ _) (pincerRecursion Ha0 H0b H _ _)
-termination_by n m => n + m
 #align nat.pincer_recursion Nat.pincerRecursion
 
 /-- Decreasing induction: if `P (k+1)` implies `P k` for all `m ≤ k < n`, then `P n` implies `P m`.
diff --git a/Mathlib/Data/Nat/Hyperoperation.lean b/Mathlib/Data/Nat/Hyperoperation.lean
index 3916234a05cd0..e1355e9fb3971 100644
--- a/Mathlib/Data/Nat/Hyperoperation.lean
+++ b/Mathlib/Data/Nat/Hyperoperation.lean
@@ -32,14 +32,12 @@ hyperoperation
 /-- Implementation of the hyperoperation sequence
 where `hyperoperation n m k` is the `n`th hyperoperation between `m` and `k`.
 -/
--- Porting note: termination_by was not required before port
 def hyperoperation : ℕ → ℕ → ℕ → ℕ
   | 0, _, k => k + 1
   | 1, m, 0 => m
   | 2, _, 0 => 0
   | _ + 3, _, 0 => 1
   | n + 1, m, k + 1 => hyperoperation n m (hyperoperation (n + 1) m k)
-  termination_by a b c => (a, b, c)
 #align hyperoperation hyperoperation
 
 -- Basic hyperoperation lemmas
diff --git a/Mathlib/Data/Prod/TProd.lean b/Mathlib/Data/Prod/TProd.lean
index f6ad035aad1f3..6609b922cc63d 100644
--- a/Mathlib/Data/Prod/TProd.lean
+++ b/Mathlib/Data/Prod/TProd.lean
@@ -109,7 +109,6 @@ theorem elim_mk : ∀ (l : List ι) (f : ∀ i, α i) {i : ι} (hi : i ∈ l), (
     · subst hji
       simp
     · rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]
-  termination_by l f j hj => l.length
 #align list.tprod.elim_mk List.TProd.elim_mk
 
 @[ext]
diff --git a/Mathlib/Data/Sym/Card.lean b/Mathlib/Data/Sym/Card.lean
index 271760c2e7c9b..922a1c3a91a56 100644
--- a/Mathlib/Data/Sym/Card.lean
+++ b/Mathlib/Data/Sym/Card.lean
@@ -104,7 +104,6 @@ theorem card_sym_fin_eq_multichoose : ∀ n k : ℕ, card (Sym (Fin n) k) = mult
     refine Fintype.card_congr (Equiv.symm ?_)
     apply (Sym.e1.symm.sumCongr Sym.e2.symm).trans
     apply Equiv.sumCompl
-  termination_by n k => n + k
 #align sym.card_sym_fin_eq_multichoose Sym.card_sym_fin_eq_multichoose
 
 /-- For any fintype `α` of cardinality `n`, `card (Sym α k) = multichoose (card α) k`. -/
diff --git a/Mathlib/GroupTheory/CommutingProbability.lean b/Mathlib/GroupTheory/CommutingProbability.lean
index 44488ec8614ae..043e0f82dd152 100644
--- a/Mathlib/GroupTheory/CommutingProbability.lean
+++ b/Mathlib/GroupTheory/CommutingProbability.lean
@@ -165,7 +165,6 @@ def reciprocalFactors (n : ℕ) : List ℕ :=
     3 :: reciprocalFactors (n / 2)
   else
     n % 4 * n :: reciprocalFactors (n / 4 + 1)
-decreasing_by all_goals { simp_wf; omega }
 
 @[simp] lemma reciprocalFactors_zero : reciprocalFactors 0 = [0] := rfl
 
diff --git a/Mathlib/RingTheory/Multiplicity.lean b/Mathlib/RingTheory/Multiplicity.lean
index f187165b757e8..130ff7e005df0 100644
--- a/Mathlib/RingTheory/Multiplicity.lean
+++ b/Mathlib/RingTheory/Multiplicity.lean
@@ -479,8 +479,8 @@ section CancelCommMonoidWithZero
 
 variable [CancelCommMonoidWithZero α]
 
-/- Porting note: removed previous wf recursion hints and added termination_by
-Also pulled a b intro parameters since Lean parses that more easily -/
+/- Porting note:
+Pulled a b intro parameters since Lean parses that more easily -/
 theorem finite_mul_aux {p : α} (hp : Prime p) {a b : α} :
     ∀ {n m : ℕ}, ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b
   | n, m => fun ha hb ⟨s, hs⟩ =>
@@ -512,7 +512,6 @@ theorem finite_mul_aux {p : α} (hp : Prime p) {a b : α} :
         ⟨s, mul_right_cancel₀ hp.1 (by
               rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]
               simp_all [mul_comm, mul_assoc, mul_left_comm, pow_add])⟩
-termination_by n m => n + m
 #align multiplicity.finite_mul_aux multiplicity.finite_mul_aux
 
 theorem finite_mul {p a b : α} (hp : Prime p) : Finite p a → Finite p b → Finite p (a * b) :=
diff --git a/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean b/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
index 69269cbfa2325..23e05866cabc5 100644
--- a/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
+++ b/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
@@ -193,8 +193,6 @@ theorem coeff_hermite_explicit :
     congr
     · 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)
 #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/WittVector/FrobeniusFractionField.lean b/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
index cd4949b8e6e5d..fbf7fe28056a9 100644
--- a/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
+++ b/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
@@ -202,7 +202,6 @@ noncomputable def frobeniusRotationCoeff {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coef
     (ha₂ : a₂.coeff 0 ≠ 0) : ℕ → k
   | 0 => solution p a₁ a₂
   | n + 1 => succNthVal p n a₁ a₂ (fun i => frobeniusRotationCoeff ha₁ ha₂ i.val) ha₁ ha₂
-decreasing_by apply Fin.is_lt
 #align witt_vector.frobenius_rotation_coeff WittVector.frobeniusRotationCoeff
 
 /-- For nonzero `a₁` and `a₂`, `frobeniusRotation a₁ a₂` is a Witt vector that satisfies the
diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean
index 3be6de9d52e7e..b46d98b6ad99d 100644
--- a/Mathlib/SetTheory/Game/Basic.lean
+++ b/Mathlib/SetTheory/Game/Basic.lean
@@ -423,7 +423,6 @@ def mulCommRelabelling (x y : PGame.{u}) : x * y ≡r y * x :=
         (mulCommRelabelling _ _).addCongr (mulCommRelabelling _ _)).subCongr
         (mulCommRelabelling _ _) }
   termination_by (x, y)
-  decreasing_by all_goals pgame_wf_tac
 #align pgame.mul_comm_relabelling SetTheory.PGame.mulCommRelabelling
 
 theorem quot_mul_comm (x y : PGame.{u}) : (⟦x * y⟧ : Game) = ⟦y * x⟧ :=
@@ -503,7 +502,6 @@ def negMulRelabelling (x y : PGame.{u}) : -x * y ≡r -(x * y) :=
         change -(mk xl xr xL xR * _) ≡r _
         exact (negMulRelabelling _ _).symm
   termination_by (x, y)
-  decreasing_by all_goals pgame_wf_tac
 #align pgame.neg_mul_relabelling SetTheory.PGame.negMulRelabelling
 
 @[simp]
@@ -617,7 +615,6 @@ theorem quot_left_distrib (x y z : PGame) : (⟦x * (y + z)⟧ : Game) = ⟦x *
         rw [quot_left_distrib (xR i) (mk yl yr yL yR) (zL k)]
         abel
   termination_by (x, y, z)
-  decreasing_by all_goals pgame_wf_tac
 #align pgame.quot_left_distrib SetTheory.PGame.quot_left_distrib
 
 /-- `x * (y + z)` is equivalent to `x * y + x * z.`-/
@@ -841,7 +838,6 @@ theorem quot_mul_assoc (x y z : PGame) : (⟦x * y * z⟧ : Game) = ⟦x * (y *
         rw [quot_mul_assoc (xR i) (yL j) (zL k)]
         abel
   termination_by (x, y, z)
-  decreasing_by all_goals pgame_wf_tac
 #align pgame.quot_mul_assoc SetTheory.PGame.quot_mul_assoc
 
 /-- `x * y * z` is equivalent to `x * (y * z).`-/
diff --git a/Mathlib/SetTheory/Game/Impartial.lean b/Mathlib/SetTheory/Game/Impartial.lean
index 3447c4acaf185..4d73aa5673b09 100644
--- a/Mathlib/SetTheory/Game/Impartial.lean
+++ b/Mathlib/SetTheory/Game/Impartial.lean
@@ -30,7 +30,6 @@ namespace PGame
 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`
-decreasing_by all_goals pgame_wf_tac
 #align pgame.impartial_aux SetTheory.PGame.ImpartialAux
 
 theorem impartialAux_def {G : PGame} :
@@ -89,7 +88,6 @@ theorem impartial_congr : ∀ {G H : PGame} (_ : G ≡r H) [G.Impartial], H.Impa
       ⟨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)
-decreasing_by all_goals pgame_wf_tac
 #align pgame.impartial.impartial_congr SetTheory.PGame.Impartial.impartial_congr
 
 instance impartial_add : ∀ (G H : PGame) [G.Impartial] [H.Impartial], (G + H).Impartial
@@ -106,7 +104,6 @@ instance impartial_add : ∀ (G H : PGame) [G.Impartial] [H.Impartial], (G + H).
         intro i; simp only [add_moveRight_inl, add_moveRight_inr]
         apply impartial_add
 termination_by G H => (G, H)
-decreasing_by all_goals pgame_wf_tac
 #align pgame.impartial.impartial_add SetTheory.PGame.Impartial.impartial_add
 
 instance impartial_neg : ∀ (G : PGame) [G.Impartial], (-G).Impartial
@@ -120,7 +117,6 @@ instance impartial_neg : ∀ (G : PGame) [G.Impartial], (-G).Impartial
     · rw [moveRight_neg']
       apply impartial_neg
 termination_by G => G
-decreasing_by all_goals pgame_wf_tac
 #align pgame.impartial.impartial_neg SetTheory.PGame.Impartial.impartial_neg
 
 variable (G : PGame) [Impartial G]
diff --git a/Mathlib/SetTheory/Game/Nim.lean b/Mathlib/SetTheory/Game/Nim.lean
index be9a9d18d7c21..01c24379de7d3 100644
--- a/Mathlib/SetTheory/Game/Nim.lean
+++ b/Mathlib/SetTheory/Game/Nim.lean
@@ -261,7 +261,6 @@ theorem nim_equiv_iff_eq {o₁ o₂ : Ordinal} : (nim o₁ ≈ nim o₂) ↔ o
 noncomputable def grundyValue : PGame.{u} → Ordinal.{u}
   | G => Ordinal.mex.{u, u} fun i => grundyValue (G.moveLeft i)
 termination_by G => G
-decreasing_by pgame_wf_tac
 #align pgame.grundy_value SetTheory.PGame.grundyValue
 
 theorem grundyValue_eq_mex_left (G : PGame) :
diff --git a/Mathlib/SetTheory/Game/Short.lean b/Mathlib/SetTheory/Game/Short.lean
index afa2609b6c918..8886c2656b958 100644
--- a/Mathlib/SetTheory/Game/Short.lean
+++ b/Mathlib/SetTheory/Game/Short.lean
@@ -239,7 +239,6 @@ def shortOfRelabelling : ∀ {x y : PGame.{u}}, Relabelling x y → Short x →
 instance shortNeg : ∀ (x : PGame.{u}) [Short x], Short (-x)
   | mk xl xr xL xR, _ => by
     exact Short.mk (fun i => shortNeg _) fun i => shortNeg _
--- Porting note: `decreasing_by pgame_wf_tac` is no longer needed.
 #align pgame.short_neg SetTheory.PGame.shortNeg
 
 instance shortAdd : ∀ (x y : PGame.{u}) [Short x] [Short y], Short (x + y)
@@ -249,9 +248,7 @@ instance shortAdd : ∀ (x y : PGame.{u}) [Short x] [Short y], Short (x + y)
       rintro ⟨i⟩
       · apply shortAdd
       · change Short (mk xl xr xL xR + _); apply shortAdd
--- Porting note: In Lean 3 `using_well_founded` didn't need this to be explicit.
 termination_by x y => (x, y)
--- Porting note: `decreasing_by pgame_wf_tac` is no longer needed.
 #align pgame.short_add SetTheory.PGame.shortAdd
 
 instance shortNat : ∀ n : ℕ, Short n
@@ -293,9 +290,7 @@ def leLFDecidable : ∀ (x y : PGame.{u}) [Short x] [Short y], Decidable (x ≤
       · apply @Fintype.decidableExistsFintype xr _ ?_ _
         intro i
         apply (leLFDecidable _ _).1
--- Porting note: In Lean 3 `using_well_founded` didn't need this to be explicit.
 termination_by x y => (x, y)
--- Porting note: `decreasing_by pgame_wf_tac` is no longer needed.
 #align pgame.le_lf_decidable SetTheory.PGame.leLFDecidable
 
 instance leDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x ≤ y) :=
diff --git a/Mathlib/SetTheory/Lists.lean b/Mathlib/SetTheory/Lists.lean
index e325afefd5bf8..8b0f60a76f4c8 100644
--- a/Mathlib/SetTheory/Lists.lean
+++ b/Mathlib/SetTheory/Lists.lean
@@ -358,7 +358,7 @@ instance instSetoidLists : Setoid (Lists α) :=
 section Decidable
 
 /-- Auxiliary function to prove termination of decidability checking -/
-@[simp, deprecated] -- Porting note: replaced by termination_by
+@[simp, deprecated]
 def Equiv.decidableMeas :
     (PSum (Σ' _l₁ : Lists α, Lists α) <|
         PSum (Σ' _l₁ : Lists' α true, Lists' α true) (Σ' _a : Lists α, Lists' α true)) →
diff --git a/Mathlib/SetTheory/Ordinal/NaturalOps.lean b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
index 41c5b81ec12ac..640dc04573bf8 100644
--- a/Mathlib/SetTheory/Ordinal/NaturalOps.lean
+++ b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
@@ -270,7 +270,6 @@ theorem nadd_comm : ∀ a b, a ♯ b = b ♯ a
   | a, b => by
     rw [nadd_def, nadd_def, max_comm]
     congr <;> ext <;> apply nadd_comm
-    -- Porting note: below was decreasing_by solve_by_elim [PSigma.Lex.left, PSigma.Lex.right]
   termination_by a b => (a,b)
 #align ordinal.nadd_comm Ordinal.nadd_comm
 
@@ -297,8 +296,6 @@ theorem nadd_assoc (a b c) : a ♯ b ♯ c = a ♯ (b ♯ c) := by
   · exact fun _ _ h => nadd_le_nadd_left h a
   · exact fun _ _ h => nadd_le_nadd_right h 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
 
 @[simp]
diff --git a/Mathlib/SetTheory/Surreal/Basic.lean b/Mathlib/SetTheory/Surreal/Basic.lean
index 981c9ca678102..30ddd10fc1f10 100644
--- a/Mathlib/SetTheory/Surreal/Basic.lean
+++ b/Mathlib/SetTheory/Surreal/Basic.lean
@@ -251,7 +251,6 @@ theorem add : ∀ {x y : PGame} (_ : Numeric x) (_ : Numeric y), Numeric (x + y)
         · apply (ox.moveRight jx).add oy
         · apply ox.add (oy.moveRight jy)⟩
 termination_by x y => (x, y) -- Porting note: Added `termination_by`
-decreasing_by all_goals pgame_wf_tac
 #align pgame.numeric.add SetTheory.PGame.Numeric.add
 
 theorem sub {x y : PGame} (ox : Numeric x) (oy : Numeric y) : Numeric (x - y) :=
diff --git a/Mathlib/Tactic/FailIfNoProgress.lean b/Mathlib/Tactic/FailIfNoProgress.lean
index 7510cb693be57..7544d90f2ec45 100644
--- a/Mathlib/Tactic/FailIfNoProgress.lean
+++ b/Mathlib/Tactic/FailIfNoProgress.lean
@@ -58,7 +58,6 @@ def lctxIsDefEq : (l₁ l₂ : List (Option LocalDecl)) → MetaM Bool
     lctxIsDefEq l₁ l₂
   | [], [] => return true
   | _, _ => return false
-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