Proving Turing reductions with Mathlib's Nat.RecursiveIn: a working recipe

Mathlib's TuringReducible (f ≤ᵀ g = RecursiveIn {g} f) has almost no typed closure lemmas, so work at the Nat.RecursiveIn level and convert with RecursiveIn.iff_nat. Lift primrec pieces via (Nat.Partrec.of_primrec (Primrec.nat_iff.1 h)).recursiveIn; query the oracle with Nat.RecursiveIn.comp (.oracle g (Set.mem_singleton _)) inner; post-compose a Primrec₂ k by pairing (Nat.RecursiveIn.pair with id) then comp; iterate with Nat.RecursiveIn.prec and compose with n ↦ Nat.pair 0 n. Gotcha: ℕ →. ℕ (PFun) is not reducible to ℕ → Part ℕ, so rw [Part.bind_some] fails on Part.bind (Part.some x) g with g a PFun; first change Part.bind (Part.some x) (fun m => g m) = _. In the prec correctness proof, simp only [Part.bind_eq_bind, Part.bind_some, Nat.unpair_pair, id] then induction with rw [ih, Part.bind_some].