feat: avoid termination_by', introduce WellFounded.wrap

I’d like to remove support for the `termination_by'` annotation. Until
leanprover-community#371 it wasn't used anywhere in
lean, std, mathlib, so this PR removes the single use of it.

It does so using the pattern that can be used to replace uses of
`termination_by'`, should there be more: Using the helper type
`WellFounded.Wrap` one can indicate an explicit `WellFounded` relation
to use.

So this PR uses that pattern to avoid the use of `termination_by'` here,
and at the same time provides the necessary definitions for others, so
when Lean drops support for `termination_by'`
(leanprover/lean4#3033), we can tell users how
migrate.

Std/WF.lean

@@ -90,6 +90,24 @@ end Acc
 
 namespace WellFounded
 
+/-- A wrapper type with an `WellFoundedRelation` instance that allows you to explicitly
+indicate the `WellFounded` relation to use in a `termination_by` clause. See `WellFounded.wrap` -/
+def Wrapped {α : Sort u} {r : α → α → Prop} (_h : WellFounded r) := α
+
+instance : WellFoundedRelation (Wrapped h) := invImage id ⟨_, h⟩
+
+/-- Wraps a value in `WellFounded.Wrapper` to indicate that this `WellFounded` relation
+should be used.
+
+Example usage:
+```
+def otherWF : WellFounded Nat := …
+def foo (n : Nat) := …
+termination_by foo n => otherWF.wrap n
+```
+-/
+def wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : h.Wrapped := x
+
 /-- A computable version of `WellFounded.fixF`.
 Workaround until Lean has native support for this. -/
 @[inline] private def fixFC {α : Sort u} {r : α → α → Prop}
@@ -105,7 +123,7 @@ Workaround until Lean has native support for this. -/
 @[specialize] private def fixC {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
     (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
   F x (fun y _ => fixC hwf F y)
-termination_by' ⟨r, hwf⟩
+termination_by _ x => hwf.wrap x
 
 @[csimp] private theorem fix_eq_fixC : @fix = @fixC := rfl