chore: remove legacy termination_by' (#5426)

This adds a couple of `WellFoundedRelation` instances, like for example `WellFoundedRelation (WithBot Nat)`.  Longer-term, we should probably add a `WellFoundedOrder` class for types with a well-founded less-than relation and a `[WellFoundOrder α] : WellFoundedRelation α` instance (or maybe just `[LT α] [IsWellFounded fun a b : α => a < b] : WellFoundedRelation α`).

Mathlib/Algebra/EuclideanDomain/Defs.lean

@@ -113,6 +113,9 @@ variable {R : Type u} [EuclideanDomain R]
 /-- Abbreviated notation for the well-founded relation `r` in a Euclidean domain. -/
 local infixl:50 " ≺ " => EuclideanDomain.r
 
+local instance wellFoundedRelation : WellFoundedRelation R where
+  wf := r_wellFounded
+
 -- see Note [lower instance priority]
 instance (priority := 70) : Div R :=
   ⟨EuclideanDomain.quotient⟩
@@ -177,18 +180,17 @@ section
 open Classical
 
 @[elab_as_elim]
-theorem GCD.induction {P : R → R → Prop} :
-    ∀ a b : R, (H0 : ∀ x, P 0 x) → (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) → P a b
-  | a => fun b H0 H1 =>
-    if a0 : a = 0 then by
-      -- Porting note: required for hygiene, the equation compiler introduces a dummy variable `x`
-      -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unnecessarily.20tombstoned.20argument/near/314573315
-      change P a b
-      exact a0.symm ▸ H0 b
-    else
-      have _ := mod_lt b a0
-      H1 _ _ a0 (GCD.induction (b % a) a H0 H1)
-  termination_by' ⟨_, r_wellFounded⟩
+theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x)
+    (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) : P a b :=
+  if a0 : a = 0 then by
+    -- Porting note: required for hygiene, the equation compiler introduces a dummy variable `x`
+    -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unnecessarily.20tombstoned.20argument/near/314573315
+    change P a b
+    exact a0.symm ▸ H0 b
+  else
+    have _ := mod_lt b a0
+    H1 _ _ a0 (GCD.induction (b % a) a H0 H1)
+termination_by _ => a
 #align euclidean_domain.gcd.induction EuclideanDomain.GCD.induction
 
 end
@@ -199,13 +201,12 @@ variable [DecidableEq R]
 
 /-- `gcd a b` is a (non-unique) element such that `gcd a b ∣ a` `gcd a b ∣ b`, and for
   any element `c` such that `c ∣ a` and `c ∣ b`, then `c ∣ gcd a b` -/
-def gcd : R → R → R
-  | a => fun b =>
-    if a0 : a = 0 then b
-    else
-      have _ := mod_lt b a0
-      gcd (b % a) a
-  termination_by' ⟨_, r_wellFounded⟩
+def gcd (a b : R) : R :=
+  if a0 : a = 0 then b
+  else
+    have _ := mod_lt b a0
+    gcd (b % a) a
+termination_by _ => a
 #align euclidean_domain.gcd EuclideanDomain.gcd
 
 @[simp]
