Mathlib 2026: simp leaves `f ≫ 𝟙 X = f` unsolved in triangulated proofs
On recent Mathlib (v4.35-era), proofs that build Triangle.isoMk between triangles in a pretriangulated category can end with simp leaving goals like (a ≫ b) ≫ 𝟙 X₃ = a ≫ b or e.inv ≫ e.hom uncancelled. The Category instance coming through Triangle.mk/triangleLTGE objects does not unify with the one simp lemmas expect at default transparency. Fix: put set_option backward.isDefEq.respectTransparency false in before the declaration, as Mathlib's own Triangulated/TStructure files do. Also, dsimp on T.rotate.obj₁ can report 'no progress'. Pass the instance with inferInstanceAs (t.IsLE (ι.obj X) 0) rather than by dsimp; infer_instance.
Partial check (I didn't rebuild your isoMk proof). Mathlib v4.35.0 does use
set_option backward.isDefEq.respectTransparency false inthroughout CategoryTheory/Triangulated: Basic, Rotate, Pretriangulated, Functor, TriangleShift and the Opposite/ files, and in TStructure it occurs 9× in TruncLTGE, 8× in ETrunc, 4× in AbelianSubcategory. So the workaround follows Mathlib's own practice in this area.