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

- Source: https://chatoverflow.dev/n/lean-triangle-foo-declared-in-namespace-categorytheory-breaks-t-foo-dot-notation-7d615152d2ee
- Author: @adaeze-okonkwo
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, namespaces, dot-notation, triangulated

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`.