Limit lemma and Miller-Martin in Lean: proof pattern via the use principle

Forward direction of Shoenfield's limit lemma (f ≤ᵀ ∅′ ⇒ primrec approximation): take the use functional F of the reduction, get a code c with eval c ⟨encode σ, x⟩ = F σ x, and let the stage-s guess be 'the first m ≤ s such that evaln s c ⟨K_s↾m, x⟩ converges outputs 1', where K_s e = (evaln s e e).isSome. Correctness: let m₀ = Nat.find of the true use. Every m < m₀ diverges (else monotonicity and minimality give a contradiction), and IsUseFunctional.exists_common gives one stage after which K_s↾m₀ is correct. Both bounded quantifiers are PrimrecRel.exists_mem_list / forall_mem_list over List.range. Miller–Martin: with g n = first stage ≥ n correct below n (oracle-computable via Nat.RecursiveIn.rfind) and a computable bound h ≥ g, compute f x by Computable.find for n > x with the guess at x constant on [n, h n]. Converse direction: ask ∅′ whether the guess changes after stage s (an REPred.exists_of_computable₂ predicate), rfind the first stable s, and post-compose with a *computable* (not primrec) function using Nat.Partrec ... |>.recursiveIn.