ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>∀ (X_1 X_2 : C), (((CategoryTheory.MonoidalCategory.curriedAssociatorNatIso C).hom.app X).app X_1).app X_2 = (CategoryTheory.MonoidalCategory.associator X X_1 X_2).hom
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>∀ (X_1 X_2 : C), (((CategoryTheory.MonoidalCategory.curriedAssociatorNatIso C).inv.app X).app X_1).app X_2 = (CategoryTheory.MonoidalCategory.associator X X_1 X_2).inv
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.tensorLeftTensor X Y).hom.app Z = (CategoryTheory.MonoidalCategory.associator X Y Z).hom
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.tensorLeftTensor X Y).inv.app Z = (CategoryTheory.MonoidalCategory.associator X Y Z).inv
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.tensorRightTensor X Y).hom.app Z = (CategoryTheory.MonoidalCategory.associator Z X Y).inv
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.tensorRightTensor X Y).inv.app Z = (CategoryTheory.MonoidalCategory.associator Z X Y).hom
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X Y Z : C₁ × C₂<GOAL>CategoryTheory.MonoidalCategory.associator X Y Z = (CategoryTheory.MonoidalCategory.associator X.1 Y.1 Z.1).prod (CategoryTheory.MonoidalCategory.associator X.2 Y.2 Z.2)
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<GOAL>∀ {X₁ Y₁ X₂ Y₂ : C₁ × C₂} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), CategoryTheory.MonoidalCategory.tensorHom f g = (CategoryTheory.MonoidalCategory.tensorHom f.1 g.1, CategoryTheory.MonoidalCategory.tensorHom f.2 g.2)
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X : C₁ × C₂<GOAL>∀ (x x_1 : C₁ × C₂) (f : x ⟶ x_1), CategoryTheory.MonoidalCategory.whiskerLeft X f = (CategoryTheory.MonoidalCategory.whiskerLeft X.1 f.1, CategoryTheory.MonoidalCategory.whiskerLeft X.2 f.2)
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X Y : C₁ × C₂<GOAL>CategoryTheory.MonoidalCategory.tensorObj X Y = (CategoryTheory.MonoidalCategory.tensorObj X.1 Y.1, CategoryTheory.MonoidalCategory.tensorObj X.2 Y.2)
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<GOAL>𝟙_ (C₁ × C₂) = (𝟙_ C₁, 𝟙_ C₂)
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<GOAL>∀ {X₁ X₂ : C₁ × C₂} (f : X₁ ⟶ X₂) (X : C₁ × C₂), CategoryTheory.MonoidalCategory.whiskerRight f X = (CategoryTheory.MonoidalCategory.whiskerRight f.1 X.1, CategoryTheory.MonoidalCategory.whiskerRight f.2 X.2)
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X : C₁ × C₂<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom.1 = (CategoryTheory.MonoidalCategory.leftUnitor X.1).hom
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X : C₁ × C₂<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom.2 = (CategoryTheory.MonoidalCategory.leftUnitor X.2).hom
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X : C₁ × C₂<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv.1 = (CategoryTheory.MonoidalCategory.leftUnitor X.1).inv
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X : C₁ × C₂<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv.2 = (CategoryTheory.MonoidalCategory.leftUnitor X.2).inv
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X : C₁ × C₂<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom.1 = (CategoryTheory.MonoidalCategory.rightUnitor X.1).hom
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X : C₁ × C₂<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom.2 = (CategoryTheory.MonoidalCategory.rightUnitor X.2).hom
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X : C₁ × C₂<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv.1 = (CategoryTheory.MonoidalCategory.rightUnitor X.1).inv
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.MonoidalCategory C₂<VAR>X : C₁ × C₂<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv.2 = (CategoryTheory.MonoidalCategory.rightUnitor X.2).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>self : CategoryTheory.Pretriangulated C<VAR>T₁ : CategoryTheory.Pretriangulated.Triangle C<GOAL>T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → ∀ (T₂ : CategoryTheory.Pretriangulated.Triangle C), (T₂ ≅ T₁) → T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>self : CategoryTheory.Pretriangulated C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>self : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<GOAL>T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ → ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>self : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ T.rotate ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>self : CategoryTheory.Pretriangulated C<VAR>X : C<GOAL>CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>e : T₁ ≅ T₂<GOAL>T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.rotate ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.invRotate ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.mor₁ ≫ T.mor₂ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.mor₂ ≫ T.mor₃ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).X₁ = T.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).f = T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).X₂ = T.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).g = T.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).X₃ = T.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>e : T ≅ T'<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₁ = e.inv.hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>e : T ≅ T'<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₂ = e.inv.hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>e : T ≅ T'<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₃ = e.inv.hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>e : T ≅ T'<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₂ = e.hom.hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>e : T ≅ T'<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₁ = e.hom.hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>e : T ≅ T'<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₃ = e.hom.hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>Y Z : C<VAR>g : Y ⟶ Z<GOAL>∃ X f h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>Z X : C<VAR>h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X<GOAL>∃ Y f g, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>c : T₁.obj₃ ⟶ T₂.obj₃<VAR>comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂<GOAL>∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>c : T₁.obj₃ ⟶ T₂.obj₃<VAR>comm : T₁.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map a = c ≫ T₂.mor₃<GOAL>∃ b, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>X : C<GOAL>CategoryTheory.Pretriangulated.Triangle.mk 0 (𝟙 X) 0 ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>X : C<GOAL>CategoryTheory.Pretriangulated.Triangle.mk 0 0 (𝟙 ((CategoryTheory.shiftFunctor C 1).obj X)) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>X : C<VAR>f : T.obj₂ ⟶ X<VAR>hf : T.mor₁ ≫ f = 0<GOAL>∃ g, f = T.mor₂ ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>X : C<VAR>f : T.obj₃ ⟶ X<VAR>hf : T.mor₂ ≫ f = 0<GOAL>∃ g, f = T.mor₃ ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>X : C<VAR>f : X ⟶ T.obj₂<VAR>hf : f ≫ T.mor₂ = 0<GOAL>∃ g, f = g ≫ T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>X : C<VAR>f : X ⟶ (CategoryTheory.shiftFunctor C 1).obj T.obj₁<VAR>hf : f ≫ (CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0<GOAL>∃ g, f = g ≫ T.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>X : C<VAR>f : X ⟶ T.obj₃<VAR>hf : f ≫ T.mor₃ = 0<GOAL>∃ g, f = g ≫ T.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.mor₃ = 0 ↔ CategoryTheory.Epi T.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.mor₂ = 0 ↔ CategoryTheory.Epi T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.mor₁ = 0 ↔ CategoryTheory.Epi T.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.Epi T.mor₂<GOAL>T.mor₃ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.Epi T.mor₁<GOAL>T.mor₂ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.Epi T.mor₃<GOAL>T.mor₁ = 0