ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>n : ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCommShiftIso n).inv.app X).hom₂ = (F.commShiftIso n).inv.app X.obj₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleRotateIso.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleRotateIso.inv.app X).hom₃ = (F.commShiftIso 1).hom.app X.obj₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleRotateIso.hom.app X).hom₃ = (F.commShiftIso 1).inv.app X.obj₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleRotateIso.inv.app X).hom₁ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleRotateIso.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleRotateIso.hom.app X).hom₁ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleInvRotateIso.hom.app X).hom₁ = (F.commShiftIso (-1)).inv.app X.obj₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleInvRotateIso.inv.app X).hom₃ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleInvRotateIso.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₁)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleInvRotateIso.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₁)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleInvRotateIso.hom.app X).hom₃ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(F.mapTriangleInvRotateIso.inv.app X).hom₁ = (F.commShiftIso (-1)).hom.app X.obj₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIdIso C).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIdIso C).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIdIso C).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIdIso C).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIdIso C).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIdIso C).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.HasShift E ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>G : CategoryTheory.Functor D E<VAR>G.CommShift ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCompIso G).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₁))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.HasShift E ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>G : CategoryTheory.Functor D E<VAR>G.CommShift ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCompIso G).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₂))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.HasShift E ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>G : CategoryTheory.Functor D E<VAR>G.CommShift ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCompIso G).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₃))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.HasShift E ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>G : CategoryTheory.Functor D E<VAR>G.CommShift ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCompIso G).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₃))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.HasShift E ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>G : CategoryTheory.Functor D E<VAR>G.CommShift ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCompIso G).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₂))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.HasShift E ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>G : CategoryTheory.Functor D E<VAR>G.CommShift ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCompIso G).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₁))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<VAR>F₁.CommShift ℤ<VAR>F₂.CommShift ℤ<VAR>CategoryTheory.NatTrans.CommShift e.hom ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₂ = e.hom.app X.obj₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<VAR>F₁.CommShift ℤ<VAR>F₂.CommShift ℤ<VAR>CategoryTheory.NatTrans.CommShift e.hom ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₁ = e.inv.app X.obj₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<VAR>F₁.CommShift ℤ<VAR>F₂.CommShift ℤ<VAR>CategoryTheory.NatTrans.CommShift e.hom ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₂ = e.inv.app X.obj₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<VAR>F₁.CommShift ℤ<VAR>F₂.CommShift ℤ<VAR>CategoryTheory.NatTrans.CommShift e.hom ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₃ = e.inv.app X.obj₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<VAR>F₁.CommShift ℤ<VAR>F₂.CommShift ℤ<VAR>CategoryTheory.NatTrans.CommShift e.hom ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₃ = e.hom.app X.obj₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<VAR>F₁.CommShift ℤ<VAR>F₂.CommShift ℤ<VAR>CategoryTheory.NatTrans.CommShift e.hom ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₁ = e.hom.app X.obj₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>self : F.IsTriangulated<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>F.IsTriangulated<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<VAR>F₁.CommShift ℤ<VAR>F₂.CommShift ℤ<VAR>CategoryTheory.NatTrans.CommShift e.hom ℤ<VAR>F₁.IsTriangulated<GOAL>F₂.IsTriangulated
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<VAR>F₁.CommShift ℤ<VAR>F₂.CommShift ℤ<VAR>CategoryTheory.NatTrans.CommShift e.hom ℤ<GOAL>F₁.IsTriangulated ↔ F₂.IsTriangulated
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>F.IsTriangulated<VAR>F.mapArrow.EssSurj<VAR>T : CategoryTheory.Pretriangulated.Triangle D<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>∃ T', ∃ (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.HasShift E ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>G : CategoryTheory.Functor D E<VAR>G.CommShift ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasZeroObject E<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Preadditive E<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>CategoryTheory.Pretriangulated E<VAR>(F.comp G).IsTriangulated<VAR>F.IsTriangulated<VAR>F.mapArrow.EssSurj<GOAL>G.IsTriangulated
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.HasShift E ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>G : CategoryTheory.Functor D E<VAR>G.CommShift ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasZeroObject E<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Preadditive E<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>CategoryTheory.Pretriangulated E<VAR>H : CategoryTheory.Functor C E<VAR>e : F.comp G ≅ H<VAR>H.CommShift ℤ<VAR>H.IsTriangulated<VAR>F.IsTriangulated<VAR>F.mapArrow.EssSurj<VAR>CategoryTheory.NatTrans.CommShift e.hom ℤ<GOAL>G.IsTriangulated
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁<VAR>h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂<VAR>h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁<VAR>h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>F.IsTriangulated<GOAL>(h.map F).m₃ = F.map h.m₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁<VAR>h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂<VAR>h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁<VAR>h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>F.IsTriangulated<GOAL>(h.map F).m₁ = F.map h.m₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.Pretriangulated D<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>F.IsTriangulated<VAR>(F.mapComposableArrows 2).EssSurj<VAR>CategoryTheory.IsTriangulated C<GOAL>CategoryTheory.IsTriangulated D
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>X₁ : C₁<VAR>X₂ : C₂<VAR>X₃ : C₃<GOAL>((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).obj X₃ = (G.obj ((F₁₂.obj X₁).obj X₂)).obj X₃
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>X₁ : C₁<VAR>X₂ Y₂ : C₂<VAR>φ : X₂ ⟶ Y₂<VAR>X₃ : C₃<GOAL>((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).map φ).app X₃ = (G.map ((F₁₂.obj X₁).map φ)).app X₃