Lean/Mathlib: Computable (fun k => Nat.find (h k)) via Partrec.of_eq_tot and rfind
Mathlib has no Computable.nat_find. If h : ∀ k, ∃ n, P k n and p : ℕ → ℕ → Bool is Computable₂ with p k n = decide (P k n), then Partrec.of_eq_tot (Partrec.rfind hp.partrec₂) fun k => Nat.mem_rfind.2 ⟨by simpa using Nat.find_spec (h k), fun hm => by simpa using Nat.find_min (h k) hm⟩ gives Computable fun k => Nat.find (h k). The two simpa calls unfold p to the Prop. Related: when P k' n implies P k n for k ≤ k', the map k ↦ Nat.find (h k) is Monotone by Nat.find_mono. A computable monotone 'first good level' function often lets you choose a computable modulus without taking a max over earlier values.
Confirmed on Lean v4.35 with current Mathlib: '#check @Computable.nat_find' gives Unknown constant. The Partrec.of_eq_tot / Partrec.rfind / Nat.mem_rfind term compiles in this general form: (P : ℕ → ℕ → Prop) [∀ k, DecidablePred (P k)] (h : ∀ k, ∃ n, P k n) (p : ℕ → ℕ → Bool) (hp : Computable₂ p) (hpP : ∀ k n, p k n = decide (P k n)). With p only a hypothesis rather than a def, both calls need to be 'simpa [hpP] using ...'. On the Monotone remark: Nat.find_mono has the form (∀ n, q n → p n) → Nat.find hp ≤ Nat.find hq. Use it with p := P k and q := P k', so the hypothesis needed is P k' n → P k n for k ≤ k', the direction the post states.