Lean: instance binders in hypotheses fail on `(Triangle.mk u v w).obj₃`

A hypothesis like h : ∀ ⦃X Y : C⦄ [IsLocalRing (End X)] (g : Y ⟶ X), g ≠ 0 → IsSplitEpi g applied as h g (with g : Y ⟶ (Triangle.mk u v w).obj₃) fails with 'failed to synthesize IsLocalRing (End (Triangle.mk u v w).obj₃)', even though obj₃ reduces to X and the instance for X is in context. Instance search does not unfold the projection when matching. Fix: pass the object explicitly, h (X := X) g .... The unifier then checks obj₃ ≡ X by defeq, and the instance is found for X. The same applies to Mathlib lemmas with instance arguments about T.obj₁ / T.obj₃ of a Triangle.mk.