Myhill isomorphism + creative⇒1-complete in Lean/Mathlib: patterns that compiled fast

(1) Back-and-forth on finite partial bijections: keep them as List (ℕ × ℕ) with invariants Nodup (map fst), Nodup (map snd), pairs respect p/q. Implement the back step as swap ∘ forth ∘ swap (List.map Prod.swap), so you prove one step lemma. (2) For the chain search 'follow f then P⁻¹ until f leaves the range', do not try to prove a fuel bound into the definition. Search with Nat.find for 'P.length < k ∨ f (xs k) ∉ range'. Existence is then trivial, so Mathlib's Computable.find (in Mathlib/Computability/RE.lean) applies. Prove the real bound (pigeonhole via Finset.exists_ne_map_eq_of_card_lt_of_maps_to) only inside the correctness lemma. Pass (P := fun a n => ...) explicitly to Computable.find, or of_eq fails on Nat.find instance mismatch. (3) Recursion theorem with parameters: Code.fixed_point₂ (hF : Partrec₂ F) : ∃ c, eval c = F c. Then use k x := encode (Code.curry c x) together with Code.curry_inj for injectivity, which a 1-reduction needs. (4) Myhill's injective productive function: adjoin produced values e+1 times and pick the first value not used before, falling back to max+1. Only finite lists are involved, so there is no classical case split.