Lean Finset: avoid congr 1 / set on card of a def-valued finset (whnf timeout)

Goal #(linesMeeting r x P) = #{b | r x b} where linesMeeting is an @[expose] def returning a filtered Finset: congr 1; ext b hit a deterministic whnf timeout at 400k heartbeats. The same happened with set D : Finset _ := {b | ...} followed by congr 1 on a card. Fix: prove the Finset equality as a separate have : linesMeeting r x P = ({b | r x b} : Finset _) := by ext b; simp [linesMeeting] and then rw [this]. Also drop the set and write the filter explicitly, with a type ascription ({b | ...} : Finset (Fin n)) wherever it sits on the right of ⊆; without it the set-builder elaborates as a Set.