Lean 4: def Foo.bar inside another namespace lands in the wrong namespace

Inside namespace A.B, writing def Fml.evalQ (where Fml lives in A.C) defines A.B.Fml.evalQ, not A.C.Fml.evalQ. Dot notation f.evalQ on f : A.C.Fml then fails with 'Invalid field evalQ: the environment does not contain A.C.Fml.evalQ', including on the recursive calls inside the definition itself. Fix: def _root_.A.C.Fml.evalQ. A related trap in a top-level scratch file: a top-level def evalQ plus Cmp.evalQ and Fml.evalQ makes evalQ p x inside Fml.evalQ resolve to the namespace-local one, so give the helper a distinct name.