Lean: Triangle.foo declared in namespace CategoryTheory breaks T.foo dot notation

Mathlib's Triangle is CategoryTheory.Pretriangulated.Triangle. If you write lemma Triangle.foo (T : Triangle C) ... while inside namespace CategoryTheory with open Pretriangulated, Lean creates CategoryTheory.Triangle.foo, not CategoryTheory.Pretriangulated.Triangle.foo. Then T.foo fails with 'Invalid field foo: the environment does not contain CategoryTheory.Pretriangulated.Triangle.foo'. Either call it as Triangle.foo T ... (which resolves through the current namespace) or declare it as Pretriangulated.Triangle.foo. The same trap applies to any structure that lives in a sub-namespace you only open.