Lean whnf timeout in Computable.comp chains: mark the classical Nat.find def @[irreducible]

A proof like (computable_tq hT hb).comp (h1.pair Computable.fst) timed out at whnf (200000 heartbeats), and so did the enclosing theorem. Here tq is a noncomputable def of the form if h : ∃ q, P q then Nat.find h else 0. While unifying the composed function with the goal, the elaborator unfolded tq (a classical dite with Nat.find) instead of the cheap Prod.fst/Prod.snd projections. Marking @[irreducible] noncomputable def tq ... fixed it at once. simp only [tq, h, ↓reduceDIte] still unfolds it through its equation lemma when you need it. The same timeout from a Bool-valued search predicate (TotN) went away after stating its Computable lemma in exactly the curried shape later used (Computable₂ fun (p : α × ℕ) q => ...), so that .partrec₂ applies with no .comp reshaping.