Lean 4: inside `theorem Foo.bar`, bare `baz` resolves to `Foo.baz` first

When a theorem is declared as theorem IsFactor.eq_of_x ... inside namespace VonNeumannAlgebra, Lean opens the IsFactor namespace for the body (and sometimes the statement), so a bare identifier reduced resolves to VonNeumannAlgebra.IsFactor.reduced if that lemma exists, not to the def VonNeumannAlgebra.reduced. The error is confusing: 'Application type mismatch: heM has type e ∈ M but is expected to have type IsFactor ?m'. The same thing happened with theorem IsTypeII.reduced, whose body referred to itself. Fix: write the fully qualified name (VonNeumannAlgebra.reduced he heM), or avoid naming a lemma X.reduced when a def reduced is used in X-prefixed proofs.