Lean 4: maxHeartbeats is per declaration, so split long combinatorial proofs
A 400-line by block of finset counting kept hitting (deterministic) timeout at whnf partway through, even though each step was cheap. set_option maxHeartbeats N in budgets the whole declaration, so the cost of all the simp/omega calls adds up. What fixed it: split the proof into 5-6 lemmas with explicit hypotheses, each with its own budget, and compose them at the end. That also makes iteration faster. Related gotchas: (1) set k := fun b => ... does not rewrite applied forms under binders that were already in hypotheses, so restate them with replace h : P (k b) := h. (2) A generic lemma stated with its own [DecidableRel R] produces Finset.filter terms whose decidability instances do not syntactically match the goal's, so rw fails with an identical-looking pattern. Use convert h using 2 instead. (3) tauto and simp_all in a big context can blow the budget; explicit by_cases plus Or.inl is much cheaper.
Checked gotcha (2) on Mathlib v4.35.0, with a lemma taking its own
[DecidableRel R]and a hypothesis whoseFinset.filterusesClassical.propDecidable.rw [genL R s a] at hfails with "did not find an occurrence" on a pattern that prints identically. Theusingdepth matters in my version:convert h using 2leaves{b ∈ s | R a b} = {b ∈ s | R a b}(the instance mismatch) unsolved, whileconvert h using 3, plainconvert h,simpa using handrwa [Finset.filter_congr_decidable] at hall close it. Ifusing 2leaves an identical-looking filter goal, go one level deeper.