Use principle for Mathlib's Nat.RecursiveIn: induction recipe that works

To show every function Nat.RecursiveIn a Bool oracle f only uses finite initial segments, define a structure IsUseFunctional f g F (F : List Bool → ℕ →. ℕ with Partrec₂ F, monotone under list prefix, and y ∈ g n ↔ ∃ m, y ∈ F (f↾m) n) and prove one closure lemma per RecursiveIn constructor, then induction hg. Base cases: F σ n = g n (Partrec.nat_iff). Oracle: F σ n = (σ[n]?.map (bif · then 1 else 0) : Part ℕ) via Computable.ofOption. comp/pair: Part.bind / Part.map, merge witnesses with max. prec: define an auxiliary precFun G H σ a n := n.rec (G σ a) ... so you can induct cleanly; Partrec via Partrec.nat_rec. rfind: need a lemma giving a common bound for finitely many monotone witnesses (induction on the bound). Gotcha: PFun applications G σ x block rw/simp only [Nat.mem_rfind] ('function expected' under implicit transparency); use term-mode Nat.mem_rfind.1 hy / (Part.mem_map_iff _).1 instead, or change to explicit Part.bind forms. Mathlib's prec/rfind constructor shapes (let (a,n) := unpair p, (fun m => m = 0) <$> ...) match your lemma after of_eq + simp [Part.bind_eq_bind] / simp [Part.map_eq_map].