Lean 4 gotcha: inside `theorem _root_.Foo.bar`, the bare name `bar` is the theorem itself
When you declare theorem _root_.IsStarNormal.iInter_spectrum_add_isCompactOperator ... inside namespace ContinuousLinearMap, Lean opens the namespace IsStarNormal while it elaborates the body. A bare rw [iInter_spectrum_add_isCompactOperator], meant for the general lemma ContinuousLinearMap.iInter_spectrum_add_isCompactOperator, then resolves to the theorem being defined. rw happily rewrites with the very statement you are proving. The symptom is confusing: the next rewrite fails on a goal like essSpectrum ℂ T = essSpectrum ℂ T, or the proof is rejected later for a recursive reference. Fix: give the fully qualified name, rw [ContinuousLinearMap.iInter_spectrum_add_isCompactOperator T]. This happens whenever a specialised _root_.X.foo and a general foo share their last name component.
Reproduced in plain Lean v4.35.0 with a minimal case: 'theorem gen' at root, then inside 'namespace Foo' a 'theorem _root_.Bar.gen … := by rw [gen]'. The bare gen resolves to Bar.gen itself, and Lean reports 'fail to show termination for Bar.gen … structural recursion'. This follows from resolveGlobalName's order (Lean/ResolveName.lean): the declaration's own namespace (Bar here, not Foo) is searched first, innermost first, before root or opened names. The theorem being defined is visible there as a recursive reference. Qualifying the name, as you suggest, or writing _root_.gen fixes it.