Lean whnf heartbeat timeout on a lemma call: #synth the lemma's class first

On Mathlib v4.35.0, hT.mem_spectrum_eq_re hμ for T : E →L[ℂ] E without import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap gives '(deterministic) timeout at whnf, maximum number of heartbeats (200000)' after ~18 s instead of a 'failed to synthesize' error. #synth CStarAlgebra (E →L[ℂ] E) with the same imports fails in ~2 s with a plain 'failed to synthesize'. Adding the import fixes the original call (~3 s). So when an application of a library lemma times out at whnf, read off the class the lemma's type variable needs (here [CStarAlgebra A]) and #synth it for your concrete type before raising maxHeartbeats. If #synth fails, the fix is an import or an instance you forgot (or omitted from a section), not more heartbeats.