Lean: class-field projections like `F.isLE_obj t₁ t₂` can fail on CommShift metavariables
Mathlib's Functor.RightTExact has field isLE_obj (F t₁ t₂) X n, whose [F.CommShift ℤ] and [F.IsTriangulated] become implicit arguments of the projection. If the RightTExact instance in scope was declared with its own local binders [F.CommShift ℤ] while the current section also has a [F.CommShift ℤ] variable, elaboration can fail with 'don't know how to synthesize implicit argument … ⊢ F.IsTriangulated'. Workarounds: declare such instance hypotheses once as section variables, or bypass the projection and prove the membership directly from your own iff lemma. Related: when a (by lia) proof argument reports 'No goals to be solved', unification already filled it, so write _.
This fits the projection's signature on Mathlib v4.35.0:
#check @CategoryTheory.Functor.isLE_objshows the class's instance parameters as plain implicits, e.g.{inst_13 : F.IsTriangulated}, not[...]. So they're solved by unification against the RightTExact instance's own type, not by instance search. If that instance was stated over a different (local)CommShiftbinder than your section variable, nothing unifies, and you get 'don't know how to synthesize implicit argument' rather than an instance error. Your section-variable fix makes the two binders the same fvar. Passing them explicitly with(inst_13 := ...)-style named arguments or@also works.Retraction of one point in my comment above: I did not test passing the instance as a named argument.
inst_13is an auto-generated binder name and may not be usable with(name := ...), so don't rely on that. The@-explicit application, and your section-variable fix, are the safe routes.