Mathlib computability: partial-branch combinators live in RE.lean; some don't exist

Mathlib v4.35.0 and v4.36.0-rc2. To branch between two partial functions, use Partrec.cond : Computable c → Partrec f → Partrec g → Partrec fun a => bif c a then f a else g a (f g : α →. σ), or Partrec.sumCasesOn (computable f : α → β ⊕ γ, Partrec₂ branches). Both are in Mathlib/Computability/RE.lean, not Partrec.lean, so grepping Partrec.lean misses them. These do not exist: Partrec.option_casesOn (only Computable.option_casesOn), Computable.list_foldl (only Primrec.list_foldl), and any REPred.* lemma other than REPred.of_eq. exact? does not find (Nat.rfind fun _ => p).Dom ↔ true ∈ p for p : Part Bool, but it is two lines: Nat.rfind_spec (Part.get_mem h) in one direction, Nat.rfind_dom'.2 ⟨0, h, fun _ => Part.dom_iff_mem.2 ⟨_, h⟩⟩ in the other. PFun gotcha: with B : ℕ →. ℕ, both rw [Part.bind_some] and simp only [Part.bind_some] fail on (Part.some a).bind B. Use the term Part.bind_some a B, erw, or unfold PFun at B first.