ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>CategoryTheory.WithInitial.down (CategoryTheory.CategoryStruct.id (CategoryTheory.WithInitial.of X)) = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.of Y<VAR>g : CategoryTheory.WithInitial.of Y ⟶ CategoryTheory.WithInitial.of Z<GOAL>CategoryTheory.WithInitial.down (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.down f) (CategoryTheory.WithInitial.down g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.star<GOAL>False
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.map F).obj X = match X with | CategoryTheory.WithInitial.of x => CategoryTheory.WithInitial.of (F.obj x) | CategoryTheory.WithInitial.star => CategoryTheory.WithInitial.star
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.WithInitial C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.WithInitial.map F).map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => PUnit.unit | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => PUnit.unit
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.mapId C).inv.app X = (match X with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of x) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.mapId C).hom.app X = (match X with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of x) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>E : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} D<VAR>CategoryTheory.Category.{u_4, u_2} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.mapComp F G).inv.app X = (match X with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of (G.obj (F.obj x))) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>E : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} D<VAR>CategoryTheory.Category.{u_4, u_2} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.mapComp F G).hom.app X = (match X with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of (G.obj (F.obj x))) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F G : CategoryTheory.Functor C D<VAR>η : F ⟶ G<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.map₂ η).app X = match X with | CategoryTheory.WithInitial.of x => η.app x | CategoryTheory.WithInitial.star => CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star
<VAR>C : CategoryTheory.Cat<GOAL>CategoryTheory.WithInitial.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithInitial ↑C)
<GOAL>∀ {X Y : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑X ↑Y), CategoryTheory.WithInitial.prelaxfunctor.map F = CategoryTheory.WithInitial.map F
<GOAL>∀ {a b : CategoryTheory.Cat} {f g : a ⟶ b} (η : f ⟶ g), CategoryTheory.WithInitial.prelaxfunctor.map₂ η = CategoryTheory.WithInitial.map₂ η
<GOAL>CategoryTheory.WithInitial.pseudofunctor.toPrelaxFunctor = CategoryTheory.WithInitial.prelaxfunctor
<GOAL>∀ {a b c : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑a ↑b) (G : CategoryTheory.Functor ↑b ↑c), CategoryTheory.WithInitial.pseudofunctor.mapComp F G = CategoryTheory.WithInitial.mapComp F G
<VAR>C : CategoryTheory.Cat<GOAL>CategoryTheory.WithInitial.pseudofunctor.mapId C = CategoryTheory.WithInitial.mapId ↑C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → Z ⟶ F.obj x<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y<VAR>X Y : CategoryTheory.WithInitial C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.WithInitial.lift F M hM).map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of x, x_1 => M x | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id ((fun X => match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z) CategoryTheory.WithInitial.star)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → Z ⟶ F.obj x<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.lift F M hM).obj X = match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → Z ⟶ F.obj x<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y<VAR>X : C<GOAL>(CategoryTheory.WithInitial.inclLift F M hM).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → Z ⟶ F.obj x<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y<VAR>X : C<GOAL>(CategoryTheory.WithInitial.inclLift F M hM).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → Z ⟶ F.obj x<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y<GOAL>(CategoryTheory.WithInitial.liftStar F M hM).inv = CategoryTheory.CategoryStruct.id Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → Z ⟶ F.obj x<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y<GOAL>(CategoryTheory.WithInitial.liftStar F M hM).hom = CategoryTheory.CategoryStruct.id Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → Z ⟶ F.obj x<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y<VAR>x : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.liftStar F M hM).hom ((CategoryTheory.WithInitial.lift F M hM).map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj x))) = CategoryTheory.CategoryStruct.comp (M x) ((CategoryTheory.WithInitial.inclLift F M hM).hom.app x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsInitial Z<VAR>X Y : CategoryTheory.WithInitial C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.WithInitial.liftToInitial F hZ).map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of x, x_1 => hZ.to (F.obj x) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsInitial Z<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.liftToInitial F hZ).obj X = match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsInitial Z<VAR>X : C<GOAL>(CategoryTheory.WithInitial.inclLiftToInitial F hZ).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsInitial Z<VAR>X : C<GOAL>(CategoryTheory.WithInitial.inclLiftToInitial F hZ).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsInitial Z<VAR>G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D<VAR>h : CategoryTheory.WithInitial.incl.comp G ≅ F<VAR>hG : G.obj CategoryTheory.WithInitial.star ≅ Z<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsInitial Z<VAR>G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D<VAR>h : CategoryTheory.WithInitial.incl.comp G ≅ F<VAR>hG : G.obj CategoryTheory.WithInitial.star ≅ Z<VAR>X : CategoryTheory.WithInitial C<GOAL>(CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C → D<VAR>CategoryTheory.Functorial F<VAR>self : CategoryTheory.LaxMonoidal F<VAR>X Y : C<VAR>X' : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft (F X') (CategoryTheory.map F f) ≫ CategoryTheory.LaxMonoidal.μ X' Y = CategoryTheory.LaxMonoidal.μ X' X ≫ CategoryTheory.map F (CategoryTheory.MonoidalCategory.whiskerLeft X' f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C → D<VAR>CategoryTheory.Functorial F<VAR>self : CategoryTheory.LaxMonoidal F<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (F X)).hom = CategoryTheory.MonoidalCategory.whiskerRight CategoryTheory.LaxMonoidal.ε (F X) ≫ CategoryTheory.LaxMonoidal.μ (𝟙_ C) X ≫ CategoryTheory.map F (CategoryTheory.MonoidalCategory.leftUnitor X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C → D<VAR>CategoryTheory.Functorial F<VAR>self : CategoryTheory.LaxMonoidal F<VAR>X Y Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.LaxMonoidal.μ X Y) (F Z) ≫ CategoryTheory.LaxMonoidal.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≫ CategoryTheory.map F (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator (F X) (F Y) (F Z)).hom ≫ CategoryTheory.MonoidalCategory.whiskerLeft (F X) (CategoryTheory.LaxMonoidal.μ Y Z) ≫ CategoryTheory.LaxMonoidal.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C → D<VAR>CategoryTheory.Functorial F<VAR>self : CategoryTheory.LaxMonoidal F<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor (F X)).hom = CategoryTheory.MonoidalCategory.whiskerLeft (F X) CategoryTheory.LaxMonoidal.ε ≫ CategoryTheory.LaxMonoidal.μ X (𝟙_ C) ≫ CategoryTheory.map F (CategoryTheory.MonoidalCategory.rightUnitor X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C → D<VAR>CategoryTheory.Functorial F<VAR>self : CategoryTheory.LaxMonoidal F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.map F f) (F X') ≫ CategoryTheory.LaxMonoidal.μ Y X' = CategoryTheory.LaxMonoidal.μ X X' ≫ CategoryTheory.map F (CategoryTheory.MonoidalCategory.whiskerRight f X')
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C → D<VAR>I₁ : CategoryTheory.Functorial F<VAR>I₂ : CategoryTheory.LaxMonoidal F<VAR>X Y : C<GOAL>(CategoryTheory.LaxMonoidalFunctor.of F).μ X Y = CategoryTheory.LaxMonoidal.μ X Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C → D<VAR>I₁ : CategoryTheory.Functorial F<VAR>I₂ : CategoryTheory.LaxMonoidal F<GOAL>(CategoryTheory.LaxMonoidalFunctor.of F).ε = CategoryTheory.LaxMonoidal.ε
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C → D<VAR>I₁ : CategoryTheory.Functorial F<VAR>I₂ : CategoryTheory.LaxMonoidal F<GOAL>∀ (a : C), (CategoryTheory.LaxMonoidalFunctor.of F).obj a = F a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C → D<VAR>I₁ : CategoryTheory.Functorial F<VAR>I₂ : CategoryTheory.LaxMonoidal F<VAR>X Y : C<GOAL>∀ (a : X ⟶ Y), (CategoryTheory.LaxMonoidalFunctor.of F).map a = CategoryTheory.Functorial.map' a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X<GOAL>(CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₃ = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X<GOAL>(CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₁ = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X<GOAL>(CategoryTheory.Pretriangulated.Triangle.mk f g h).obj₁ = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X<GOAL>(CategoryTheory.Pretriangulated.Triangle.mk f g h).obj₃ = Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X<GOAL>(CategoryTheory.Pretriangulated.Triangle.mk f g h).obj₂ = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X<GOAL>(CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₂ = g
<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.contractibleTriangle X).obj₂ = 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<VAR>X : C<GOAL>(CategoryTheory.Pretriangulated.contractibleTriangle X).mor₁ = 𝟙 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<VAR>X : C<GOAL>(CategoryTheory.Pretriangulated.contractibleTriangle X).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.contractibleTriangle X).obj₁ = 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<VAR>X : C<GOAL>(CategoryTheory.Pretriangulated.contractibleTriangle X).obj₃ = 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.contractibleTriangle X).mor₃ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂<GOAL>T₁.mor₁ ≫ self.hom₂ = self.hom₁ ≫ T₂.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂<GOAL>T₁.mor₂ ≫ self.hom₃ = self.hom₂ ≫ T₂.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂<GOAL>T₁.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map self.hom₁ = self.hom₃ ≫ T₂.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.triangleMorphismId T).hom₃ = 𝟙 T.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.triangleMorphismId T).hom₂ = 𝟙 T.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.triangleMorphismId T).hom₁ = 𝟙 T.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ T₃ : CategoryTheory.Pretriangulated.Triangle C<VAR>f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂<VAR>g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃<GOAL>(f.comp g).hom₂ = f.hom₂ ≫ g.hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ T₃ : CategoryTheory.Pretriangulated.Triangle C<VAR>f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂<VAR>g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃<GOAL>(f.comp g).hom₁ = f.hom₁ ≫ g.hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ T₃ : CategoryTheory.Pretriangulated.Triangle C<VAR>f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂<VAR>g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃<GOAL>(f.comp g).hom₃ = f.hom₃ ≫ g.hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<GOAL>∀ {X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z), f ≫ g = CategoryTheory.Pretriangulated.TriangleMorphism.comp f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A : CategoryTheory.Pretriangulated.Triangle C<GOAL>𝟙 A = CategoryTheory.Pretriangulated.triangleMorphismId A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>f g : A ⟶ B<VAR>h₁ : f.hom₁ = g.hom₁<VAR>h₂ : f.hom₂ = g.hom₂<VAR>h₃ : f.hom₃ = g.hom₃<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A : CategoryTheory.Pretriangulated.Triangle C<GOAL>(𝟙 A).hom₁ = 𝟙 A.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A : CategoryTheory.Pretriangulated.Triangle C<GOAL>(𝟙 A).hom₂ = 𝟙 A.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A : CategoryTheory.Pretriangulated.Triangle C<GOAL>(𝟙 A).hom₃ = 𝟙 A.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X Y Z : CategoryTheory.Pretriangulated.Triangle C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).hom₁ = f.hom₁ ≫ g.hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X Y Z : CategoryTheory.Pretriangulated.Triangle C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).hom₂ = f.hom₂ ≫ g.hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X Y Z : CategoryTheory.Pretriangulated.Triangle C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).hom₃ = f.hom₃ ≫ g.hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>hom₁ : A.obj₁ ⟶ B.obj₁<VAR>hom₂ : A.obj₂ ⟶ B.obj₂<VAR>hom₃ : A.obj₃ ⟶ B.obj₃<VAR>comm₁ : A.mor₁ ≫ hom₂ = hom₁ ≫ B.mor₁ := by aesop_cat<VAR>comm₂ : A.mor₂ ≫ hom₃ = hom₂ ≫ B.mor₂ := by aesop_cat<VAR>comm₃ : A.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map hom₁ = hom₃ ≫ B.mor₃ := by aesop_cat<GOAL>(A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₁ = hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>hom₁ : A.obj₁ ⟶ B.obj₁<VAR>hom₂ : A.obj₂ ⟶ B.obj₂<VAR>hom₃ : A.obj₃ ⟶ B.obj₃<VAR>comm₁ : A.mor₁ ≫ hom₂ = hom₁ ≫ B.mor₁ := by aesop_cat<VAR>comm₂ : A.mor₂ ≫ hom₃ = hom₂ ≫ B.mor₂ := by aesop_cat<VAR>comm₃ : A.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map hom₁ = hom₃ ≫ B.mor₃ := by aesop_cat<GOAL>(A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₂ = hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.HasShift C ℤ<VAR>A B : CategoryTheory.Pretriangulated.Triangle C<VAR>hom₁ : A.obj₁ ⟶ B.obj₁<VAR>hom₂ : A.obj₂ ⟶ B.obj₂<VAR>hom₃ : A.obj₃ ⟶ B.obj₃<VAR>comm₁ : A.mor₁ ≫ hom₂ = hom₁ ≫ B.mor₁ := by aesop_cat<VAR>comm₂ : A.mor₂ ≫ hom₃ = hom₂ ≫ B.mor₂ := by aesop_cat<VAR>comm₃ : A.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map hom₁ = hom₃ ≫ B.mor₃ := by aesop_cat<GOAL>(A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₃ = hom₃