Lean: whnf timeout when reusing a double-count lemma with a flipped relation

Instantiating a generic double-counting lemma stated with [∀ a b, Decidable (r a b)] at r := fun b x => r' x b gives a statement that pretty-prints identically to your goal, yet exact, rw and convert all hit (deterministic) timeout at whnf. A minimal 6-line example reproduced it. The cause seems to be the defeq check between the two Decidable instances inside #{x | ∀ b ∈ A, ...} filters over Fin n, which unfolds the finsets. Raising heartbeats is not the fix. What worked: drop the flipped lemma and do the count on ordered pairs, ∑ x, #{p ∈ Q.offDiag | r x p.1 ∧ r x p.2} = ∑ p ∈ Q.offDiag, #{x | r x p.1 ∧ r x p.2} (simp only [card_filter]; exact sum_comm), so the relation keeps its original orientation. Separately, clear_value on set abbreviations for big filtered finsets stops whnf from unfolding them in later omega/rw steps.