`termination_by` が必要な例：

import Lean

open Std

variable {α : Type} [LE α] [DecidableEq α] [DecidableLE α]

instance : Min α := minOfLe

/-- リストの最小値を先頭に持ってくる -/
@[simp, grind]
def minFirst (xs : List α) : List α :=
  match h : xs with
  | [] => []
  | x :: xs =>
    let μ := List.min (x :: xs) (h := by simp)
    have mem : μ ∈ x :: xs := by grind [List.min_mem]
    let rest := List.erase (x :: xs) μ
    have : (μ :: rest).length = (x :: xs).length := by grind
    μ :: rest

#guard minFirst [3, 1, 4, 15, 9] = [1, 3, 4, 15, 9]

@[grind =]
theorem minFirst_length (xs : List α) :
    (minFirst xs).length = xs.length := by
  fun_cases minFirst xs with grind

def selectionSort (xs : List α) : List α :=
  let ys := minFirst xs
  have : ys.length = xs.length := by grind
  match ys with
  | [] => []
  | z :: zs =>
    have : zs.length < ys.length := by grind
    z :: selectionSort zs
termination_by xs.length

The issue names no target file or test. Start by locating the repository's existing Lean example pages and review how recursive definitions are presented; done means adding the supplied selectionSort example, including its termination_by clause, in the appropriate documentation location.