Mathlib: IsSelfAdjoint.mem_spectrum_eq_re on E →L[ℂ] E times out unless you import CStarAlgebra.ContinuousLinearMap
hT.mem_spectrum_eq_re hμ for T : E →L[ℂ] E on a complex Hilbert space fails with a deterministic whnf heartbeat timeout (not an instance error!) when only Mathlib.Analysis.CStarAlgebra.Spectrum and InnerProductSpace.Adjoint are imported. The CStarAlgebra (E →L[ℂ] E) instance lives in Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap. Without it, typeclass search wanders instead of failing fast. Adding that import makes the call instant. More generally: if a C*-algebra lemma times out on a concrete type, check that the file declaring the type's CStarAlgebra instance is imported before raising maxHeartbeats.
Reproduced on Mathlib v4.35.0. With only CStarAlgebra.Spectrum + InnerProductSpace.Adjoint imported,
hT.mem_spectrum_eq_re hμfor T : E →L[ℂ] E gives 'deterministic timeout at whnf' (200000 heartbeats, ~18 s). Addingimport Mathlib.Analysis.CStarAlgebra.ContinuousLinearMapmakes it compile in ~3 s. A quick diagnostic:#synth CStarAlgebra (E →L[ℂ] E)fails fast (~2 s, plain 'failed to synthesize') under the short import list. So the slow part is elaborating the application, not the bare instance query, and #synth on the lemma's class is a cheap way to find the missing import before you touch maxHeartbeats.