ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>a : B<GOAL>(CategoryTheory.Bicategory.leftUnitor η).hom.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<GOAL>∀ {X Y Z : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.OplaxNatTrans X Y) (θ : CategoryTheory.OplaxNatTrans Y Z) (a : B), (CategoryTheory.CategoryStruct.comp η θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H : CategoryTheory.OplaxFunctor B C<GOAL>∀ (x x_1 : F ⟶ G) (Γ : x ⟶ x_1) (η : G ⟶ H) (a : B), (CategoryTheory.Bicategory.whiskerRight Γ η).app a = CategoryTheory.Bicategory.whiskerRight (Γ.app a) (η.app a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>a : B<GOAL>(CategoryTheory.Bicategory.leftUnitor η).inv.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>a : B<GOAL>(CategoryTheory.CategoryStruct.id F).app a = CategoryTheory.CategoryStruct.id (F.obj a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<GOAL>(F ⟶ G) = CategoryTheory.OplaxNatTrans F G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C 0 0 ⋯).hom.app X) ((CategoryTheory.shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C 0 0 ⋯).inv.app X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>a₁ a₂ a₃ : ℤ<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : ℤ<VAR>h₁ : a₁ + b₁ = 0<VAR>h₂ : a₂ + b₂ = 0<VAR>h₃ : a₃ + b₃ = 0<GOAL>(CategoryTheory.shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₃ b₃ h₃).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C b₁).toPrefunctor.1 (Opposite.unop X)))) ((CategoryTheory.shiftFunctor Cᵒᵖ a₂).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₁ b₁ h₁).inv.app X))))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>a₁ a₂ a₃ : ℤ<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : ℤ<VAR>h₁ : a₁ + b₁ = 0<VAR>h₂ : a₂ + b₂ = 0<VAR>h₃ : a₃ + b₃ = 0<GOAL>(CategoryTheory.shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ a₂).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₁ b₁ h₁).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((CategoryTheory.shiftFunctor C b₁).op.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₃ b₃ h₃).inv.app X)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>n m : ℤ<VAR>hnm : n + m = 0<VAR>K L : Cᵒᵖ<VAR>φ : K ⟶ L<GOAL>(CategoryTheory.shiftFunctor Cᵒᵖ n).map φ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app K) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m).map φ.unop).op ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app L))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<GOAL>(CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor = CategoryTheory.shiftFunctor Cᵒᵖ n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<GOAL>(CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse = (CategoryTheory.shiftFunctor C n).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X) ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X) f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op) ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X) f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X) ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>n : ℤ<GOAL>(CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X).unop = ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>n : ℤ<GOAL>(CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X).unop = ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>n : ℤ<GOAL>(CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) = (CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>n : ℤ<GOAL>(CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) = (CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ<VAR>φ : T₁ ⟶ T₂<GOAL>((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₁ = φ.unop.hom₃.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).obj T = CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop T).mor₂.op (Opposite.unop T).mor₁.op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T).obj₁)) ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop T).mor₃.op))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ<VAR>φ : T₁ ⟶ T₂<GOAL>((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₂ = φ.unop.hom₂.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ<VAR>φ : T₁ ⟶ T₂<GOAL>((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₃ = φ.unop.hom₁.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<VAR>φ : T₁ ⟶ T₂<GOAL>(CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).map φ = Quiver.Hom.op { hom₁ := φ.hom₃.unop, hom₂ := φ.hom₂.unop, hom₃ := φ.hom₁.unop, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).obj T = Opposite.op (CategoryTheory.Pretriangulated.Triangle.mk T.mor₂.unop T.mor₁.unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁).unop ((CategoryTheory.shiftFunctor C 1).map T.mor₃.unop)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C).hom.app X = ((CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop X).mor₁ (Opposite.unop X).mor₂ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app (Opposite.op (Opposite.unop X).obj₃)).unop ((CategoryTheory.shiftFunctor C 1).map (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop X).mor₃.op).unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop X).obj₁)).unop)))).homMk (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₁) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₂) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₃) ⋯ ⋯ ⋯).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C).inv.app X = ((Opposite.unop X).homMk (CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop X).mor₁ (Opposite.unop X).mor₂ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app (Opposite.op (Opposite.unop X).obj₃)).unop ((CategoryTheory.shiftFunctor C 1).map (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop X).mor₃.op).unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop X).obj₁)).unop)))) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₁) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₂) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₃) ⋯ ⋯ ⋯).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<GOAL>(CategoryTheory.Pretriangulated.triangleOpEquivalence C).counitIso = CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<GOAL>(CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse = CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<GOAL>(CategoryTheory.Pretriangulated.triangleOpEquivalence C).unitIso = CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<GOAL>(CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor = CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔ Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔ ∃ T', ∃ (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (T ≅ (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T'))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T₁ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C<VAR>T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<VAR>e : T₂ ≅ T₁<GOAL>T₂ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).inv.hom₃ = (⋯.iso ⋯).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).hom.hom₁ = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).inv.hom₁ = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).hom.hom₃ = (⋯.iso ⋯).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).inv.hom₂ = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).hom.hom₂ = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>X : Cᵒᵖ<GOAL>CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔ T.rotate ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁<GOAL>∃ c, CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<GOAL>T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ ∃ T', ∃ (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (T ≅ (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T'))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>(CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<VAR>CategoryTheory.Abelian A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>F.IsHomological<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).op.map F).Exact
<VAR>C : Type u<VAR>a : CategoryTheory.LocallyDiscrete C<GOAL>{ as := a.as } = a
<VAR>C : Type u<VAR>as : C<GOAL>(CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv.symm as).as = as
<VAR>C : Type u<VAR>self : CategoryTheory.LocallyDiscrete C<GOAL>CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv self = self.as
<VAR>C : Type u<VAR>CategoryTheory.CategoryStruct.{v, u} C<VAR>a : CategoryTheory.LocallyDiscrete C<GOAL>(CategoryTheory.CategoryStruct.id a).as = CategoryTheory.CategoryStruct.id a.as
<VAR>C : Type u<VAR>CategoryTheory.CategoryStruct.{v, u} C<VAR>a b c : CategoryTheory.LocallyDiscrete C<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(CategoryTheory.CategoryStruct.comp f g).as = CategoryTheory.CategoryStruct.comp f.as g.as
<VAR>C : Type u<VAR>CategoryTheory.CategoryStruct.{v, u} C<VAR>X Y : CategoryTheory.LocallyDiscrete C<VAR>f g : X ⟶ Y<VAR>η : f ⟶ g<GOAL>f = g