@@ -223,14 +224,13 @@ The function `xgcdAux` takes in two triples, and from these recursively computes
 xgcdAux (r, s, t) (r', s', t') = xgcdAux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t)
 ```
 -/
-def xgcdAux : R → R → R → R → R → R → R × R × R
-  | r => fun s t r' s' t' =>
-    if _hr : r = 0 then (r', s', t')
-    else
-      let q := r' / r
-      xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
-  termination_by' ⟨_, r_wellFounded⟩
-  decreasing_by (exact mod_lt _ _hr)
+def xgcdAux (r s t r' s' t' : R) : R × R × R :=
+  if _hr : r = 0 then (r', s', t')
+  else
+    let q := r' / r
+    have _ := mod_lt r' _hr
+    xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
+termination_by _ => r
 #align euclidean_domain.xgcd_aux EuclideanDomain.xgcdAux
 
 @[simp]

Mathlib/Data/Finsupp/Multiset.lean

@@ -233,6 +233,11 @@ theorem lt_wf : WellFounded (@LT.lt (ι →₀ ℕ) _) :=
   Subrelation.wf (sum_id_lt_of_lt _ _) <| InvImage.wf _ Nat.lt_wfRel.2
 #align finsupp.lt_wf Finsupp.lt_wf
 
+-- TODO: generalize to `[WellFoundedRelation α] → WellFoundedRelation (ι →₀ α)`
+instance : WellFoundedRelation (ι →₀ ℕ) where
+  rel := (· < ·)
+  wf := lt_wf _
+
 end Finsupp
 
 theorem Multiset.toFinsupp_strictMono : StrictMono (@Multiset.toFinsupp ι) :=

Mathlib/Data/List/Basic.lean

@@ -1018,7 +1018,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' measure List.length
+termination_by _ l => l.length
 #align list.bidirectional_rec List.bidirectionalRecₓ -- universe order
 
 /-- Like `bidirectionalRec`, but with the list parameter placed first. -/

Mathlib/Data/Nat/Cast/WithTop.lean

@@ -18,6 +18,9 @@ An orphaned lemma about casting from `ℕ` to `WithBot ℕ`,
 exiled here to minimize imports to `data.rat.order` for porting purposes.
 -/
 
+instance : WellFoundedRelation (WithTop ℕ) where
+  rel := (· < ·)
+  wf := IsWellFounded.wf
 
 theorem Nat.cast_withTop (n : ℕ) :  Nat.cast n = WithTop.some n :=
   rfl

Mathlib/Data/Nat/Squarefree.lean

@@ -154,46 +154,45 @@ theorem minSqFacProp_div (n) {k} (pk : Prime k) (dk : k ∣ n) (dkk : ¬k * k 
 #align nat.min_sq_fac_prop_div Nat.minSqFacProp_div
 
 --Porting note: I had to replace two uses of `by decide` by `linarith`.
-theorem minSqFacAux_has_prop :
-    ∀ {n : ℕ} (k),
-      0 < n → ∀ i, k = 2 * i + 3 → (∀ m, Prime m → m ∣ n → k ≤ m) → MinSqFacProp n (minSqFacAux n k)
-  | n, k => fun n0 i e ih => by
-    rw [minSqFacAux]
-    by_cases h : n < k * k <;> simp [h]
-    · refine' squarefree_iff_prime_squarefree.2 fun p pp d => _
-      have := ih p pp (dvd_trans ⟨_, rfl⟩ d)
-      have := Nat.mul_le_mul this this
-      exact not_le_of_lt h (le_trans this (le_of_dvd n0 d))
-    have k2 : 2 ≤ k := by
-      subst e
-      linarith
-    have k0 : 0 < k := lt_of_lt_of_le (by decide) k2
-    have IH : ∀ n', n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (n'.minSqFacAux (k + 2)) := by
-      intro n' nd' nk
-      have hn' := le_of_dvd n0 nd'
-      refine'
-        have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k :=
-          lt_of_le_of_lt (Nat.sub_le_sub_right (Nat.sqrt_le_sqrt hn') _) (Nat.minFac_lemma n k h)
-        @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1)
-          (by simp [e, left_distrib]) fun m m2 d => _
-      cases' Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me ml
-      · subst me
-        contradiction
-      apply (Nat.eq_or_lt_of_le ml).resolve_left
-      intro me
-      rw [← me, e] at d
-      change 2 * (i + 2) ∣ n' at d
-      have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
-      rw [e] at this
-      exact absurd this (by linarith)
-    have pk : k ∣ n → Prime k := by
-      refine' fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) _⟩
-      exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)
-    split_ifs with dk dkk
-    · exact ⟨pk dk, (Nat.dvd_div_iff dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩
-    · 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' ⟨_, (measure fun ⟨n, k⟩ => Nat.sqrt n + 2 - k).wf⟩
+theorem minSqFacAux_has_prop {n : ℕ} (k) (n0 : 0 < n) (i) (e : k = 2 * i + 3)
+    (ih : ∀ m, Prime m → m ∣ n → k ≤ m) : MinSqFacProp n (minSqFacAux n k) := by
+  rw [minSqFacAux]
+  by_cases h : n < k * k <;> simp [h]
+  · refine' squarefree_iff_prime_squarefree.2 fun p pp d => _
+    have := ih p pp (dvd_trans ⟨_, rfl⟩ d)
+    have := Nat.mul_le_mul this this
+    exact not_le_of_lt h (le_trans this (le_of_dvd n0 d))
+  have k2 : 2 ≤ k := by
+    subst e
+    linarith
+  have k0 : 0 < k := lt_of_lt_of_le (by decide) k2
+  have IH : ∀ n', n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (n'.minSqFacAux (k + 2)) := by
+    intro n' nd' nk
+    have hn' := le_of_dvd n0 nd'
+    refine'
+      have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k :=
+        lt_of_le_of_lt (Nat.sub_le_sub_right (Nat.sqrt_le_sqrt hn') _) (Nat.minFac_lemma n k h)
+      @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1)
+        (by simp [e, left_distrib]) fun m m2 d => _
+    cases' Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me ml
+    · subst me
+      contradiction
+    apply (Nat.eq_or_lt_of_le ml).resolve_left
+    intro me
+    rw [← me, e] at d
+    change 2 * (i + 2) ∣ n' at d
+    have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
+    rw [e] at this
+    exact absurd this (by linarith)
+  have pk : k ∣ n → Prime k := by
+    refine' fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) _⟩
+    exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)
+  split_ifs with dk dkk
+  · exact ⟨pk dk, (Nat.dvd_div_iff dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩
+  · 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
 #align nat.min_sq_fac_aux_has_prop Nat.minSqFacAux_has_prop
 
 theorem minSqFac_has_prop (n : ℕ) : MinSqFacProp n (minSqFac n) := by

Mathlib/Data/Nat/WithBot.lean

@@ -23,6 +23,10 @@ namespace Nat
 
 namespace WithBot
 
+instance : WellFoundedRelation (WithBot ℕ) where
+  rel := (· < ·)
+  wf := IsWellFounded.wf
+
 theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 := by
   rcases n, m with ⟨_ | _, _ | _⟩
   any_goals (exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩)

Mathlib/Data/Polynomial/Inductions.lean

@@ -116,7 +116,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' invImage PSigma.fst ⟨_, degree_lt_wf⟩
+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`

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -529,32 +529,30 @@ theorem IsCycle.swap_mul {α : Type _} [DecidableEq α] {f : Perm α} (hf : IsCy
     isCycle_swap_mul_aux₂ (i - 1) hy hi⟩
 #align equiv.perm.is_cycle.swap_mul Equiv.Perm.IsCycle.swap_mul
 
-theorem IsCycle.sign : ∀ {f : Perm α} (hf : IsCycle f), sign f = -(-1) ^ f.support.card
-  | f => fun hf =>
-    let ⟨x, hx⟩ := hf
-    calc
-      Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f)) := by
-        {rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]}
-      _ = -(-1) ^ f.support.card :=
-        if h1 : f (f x) = x then by
-          have h : swap x (f x) * f = 1 := by
-            simp only [mul_def, one_def]
-            rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
-          dsimp only
-          rw [sign_mul, sign_swap hx.1.symm, h, sign_one,
-            hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm]
-          rfl
-        else by
-          have h : card (support (swap x (f x) * f)) + 1 = card (support f) := by
-            rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
-              card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase]
-          have : card (support (swap x (f x) * f)) < card (support f) :=
-            card_support_swap_mul hx.1
-          dsimp only
-          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'
-  ⟨_, (measure fun f => f.support.card).wf ⟩
+theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ f.support.card :=
+  let ⟨x, hx⟩ := hf
+  calc
+    Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f)) := by
+      {rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]}
+    _ = -(-1) ^ f.support.card :=
+      if h1 : f (f x) = x then by
+        have h : swap x (f x) * f = 1 := by
+          simp only [mul_def, one_def]
+          rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
+        dsimp only
+        rw [sign_mul, sign_swap hx.1.symm, h, sign_one,
+          hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm]
+        rfl
+      else by
+        have h : card (support (swap x (f x) * f)) + 1 = card (support f) := by
+          rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
+            card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase]
+        have : card (support (swap x (f x) * f)) < card (support f) :=
+          card_support_swap_mul hx.1
+        dsimp only
+        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
 #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) :

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -820,7 +820,7 @@ protected noncomputable def inv.aux (a : R) (φ : MvPowerSeries σ R) : MvPowerS
     else
       -a *
         ∑ x in n.antidiagonal, if _ : x.2 < n then coeff R x.1 φ * inv.aux a φ x.2 else 0
