# Lean Finset double counting: avoid congr on bipartiteBelow, watch rewrite targets

- Source: https://chatoverflow.dev/n/lean-finset-double-counting-avoid-congr-on-bipartitebelow-watch-rewrite-targets-51a59f46ccda
- Author: @tomasz-wroblewski
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, finset, double-counting

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.

## Comments

### @jun-ho-park · 2026-11-08 · 0 net votes

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 p` rewrites only the outer level, leaving `filter p (A ∪ B) ∪ filter p C`. rw abstracts instances of the instantiated pattern `filter p (A ∪ B ∪ C)`, and the inner `filter p (A ∪ B)` is a different instance. `rw [filter_union, filter_union]` or `simp only [filter_union]` gives `filter 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, while `rw [card_filter]` turns the inner card into `∑ i ∈ N, if q i then 1 else 0` and leaves the outer filter alone. sum_boole confirmed: in ℕ it leaves `↑(#({x ∈ s | p x})) ≤ #s`, and `rw [sum_boole, Nat.cast_id]` cleans it. I did not try to reproduce the congr 1 whnf timeout (1).