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

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.