ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u₂<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : CategoryTheory.Functor (CategoryTheory.Discrete J) C} (f : X ⟶ Y) (j : J), (CategoryTheory.piEquivalenceFunctorDiscrete J C).inverse.map f j = f.app { as := j }
<VAR>J : Type u₂<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : J → C} (f : X ⟶ Y), (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.map f = CategoryTheory.Discrete.natTrans fun j => f j.as
<VAR>J : Type u₂<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.piEquivalenceFunctorDiscrete J C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (J → C))
<VAR>J : Type u₂<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete J) C<VAR>j : J<GOAL>(CategoryTheory.piEquivalenceFunctorDiscrete J C).inverse.obj F j = F.obj { as := j }
<VAR>J : Type u₂<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : J → C<GOAL>(CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.obj F = CategoryTheory.Discrete.functor F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.IsCompatibleWithTriangulation<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₂), W a → W b → CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ → ∃ c, ∃ (_ : W 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>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.HasShift D ℤ<VAR>L.CommShift ℤ<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle D<VAR>e : T₂ ≅ T₁<VAR>h : T₁ ∈ L.essImageDistTriang<GOAL>T₂ ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.HasShift D ℤ<VAR>L.CommShift ℤ<VAR>L.EssSurj<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>L.PreservesZeroMorphisms<VAR>X : D<GOAL>CategoryTheory.Pretriangulated.contractibleTriangle X ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.HasShift D ℤ<VAR>L.CommShift ℤ<VAR>CategoryTheory.Preadditive D<VAR>L.Additive<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>T : CategoryTheory.Pretriangulated.Triangle D<GOAL>T ∈ L.essImageDistTriang ↔ T.rotate ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.HasShift D ℤ<VAR>L.CommShift ℤ<VAR>H : ∀ (T₁' T₂' : CategoryTheory.Pretriangulated.Triangle C), T₁' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → T₂' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), CategoryTheory.CategoryStruct.comp (L.map T₁'.mor₁) b = CategoryTheory.CategoryStruct.comp a (L.map T₂'.mor₁) → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle D<VAR>hT₁ : T₁ ∈ L.essImageDistTriang<VAR>hT₂ : T₂ ∈ L.essImageDistTriang<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : 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 D 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.HasShift D ℤ<VAR>L.CommShift ℤ<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.HasShift D ℤ<VAR>L.CommShift ℤ<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.IsCompatibleWithTriangulation<VAR>W.HasLeftCalculusOfFractions<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle D<VAR>hT₁ : T₁ ∈ L.essImageDistTriang<VAR>hT₂ : T₂ ∈ L.essImageDistTriang<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : 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 D 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.HasShift D ℤ<VAR>L.CommShift ℤ<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated D<VAR>L.IsTriangulated<VAR>CategoryTheory.IsTriangulated C<GOAL>CategoryTheory.IsTriangulated D
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>CategoryTheory.HasShift D ℤ<VAR>L.CommShift ℤ<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Preadditive D<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive<VAR>CategoryTheory.Pretriangulated D<VAR>L.mapArrow.EssSurj<VAR>L.IsTriangulated<VAR>T : CategoryTheory.Pretriangulated.Triangle D<GOAL>T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ T ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>self : CategoryTheory.SingleFunctors C D A<VAR>a : A<GOAL>self.shiftIso 0 a a ⋯ = CategoryTheory.isoWhiskerLeft (self.functor a) (CategoryTheory.shiftFunctorZero D A)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>self : CategoryTheory.SingleFunctors C D A<VAR>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>self.shiftIso (m + n) a a'' ⋯ = CategoryTheory.isoWhiskerLeft (self.functor a'') (CategoryTheory.shiftFunctorAdd D m n) ≪≫ ((self.functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫ CategoryTheory.isoWhiskerRight (self.shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫ self.shiftIso n a a' ha'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso (m + n) a a'' ⋯).hom.app X = (CategoryTheory.shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X) ≫ (CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso (m + n) a a'' ⋯).inv.app X = (F.shiftIso n a a' ha').inv.app X ≫ (CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X) ≫ (CategoryTheory.shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>n m mn : A<VAR>hnm : m + n = mn<VAR>a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>F.shiftIso mn a a'' ⋯ = CategoryTheory.isoWhiskerLeft (F.functor a'') (CategoryTheory.shiftFunctorAdd' D m n mn hnm) ≪≫ ((F.functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫ CategoryTheory.isoWhiskerRight (F.shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>n m mn : A<VAR>hnm : m + n = mn<VAR>a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso mn a a'' ⋯).hom.app X = (CategoryTheory.shiftFunctorAdd' D m n mn hnm).hom.app ((F.functor a'').obj X) ≫ (CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>n m mn : A<VAR>hnm : m + n = mn<VAR>a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso mn a a'' ⋯).inv.app X = (F.shiftIso n a a' ha').inv.app X ≫ (CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X) ≫ (CategoryTheory.shiftFunctorAdd' D m n mn hnm).inv.app ((F.functor a'').obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>a : A<VAR>X : C<GOAL>(F.shiftIso 0 a a ⋯).hom.app X = (CategoryTheory.shiftFunctorZero D A).hom.app ((F.functor a).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>a : A<VAR>X : C<GOAL>(F.shiftIso 0 a a ⋯).inv.app X = (CategoryTheory.shiftFunctorZero D A).inv.app ((F.functor a).toPrefunctor.1 X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G : CategoryTheory.SingleFunctors C D A<VAR>self : F.Hom G<VAR>n a a' : A<VAR>ha' : n + a = a'<GOAL>(F.shiftIso n a a' ha').hom ≫ self.hom a = CategoryTheory.whiskerRight (self.hom a') (CategoryTheory.shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>a : A<GOAL>(CategoryTheory.SingleFunctors.Hom.id F).hom a = 𝟙 (F.functor a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G H : CategoryTheory.SingleFunctors C D A<VAR>α : F.Hom G<VAR>β : G.Hom H<VAR>a : A<GOAL>(α.comp β).hom a = α.hom a ≫ β.hom a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>a : A<GOAL>(𝟙 F).hom a = 𝟙 (F.functor a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G H : CategoryTheory.SingleFunctors C D A<VAR>f : F ⟶ G<VAR>g : G ⟶ H<VAR>a : A<GOAL>(f ≫ g).hom a = f.hom a ≫ g.hom a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G : CategoryTheory.SingleFunctors C D A<VAR>f g : F ⟶ G<VAR>h : f.hom = g.hom<GOAL>f = g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G : CategoryTheory.SingleFunctors C D A<VAR>iso : (a : A) → F.functor a ≅ G.functor a<VAR>comm : ∀ (n a a' : A) (ha' : n + a = a'), (F.shiftIso n a a' ha').hom ≫ (iso a).hom = CategoryTheory.whiskerRight (iso a').hom (CategoryTheory.shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom<VAR>a : A<GOAL>(CategoryTheory.SingleFunctors.isoMk iso comm).inv.hom a = (iso a).inv
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G : CategoryTheory.SingleFunctors C D A<VAR>iso : (a : A) → F.functor a ≅ G.functor a<VAR>comm : ∀ (n a a' : A) (ha' : n + a = a'), (F.shiftIso n a a' ha').hom ≫ (iso a).hom = CategoryTheory.whiskerRight (iso a').hom (CategoryTheory.shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom<VAR>a : A<GOAL>(CategoryTheory.SingleFunctors.isoMk iso comm).hom.hom a = (iso a).hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>a : A<VAR>F : CategoryTheory.SingleFunctors C D A<GOAL>(CategoryTheory.SingleFunctors.evaluation C D a).obj F = F.functor a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>a : A<VAR>F G : CategoryTheory.SingleFunctors C D A<VAR>φ : F ⟶ G<GOAL>(CategoryTheory.SingleFunctors.evaluation C D a).map φ = φ.hom a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G : CategoryTheory.SingleFunctors C D A<VAR>e : F ≅ G<VAR>n : A<GOAL>e.hom.hom n ≫ e.inv.hom n = 𝟙 (F.functor n)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G : CategoryTheory.SingleFunctors C D A<VAR>e : F ≅ G<VAR>n : A<GOAL>e.inv.hom n ≫ e.hom.hom n = 𝟙 (G.functor n)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G : CategoryTheory.SingleFunctors C D A<VAR>e : F ≅ G<VAR>n : A<VAR>X : C<GOAL>(e.hom.hom n).app X ≫ (e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F G : CategoryTheory.SingleFunctors C D A<VAR>e : F ≅ G<VAR>n : A<VAR>X : C<GOAL>(e.inv.hom n).app X ≫ (e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_8, u_3} E<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>G : D ⥤ E<VAR>G.CommShift A<VAR>n a a' : A<VAR>ha' : n + a = a'<VAR>X : C<GOAL>((F.postcomp G).shiftIso n a a' ha').inv.app X = G.map ((F.shiftIso n a a' ha').inv.app X) ≫ (G.commShiftIso n).hom.app ((F.functor a').obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_8, u_3} E<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>G : D ⥤ E<VAR>G.CommShift A<VAR>n a a' : A<VAR>ha' : n + a = a'<VAR>X : C<GOAL>((F.postcomp G).shiftIso n a a' ha').hom.app X = (G.commShiftIso n).inv.app ((F.functor a').obj X) ≫ G.map ((F.shiftIso n a a' ha').hom.app X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_8, u_3} E<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>G : D ⥤ E<VAR>G.CommShift A<VAR>a : A<GOAL>(F.postcomp G).functor a = F.functor a ⋙ G
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_8, u_3} E<VAR>CategoryTheory.Category.{u_9, u_4} E'<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>CategoryTheory.HasShift E' A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>G : D ⥤ E<VAR>G' : E ⥤ E'<VAR>G.CommShift A<VAR>G'.CommShift A<VAR>a : A<GOAL>∀ (x : C), ((F.postcompPostcompIso G G').inv.hom a).app x = 𝟙 (G'.obj (G.obj ((F.functor a).obj x)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_8, u_3} E<VAR>CategoryTheory.Category.{u_9, u_4} E'<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>CategoryTheory.HasShift E' A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>G : D ⥤ E<VAR>G' : E ⥤ E'<VAR>G.CommShift A<VAR>G'.CommShift A<VAR>a : A<GOAL>∀ (x : C), ((F.postcompPostcompIso G G').hom.hom a).app x = 𝟙 (G'.obj (G.obj ((F.functor a).obj x)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_8, u_3} E<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>G G' : D ⥤ E<VAR>e : G ≅ G'<VAR>G.CommShift A<VAR>G'.CommShift A<VAR>CategoryTheory.NatTrans.CommShift e.hom A<VAR>a : A<VAR>X : C<GOAL>((F.postcompIsoOfIso e).hom.hom a).app X = e.hom.app ((F.functor a).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_8, u_3} E<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>F : CategoryTheory.SingleFunctors C D A<VAR>G G' : D ⥤ E<VAR>e : G ≅ G'<VAR>G.CommShift A<VAR>G'.CommShift A<VAR>CategoryTheory.NatTrans.CommShift e.hom A<VAR>a : A<VAR>X : C<GOAL>((F.postcompIsoOfIso e).inv.hom a).app X = e.inv.app ((F.functor a).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>ι : Type v<VAR>B : ι → C<VAR>hB : ∀ (A : C), ∃ i, Nonempty (B i ⟶ A)<GOAL>∃ T, ∀ (X : C), Nonempty (T ⟶ X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasWideEqualizers C<VAR>T : C<VAR>hT : ∀ (X : C), Nonempty (T ⟶ X)<GOAL>CategoryTheory.Limits.HasInitial C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>T : CategoryTheory.Monad C<VAR>T.Additive<VAR>F G : T.Algebra<VAR>α β : F ⟶ G<GOAL>(α + β).f = α.f + β.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>T : CategoryTheory.Monad C<VAR>T.Additive<VAR>F G : T.Algebra<VAR>r : ℤ<VAR>α : F ⟶ G<GOAL>(r • α).f = r • α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>T : CategoryTheory.Monad C<VAR>T.Additive<VAR>F G : T.Algebra<GOAL>CategoryTheory.Monad.Algebra.Hom.f 0 = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>T : CategoryTheory.Monad C<VAR>T.Additive<VAR>F G : T.Algebra<VAR>n : ℕ<VAR>α : F ⟶ G<GOAL>(n • α).f = n • α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>T : CategoryTheory.Monad C<VAR>T.Additive<VAR>F G : T.Algebra<VAR>α : F ⟶ G<GOAL>(-α).f = -α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>T : CategoryTheory.Monad C<VAR>T.Additive<VAR>F G : T.Algebra<VAR>α β : F ⟶ G<GOAL>(α - β).f = α.f - β.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>U : CategoryTheory.Comonad C<VAR>U.Additive<VAR>F G : U.Coalgebra<VAR>n : ℕ<VAR>α : F ⟶ G<GOAL>(n • α).f = n • α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>U : CategoryTheory.Comonad C<VAR>U.Additive<VAR>F G : U.Coalgebra<GOAL>CategoryTheory.Comonad.Coalgebra.Hom.f 0 = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>U : CategoryTheory.Comonad C<VAR>U.Additive<VAR>F G : U.Coalgebra<VAR>α : F ⟶ G<GOAL>(-α).f = -α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>U : CategoryTheory.Comonad C<VAR>U.Additive<VAR>F G : U.Coalgebra<VAR>r : ℤ<VAR>α : F ⟶ G<GOAL>(r • α).f = r • α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>U : CategoryTheory.Comonad C<VAR>U.Additive<VAR>F G : U.Coalgebra<VAR>α β : F ⟶ G<GOAL>(α + β).f = α.f + β.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>U : CategoryTheory.Comonad C<VAR>U.Additive<VAR>F G : U.Coalgebra<VAR>α β : F ⟶ G<GOAL>(α - β).f = α.f - β.f