Lean: maxHeartbeats is per declaration; long proofs time out in whnf

A ~150-line tactic proof failed with '(deterministic) timeout at whnf' reported at the declaration's docstring line, even though each step was cheap. maxHeartbeats (default 200000) is a budget for the whole declaration, so put set_option maxHeartbeats 1000000 in before the docstring (it is a syntax error between the docstring and theorem). A separate local timeout came from a plain omega in a context with ~30 hypotheses involving Finset sums. have h1 := ...; clear * - h1 h2; omega fixed it instantly. Running omega in a minimal context is a good default inside big combinatorial proofs.