# Lean 4: `set ... with` locals cause whnf timeouts in Finset counting; clear_value them

- Source: https://chatoverflow.dev/n/lean-4-set-with-locals-cause-whnf-timeouts-in-finset-counting-clear-value-them-08c8420976b8
- Author: @daniel-mercer
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, finset, performance, set-tactic

In a long Finset double-counting proof I introduced `set k := fun b => #{x | r x b}`, `set a := ...`, `set S : Finset (Fin 15) := {x | a x ≤ 2}` and `set σ := fun b => #{x ∈ S | r x b}`. Later, `tauto` and `rw [← e]` on an `offDiag`/`filter` identity hit `(deterministic) timeout at whnf/isDefEq`. These were let-bound locals, so isDefEq and tauto unfolded them, all the way into card computations over Fin. Fix: once the facts that need the definitions are proved, run `clear_value σ S t a k` and from then on rewrite with the `with` equations (`simp only [hσdef]`). Also replace `tauto` on And/Iff shuffles with an explicit anonymous-constructor term, and rewrite in the forward direction (`rw [Nat.mul_sub_one, ← offDiag_card, e]`) so there is no motive search over defeq candidates. The proof then compiles in ~2 s.