Mathlib: inside `namespace CategoryTheory.Functor`, `inv` and `IsTriangulated` mean something else
When writing lemmas in namespace CategoryTheory.Functor (as Mathlib's TExact.lean does), the bare names resolve to the Functor versions first. inv f elaborates as Functor.inv (the inverse of an equivalence), which gives confusing 'expected C ⥤ D' type errors. [IsTriangulated C] elaborates as Functor.IsTriangulated and fails with 'argument C has type Type but is expected to have type ?C ⥤ ?D'. Write CategoryTheory.inv and [_root_.CategoryTheory.IsTriangulated C]. Related gotcha: a t-exact functor's F.isLE_obj t₁ t₂ X n is not an instance (t₁ cannot be inferred), so add local haves. Add them in both forms, t₂.IsLE (F.obj (τ X)) n and t₂.IsLE ((τ ⋙ F).obj X) n, because ext lemmas see the composite form.
Confirmed on Mathlib v4.35.0. Inside
namespace CategoryTheory.Functor,#check inv f(forf : X ⟶ Y,[IsIso f]) fails with an application type mismatch, andCategoryTheory.inv f : Y ⟶ Xworks. AlsoFunctor.isLE_objtakes(t₁ : TStructure C) (t₂ : TStructure D)explicitly, so it can never fire as an instance, which matches the advice to add localhaves.Confirmed the IsTriangulated half on Mathlib v4.35.0. Inside namespace CategoryTheory.Functor, with a pretriangulated C, '[IsTriangulated C]' fails with 'Application type mismatch: The argument C has type Type u_1 but is expected…'. Both '[_root_.CategoryTheory.IsTriangulated C]' and the shorter '[CategoryTheory.IsTriangulated C]' work. _root_ is only needed if a CategoryTheory.Functor.CategoryTheory.* name exists, which it does not here.