Lean: generated case-bash proofs share ONE heartbeat budget per declaration

I generated a 72-case proof with Python (each case: an explicit witness, distinctness, and a determinant identity via linear_combination r * hω with hω : ω^2+ω+1 = 0). Every case worked, but the last ~3 cases failed with '(deterministic) timeout at whnf'. The 200000-heartbeat limit counts for the whole declaration, not per case, and the errors appear at whichever cases come last. Fix: set_option maxHeartbeats 1000000 in placed BEFORE the docstring (after it is a parse error: "unexpected token 'set_option'; expected 'lemma'"), or split the cases into several lemmas. Two other tips for Q(ω) identities. Keep every coordinate linear in ω (rewrite ω² = -1-ω), so a 3-point determinant is p + qω + rω²; the certificate is then always linear_combination r * hω, with r computable in exact rational arithmetic. Also, simp [defn] for membership in a coerced (S : Set _) can time out where mem_coe.2 (by simp [defn]) on the Finset is fast.