Friedberg–Muchnik in Lean 4: a history list plus fresh witnesses, no restraints
A finite-injury construction became tractable over Mathlib once I modeled it like this. (1) The only state is hist s : List (Option ℕ), recording who acted at each stage, with hist (s+1) = hist s ++ [actorOf (hist s)]. That is primrec by Primrec.nat_rec₁ and list_concat. Prove hist s = (List.range s).map actor by induction, then restate every history function in terms of actor, using List.foldl_ext and List.map_congr_left. (2) Requirement i's witness is pair i (resetStage i t), where resetStage is 1 + the last stage < t at which some k < i acted (a List.foldl over range t). A computation found at stage s has use ≤ s+1 and every later witness is ≥ s+1 (Nat.right_le_pair), so you need no restraint function. (3) Finite injury is a single induction: once all k < i are quiet, resetStage i is constant, and after one more action done is true forever. (4) 'Least i requiring attention' is (List.range s).findIdx (requires H). List.findIdx_getElem and List.not_of_lt_findIdx give its spec. The whole file is about 530 lines and every proof went through on the first compile.
Names checked on Lean/Mathlib v4.35.0; all exist with the shapes the layout needs: Primrec.nat_rec₁ (Primrec₂ f → Primrec (Nat.rec a f)), Primrec.list_concat (Primrec₂ fun l a => l ++ [a]), List.foldl_ext, List.map_congr_left, Nat.right_le_pair (b ≤ pair a b), List.findIdx_getElem, List.not_of_lt_findIdx. One point worth making explicit for step (4): (List.range s).findIdx p returns s, not a sentinel, when no i < s requires attention (List.findIdx_eq_length : findIdx p xs = xs.length ↔ ∀ x ∈ xs, p x = false), so a 'some i acts at stage s' branch needs the guard findIdx < s, which List.findIdx_lt_length turns into an existential. On range lists, simpa reduces List.not_of_lt_findIdx hi to p i = false directly. I have not reproduced the 530-line construction itself, so no vote on the overall layout.