ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>iso₁ : A.obj₁ ≅ B.obj₁<VAR>iso₂ : A.obj₂ ≅ B.obj₂<VAR>iso₃ : A.obj₃ ≅ B.obj₃<VAR>comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁ := by aesop_cat<VAR>comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂ := by aesop_cat<VAR>comm₃ : A.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃ := by aesop_cat<GOAL>(A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom = A.homMk B iso₁.hom iso₂.hom iso₃.hom comm₁ comm₂ comm₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>iso₁ : A.obj₁ ≅ B.obj₁<VAR>iso₂ : A.obj₂ ≅ B.obj₂<VAR>iso₃ : A.obj₃ ≅ B.obj₃<VAR>comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁ := by aesop_cat<VAR>comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂ := by aesop_cat<VAR>comm₃ : A.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃ := by aesop_cat<GOAL>(A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv = B.homMk A iso₁.inv iso₂.inv iso₃.inv ⋯ ⋯ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>f : A ⟶ B<VAR>h₁ : CategoryTheory.IsIso f.hom₁<VAR>h₂ : CategoryTheory.IsIso f.hom₂<VAR>h₃ : CategoryTheory.IsIso f.hom₃<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>e : A ≅ B<GOAL>e.hom.hom₁ ≫ e.inv.hom₁ = 𝟙 A.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>e : A ≅ B<GOAL>e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 A.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>e : A ≅ B<GOAL>e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 A.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>e : A ≅ B<GOAL>e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 B.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>e : A ≅ B<GOAL>e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>e : A ≅ B<GOAL>e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 B.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>h : A = B<GOAL>(CategoryTheory.eqToHom h).hom₁ = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>h : A = B<GOAL>(CategoryTheory.eqToHom h).hom₂ = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>h : A = B<GOAL>(CategoryTheory.eqToHom h).hom₃ = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).mor₁ = CategoryTheory.Limits.biprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).mor₃ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).mor₂ = CategoryTheory.Limits.biprod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).obj₂ = (X₁ ⊞ X₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).obj₃ = X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).obj₁ = X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).obj₂ = (X₁ ⨯ X₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).obj₃ = X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).mor₁ = CategoryTheory.Limits.prod.lift (𝟙 X₁) 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).mor₃ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).obj₁ = X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryProduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).mor₂ = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₃ = 𝟙 X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₁ = 𝟙 X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₁ = 𝟙 X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₂ = CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₂ = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X₁ X₂ : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂<GOAL>(CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₃ = 𝟙 X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<GOAL>(CategoryTheory.Pretriangulated.productTriangle T).mor₃ = (CategoryTheory.Limits.Pi.map fun j => (T j).mor₃) ≫ CategoryTheory.inv (CategoryTheory.Limits.piComparison (CategoryTheory.shiftFunctor C 1) fun j => (T j).obj₁)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<GOAL>(CategoryTheory.Pretriangulated.productTriangle T).mor₁ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<GOAL>(CategoryTheory.Pretriangulated.productTriangle T).mor₂ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<GOAL>(CategoryTheory.Pretriangulated.productTriangle T).obj₂ = ∏ᶜ fun j => (T j).obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<GOAL>(CategoryTheory.Pretriangulated.productTriangle T).obj₁ = ∏ᶜ fun j => (T j).obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<GOAL>(CategoryTheory.Pretriangulated.productTriangle T).obj₃ = ∏ᶜ fun j => (T j).obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<VAR>j : J<GOAL>(CategoryTheory.Pretriangulated.productTriangle.π T j).hom₁ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₁) j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<VAR>j : J<GOAL>(CategoryTheory.Pretriangulated.productTriangle.π T j).hom₂ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₂) j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<VAR>j : J<GOAL>(CategoryTheory.Pretriangulated.productTriangle.π T j).hom₃ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₃) j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<VAR>T' : CategoryTheory.Pretriangulated.Triangle C<VAR>φ : (j : J) → T' ⟶ T j<GOAL>(CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₁ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<VAR>T' : CategoryTheory.Pretriangulated.Triangle C<VAR>φ : (j : J) → T' ⟶ T j<GOAL>(CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₃ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<VAR>T' : CategoryTheory.Pretriangulated.Triangle C<VAR>φ : (j : J) → T' ⟶ T j<GOAL>(CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₂ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>h : ∀ (j : J), (T j).mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map (T j).mor₁ = 0<GOAL>(CategoryTheory.Pretriangulated.productTriangle T).mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map (CategoryTheory.Pretriangulated.productTriangle T).mor₁ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>(CategoryTheory.Pretriangulated.contractibleTriangleFunctor C).obj X = CategoryTheory.Pretriangulated.contractibleTriangle X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.contractibleTriangleFunctor C).map f).hom₃ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.contractibleTriangleFunctor C).map f).hom₁ = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.contractibleTriangleFunctor C).map f).hom₂ = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>CategoryTheory.Pretriangulated.Triangle.π₁.obj T = T.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), CategoryTheory.Pretriangulated.Triangle.π₁.map f = f.hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>CategoryTheory.Pretriangulated.Triangle.π₂.obj T = T.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), CategoryTheory.Pretriangulated.Triangle.π₂.map f = f.hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), CategoryTheory.Pretriangulated.Triangle.π₃.map f = f.hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>CategoryTheory.Pretriangulated.Triangle.π₃.obj T = T.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.rotate.obj₃ = (CategoryTheory.shiftFunctor C 1).obj T.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.rotate.mor₁ = T.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.rotate.mor₂ = T.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.rotate.mor₃ = -(CategoryTheory.shiftFunctor C 1).map T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.rotate.obj₁ = T.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.rotate.obj₂ = T.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.invRotate.mor₂ = T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.invRotate.mor₃ = T.mor₂ ≫ (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.invRotate.obj₁ = (CategoryTheory.shiftFunctor C (-1)).obj T.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.invRotate.obj₂ = T.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.invRotate.obj₃ = T.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T.invRotate.mor₁ = -(CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.rotate C).map f).hom₁ = f.hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.rotate C).obj T = T.rotate
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.rotate C).map f).hom₂ = f.hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.rotate C).map f).hom₃ = (CategoryTheory.shiftFunctor C 1).map f.hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.invRotate C).obj T = T.invRotate
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.invRotate C).map f).hom₁ = (CategoryTheory.shiftFunctor C (-1)).map f.hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.invRotate C).map f).hom₃ = f.hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.invRotate C).map f).hom₂ = f.hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₃ = 𝟙 X.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₂ = 𝟙 X.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₃ = 𝟙 X.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app X.obj₁