ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : CommMon_ C<GOAL>((CommMon_.EquivLaxBraidedFunctorPUnit.counitIso C).hom.app X).hom = 𝟙 X.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : CommMon_ C<GOAL>((CommMon_.EquivLaxBraidedFunctorPUnit.counitIso C).inv.app X).hom = 𝟙 X.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CommMon_.equivLaxBraidedFunctorPUnit C).unitIso = CommMon_.EquivLaxBraidedFunctorPUnit.unitIso C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CommMon_.equivLaxBraidedFunctorPUnit C).counitIso = CommMon_.EquivLaxBraidedFunctorPUnit.counitIso C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CommMon_.equivLaxBraidedFunctorPUnit C).functor = CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CommMon_.equivLaxBraidedFunctorPUnit C).inverse = CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<VAR>self : Mod_ A<GOAL>A.mul ▷ self.X ≫ self.act = (α_ A.X A.X self.X).hom ≫ A.X ◁ self.act ≫ self.act
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<VAR>self : Mod_ A<GOAL>A.one ▷ self.X ≫ self.act = (λ_ self.X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<VAR>M : Mod_ A<GOAL>A.X ◁ M.act ≫ M.act = (α_ A.X A.X M.X).inv ≫ A.mul ▷ M.X ≫ M.act
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<VAR>M N : Mod_ A<VAR>self : M.Hom N<GOAL>M.act ≫ self.hom = A.X ◁ self.hom ≫ N.act
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<VAR>M : Mod_ A<GOAL>M.id.hom = 𝟙 M.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<VAR>M N O : Mod_ A<VAR>f : M.Hom N<VAR>g : N.Hom O<GOAL>(Mod_.comp f g).hom = f.hom ≫ g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<VAR>M N : Mod_ A<VAR>f₁ f₂ : M ⟶ N<VAR>h : f₁.hom = f₂.hom<GOAL>f₁ = f₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<VAR>M : Mod_ A<GOAL>(𝟙 M).hom = 𝟙 M.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<VAR>M N K : Mod_ A<VAR>f : M ⟶ N<VAR>g : N ⟶ K<GOAL>(f ≫ g).hom = f.hom ≫ g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<GOAL>(Mod_.regular A).act = A.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<GOAL>(Mod_.regular A).X = A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>((Mod_.comap f).obj M).act = f.hom ▷ M.X ≫ M.act
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>((Mod_.comap f).obj M).X = M.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>f : A ⟶ B<GOAL>∀ {X Y : Mod_ B} (g : X ⟶ Y), ((Mod_.comap f).map g).hom = g.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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>self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃<GOAL>CategoryTheory.Pretriangulated.Triangle.mk self.m₁ self.m₃ (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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>self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃<GOAL>CategoryTheory.CategoryStruct.comp v₁₂ self.m₁ = CategoryTheory.CategoryStruct.comp u₂₃ v₁₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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>self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃<GOAL>CategoryTheory.CategoryStruct.comp v₁₃ self.m₃ = v₂₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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>self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃<GOAL>CategoryTheory.CategoryStruct.comp self.m₁ w₁₃ = w₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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>self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃<GOAL>CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map u₁₂) = CategoryTheory.CategoryStruct.comp self.m₃ w₂₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangle.mor₂ = h.m₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangle.mor₁ = h.m₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangle.mor₃ = CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangle.obj₃ = Z₂₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangle.obj₁ = Z₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangle.obj₂ = Z₁₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangleMorphism₁.hom₁ = CategoryTheory.CategoryStruct.id X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangleMorphism₁.hom₃ = h.m₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangleMorphism₁.hom₂ = u₂₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangleMorphism₂.hom₁ = u₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangleMorphism₂.hom₃ = h.m₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<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₁₃<GOAL>h.triangleMorphism₂.hom₂ = CategoryTheory.CategoryStruct.id X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.IsTriangulated C<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<GOAL>Nonempty (CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)