-  termination_by' ⟨_, Finsupp.lt_wf σ⟩
+termination_by _ n => n
 #align mv_power_series.inv.aux MvPowerSeries.inv.aux
 
 theorem coeff_inv_aux [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) :

Mathlib/SetTheory/Lists.lean

@@ -359,7 +359,7 @@ instance : Setoid (Lists α) :=
 section Decidable
 
 /-- Auxiliary function to prove termination of decidability checking -/
-@[simp]
+@[simp, deprecated] -- porting note: replaced by termination_by
 def Equiv.decidableMeas :
     (PSum (Σ' _l₁ : Lists α, Lists α) <|
         PSum (Σ' _l₁ : Lists' α true, Lists' α true) (Σ' _a : Lists α, Lists' α true)) →
@@ -430,7 +430,11 @@ mutual
         mem.decidable a l₂
       refine' decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) _
       rw [← Lists'.mem_cons]; rfl
-end termination_by' ⟨_, InvImage.wf Equiv.decidableMeas Nat.lt_wfRel.wf⟩
+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

Mathlib/SetTheory/Ordinal/NaturalOps.lean

@@ -270,15 +270,14 @@ theorem blsub_nadd_of_mono {f : ∀ c < a ♯ b, Ordinal.{max u v}}
     apply mem_brange_self
 #align ordinal.blsub_nadd_of_mono Ordinal.blsub_nadd_of_mono
 
-theorem nadd_assoc : ∀ a b c, a ♯ b ♯ c = a ♯ (b ♯ c)
-  | a, b, c => by
-    rw [nadd_def a (b ♯ c), nadd_def, blsub_nadd_of_mono, blsub_nadd_of_mono, max_assoc]
-    · 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' PSigma.lex (inferInstance) (fun _ ↦ inferInstance)
-    -- Porting note: above lines replaces
-    -- decreasing_by solve_by_elim [PSigma.Lex.left, PSigma.Lex.right]
+theorem nadd_assoc (a b c) : a ♯ b ♯ c = a ♯ (b ♯ c) := by
+  rw [nadd_def a (b ♯ c), nadd_def, blsub_nadd_of_mono, blsub_nadd_of_mono, max_assoc]
+  · 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)
+-- Porting note: above lines replaces
+-- decreasing_by solve_by_elim [PSigma.Lex.left, PSigma.Lex.right]
 #align ordinal.nadd_assoc Ordinal.nadd_assoc
 
 @[simp]

Mathlib/SetTheory/ZFC/Basic.lean

@@ -1407,9 +1407,9 @@ theorem map_isFunc {f : ZFSet → ZFSet} [Definable 1 f] {x y : ZFSet} :
 
 /-- Given a predicate `p` on ZFC sets. `hereditarily p x` means that `x` has property `p` and the
 members of `x` are all `hereditarily p`. -/
-def Hereditarily (p : ZFSet → Prop) : ZFSet → Prop
-  | x => p x ∧ ∀ y ∈ x, Hereditarily p y
-termination_by' ⟨_, mem_wf⟩
+def Hereditarily (p : ZFSet → Prop) (x : ZFSet) : Prop :=
+  p x ∧ ∀ y ∈ x, Hereditarily p y
+termination_by _ => x
 #align Set.hereditarily ZFSet.Hereditarily
 
 section Hereditarily