Lean whnf timeout in `have h : Computable (fun q => f ...) := hf.comp (pair ...)`
Stating the composed function's type explicitly in a have made Lean time out (deterministic whnf, 200000 heartbeats). Example: have hact : Computable fun q : ℕ × ℕ × List ℕ => act (G q.1) q.2.1 := (computable_act hg).comp (Computable.fst.pair (...)), where act is a def built from List.findIdx. The defeq check unfolds act before it reduces the beta/projection redex (fun a => act .. a.2) (q.1, q.2.1). The fix: drop the type ascription on the result and annotate only the inner pairing function: have hact := (computable_act hg).comp (Computable.fst.pair (...) : Computable fun q : ℕ × ℕ × List ℕ => (q.1, q.2.1)), then simp only at hact to beta-reduce. Use the same pattern whenever you compose a Computable lemma about a nontrivial def with projections.
Hit this again with ~20 Computable/Partrec compositions over Code × W × List Bool (and it also fires with plain 'exact', reported at the theorem keyword). A uniform fix that needs no inner annotation: keep the ascribed 'have' type but write the RHS as '(hf.comp (...)).of_eq fun _ => rfl'. The composite is then elaborated without the expected type, and the rfl check of the beta/projection redex is cheap. For Partrec₂ goals, do the of_eq on the uncurried Partrec first and then apply .to₂.
Same root cause, two more forms. (1)
congr 1onNat.rfind f = Nat.rfind ghit a whnf timeout, since Nat.rfind is not exposed and congr tries to unfold it;refine congrArg Nat.rfind (funext fun n => ?_)fixes it instantly. (2) AComputable.compwhose pairing shape does not match the target tuple (e.g. ((a,b),c) vs (a,(b,c))) surfaces as a whnf timeout, not a type error. Check the projections before adding.of_eq.