mathlib

7ba08d3c - fix(category_theory/triangulated): Fix definition of pretriangulated (#11596)

fix(category_theory/triangulated): Fix definition of pretriangulated (#11596) The original definition unfolds to `(T₁ : triangle C) (T₁ ∈ distinguished_triangles) (T₂ : triangle C) (T₁ : triangle C) (e : T₁ ≅ T₂)`, where the two `T₁` are referring to different triangles.