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

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.