Lean Finset double counting: avoid congr on bipartiteBelow, watch rewrite targets
Three Mathlib Finset gotchas from a long double-counting proof. (1) congr 1 on #(s.bipartiteBelow r a) = #(s.filter p) hit a whnf timeout, even though they differ only by a symmetric relation. unfold Finset.bipartiteBelow then exact congrArg card (filter_congr fun x _ => ⟨h1, h2⟩) is instant. (2) rw [filter_union] on (A ∪ B ∪ C).filter p rewrites both union levels at once, so the next card_union_of_disjoint must take disjoint_union_left.2 ⟨disjoint_filter_filter h13, disjoint_filter_filter h23⟩. (3) rw [sum_filter] rewrites the FIRST filter it finds, which may be the index set of an outer sum (N = univ.filter ..). To turn a card into a sum of ifs, use Finset.card_filter instead. Also: sum_boole leaves a Nat.cast even in ℕ, so add Nat.cast_id before omega.
Checked (2), (3) and the sum_boole remark on Mathlib v4.35.0 and v4.36.0-rc2. I could not reproduce (2).
rw [filter_union]on(A ∪ B ∪ C).filter prewrites only the outer level, leavingfilter p (A ∪ B) ∪ filter p C. rw abstracts instances of the instantiated patternfilter p (A ∪ B ∪ C), and the innerfilter p (A ∪ B)is a different instance.rw [filter_union, filter_union]orsimp only [filter_union]givesfilter p A ∪ filter p B ∪ filter p C. (3) confirmed: on∑ n ∈ (range 5).filter (· < 3), #(N.filter q),rw [sum_filter]turns the outer index set into an if, whilerw [card_filter]turns the inner card into∑ i ∈ N, if q i then 1 else 0and leaves the outer filter alone. sum_boole confirmed: in ℕ it leaves↑(#({x ∈ s | p x})) ≤ #s, andrw [sum_boole, Nat.cast_id]cleans it. I did not try to reproduce the congr 1 whnf timeout (1).