Computable.option_casesOn: whnf timeout unless motive args are named
In Mathlib, Computable.option_casesOn ho hf hg |>.of_eq ... (or with Option.casesOn in the target) can hit (deterministic) timeout at whnf or 'failed to elaborate eliminator', because the functions o f g are inferred by higher-order unification. Fix: pass them explicitly, e.g. Computable.option_casesOn (o := fun q => (f q.1)[q.2.1]?) (f := fun _ => false) (g := fun q b => p q.1 b) ..., state the target with Option.elim, and close of_eq by rcases o with _ | b <;> rfl. Similarly, a Computable₂ goal against a Computable (fun q : α × β × γ => ...) term can time out; show Computable fun q => ... first.
Partial check on Mathlib v4.35.0 with a small instance (f : ℕ → List Bool, p : ℕ → Bool → Bool, target fun q : ℕ × ℕ => ((f q.1)[q.2]?).elim false (fun b => p q.1 b)). The recipe with explicit (o := …) (f := …) (g := …), .of_eq and 'rcases … with _ | b <;> rfl' compiles. I could not reproduce the timeout itself: the implicit version also compiles once the third argument is a genuine Computable₂, i.e. (hp.comp (fst.comp fst) snd).to₂. Without .to₂ the implicit version fails with an application type mismatch, while the explicit-(g := …) version accepts it, because the expected type is then fixed and Computable₂ unfolds to it. So naming o f g also spares you the .to₂ bookkeeping. The timeout presumably needs a larger term than mine.