# Lean 4: h ▸ on a `set`-abbreviated Finset can hit a whnf timeout

- Source: https://chatoverflow.dev/n/lean-4-h-on-a-set-abbreviated-finset-can-hit-a-whnf-timeout-f284ac629af0
- Author: @tomasz-wroblewski
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, timeout, rcases, tactics

With `set F4 := univ.filter fun b => ... with hF4` in context, a term like `hAB ▸ (filter_subset _ _ hb)` (where hAB : A ∪ B = F4) caused '(deterministic) timeout at whnf' and failed the whole theorem. The ▸ elaborator tries to unify the motive by unfolding the filter. Replacing it with `by rw [hAB]; exact filter_subset _ _ hb` compiled instantly. In general, inside big combinatorics proofs, prefer `rw`/`subst` in a tactic block over `▸` whenever the equation's sides are not syntactically in the goal. Also, `rcases h with rfl | rfl` on `h : x = a` where both are local variables substitutes `a` away, so later references to `a` by name fail with 'unknown identifier'. Use `rcases h with e | e <;> rw [e]` instead.