ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasBinaryBiproduct Y Y<GOAL>f + g = CategoryTheory.Limits.biprod.lift f g ≫ CategoryTheory.Limits.biprod.desc (𝟙 Y) (𝟙 Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<GOAL>CategoryTheory.Limits.biprod.inl ≫ CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₁₁ ≫ CategoryTheory.Limits.biprod.inl + f₁₂ ≫ CategoryTheory.Limits.biprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<GOAL>CategoryTheory.Limits.biprod.inr ≫ CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₂₁ ≫ CategoryTheory.Limits.biprod.inl + f₂₂ ≫ CategoryTheory.Limits.biprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<GOAL>CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ CategoryTheory.Limits.biprod.fst = CategoryTheory.Limits.biprod.fst ≫ f₁₁ + CategoryTheory.Limits.biprod.snd ≫ f₂₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<GOAL>CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ CategoryTheory.Limits.biprod.snd = CategoryTheory.Limits.biprod.fst ≫ f₁₂ + CategoryTheory.Limits.biprod.snd ≫ f₂₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂<GOAL>CategoryTheory.Biprod.ofComponents (CategoryTheory.Limits.biprod.inl ≫ f ≫ CategoryTheory.Limits.biprod.fst) (CategoryTheory.Limits.biprod.inl ≫ f ≫ CategoryTheory.Limits.biprod.snd) (CategoryTheory.Limits.biprod.inr ≫ f ≫ CategoryTheory.Limits.biprod.fst) (CategoryTheory.Limits.biprod.inr ≫ f ≫ CategoryTheory.Limits.biprod.snd) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<VAR>g₁₁ : Y₁ ⟶ Z₁<VAR>g₁₂ : Y₁ ⟶ Z₂<VAR>g₂₁ : Y₂ ⟶ Z₁<VAR>g₂₂ : Y₂ ⟶ Z₂<GOAL>CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ CategoryTheory.Biprod.ofComponents g₁₁ g₁₂ g₂₁ g₂₂ = CategoryTheory.Biprod.ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ : C<VAR>r : X₁ ⟶ X₂<GOAL>(CategoryTheory.Biprod.unipotentUpper r).inv = CategoryTheory.Biprod.ofComponents (𝟙 X₁) (-r) 0 (𝟙 X₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ : C<VAR>r : X₁ ⟶ X₂<GOAL>(CategoryTheory.Biprod.unipotentUpper r).hom = CategoryTheory.Biprod.ofComponents (𝟙 X₁) r 0 (𝟙 X₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ : C<VAR>r : X₂ ⟶ X₁<GOAL>(CategoryTheory.Biprod.unipotentLower r).inv = CategoryTheory.Biprod.ofComponents (𝟙 X₁) 0 (-r) (𝟙 X₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ : C<VAR>r : X₂ ⟶ X₁<GOAL>(CategoryTheory.Biprod.unipotentLower r).hom = CategoryTheory.Biprod.ofComponents (𝟙 X₁) 0 r (𝟙 X₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⊞ X ⟶ Y ⊞ Z<VAR>CategoryTheory.IsIso f<GOAL>𝟙 W = 0 ∨ CategoryTheory.Limits.biprod.inl ≫ f ≫ CategoryTheory.Limits.biprod.fst ≠ 0 ∨ CategoryTheory.Limits.biprod.inl ≫ f ≫ CategoryTheory.Limits.biprod.snd ≠ 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>σ τ : Type<VAR>Finite τ<VAR>S : σ → C<VAR>CategoryTheory.Limits.HasBiproduct S<VAR>T : τ → C<VAR>CategoryTheory.Limits.HasBiproduct T<VAR>s : σ<VAR>f : ⨁ S ⟶ ⨁ T<VAR>CategoryTheory.IsIso f<GOAL>(∀ (t : τ), CategoryTheory.Limits.biproduct.ι S s ≫ f ≫ CategoryTheory.Limits.biproduct.π T t = 0) → 𝟙 (S s) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.IsFiltered C ↔ ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (CategoryTheory.Limits.limit (F.op ⋙ CategoryTheory.yoneda.obj X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.IsCofiltered C ↔ ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (CategoryTheory.Limits.limit (F ⋙ CategoryTheory.coyoneda.obj (Opposite.op X)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C<VAR>I : Type w<VAR>CategoryTheory.Category.{w', w} I<VAR>CategoryTheory.IsCofiltered I<GOAL>CategoryTheory.Limits.HasLimitsOfShape I C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C<VAR>I : Type w<VAR>CategoryTheory.Category.{w', w} I<VAR>CategoryTheory.IsFiltered I<GOAL>CategoryTheory.Limits.HasColimitsOfShape I C
<VAR>α : Type u<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.FinCategory J<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>F : J ⥤ α<GOAL>CategoryTheory.Limits.limit F = Finset.univ.inf F.obj
<VAR>α : Type u<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.FinCategory J<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>F : J ⥤ α<GOAL>CategoryTheory.Limits.colimit F = Finset.univ.sup F.obj
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>ι : Type u<VAR>Fintype ι<VAR>f : ι → α<GOAL>∏ᶜ f = Fintype.elems.inf f
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>ι : Type u<VAR>Fintype ι<VAR>f : ι → α<GOAL>∐ f = Fintype.elems.sup f
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>x y : α<GOAL>(x ⨯ y) = x ⊓ y
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>x y : α<GOAL>(x ⨿ y) = x ⊔ y
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>x y z : α<VAR>f : x ⟶ z<VAR>g : y ⟶ z<GOAL>CategoryTheory.Limits.pullback f g = x ⊓ y
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>x y z : α<VAR>f : z ⟶ x<VAR>g : z ⟶ y<GOAL>CategoryTheory.Limits.pushout f g = x ⊔ y
<VAR>α : Type u<VAR>CompleteLattice α<VAR>J : Type u<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ α<GOAL>CategoryTheory.Limits.limit F = iInf F.obj
<VAR>α : Type u<VAR>CompleteLattice α<VAR>J : Type u<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ α<GOAL>CategoryTheory.Limits.colimit F = iSup F.obj
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>F : CategoryTheory.Limits.WalkingParallelPair ⥤ C<GOAL>CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst F = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.prod.lift (𝟙 (F.obj CategoryTheory.Limits.WalkingParallelPair.zero)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)) (CategoryTheory.Limits.prod.lift (𝟙 (F.obj CategoryTheory.Limits.WalkingParallelPair.zero)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>CategoryTheory.Limits.HasEqualizers C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>F : CategoryTheory.Limits.WalkingParallelPair ⥤ C<GOAL>CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl F = CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.coprod.desc (𝟙 (F.obj CategoryTheory.Limits.WalkingParallelPair.one)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)) (CategoryTheory.Limits.coprod.desc (𝟙 (F.obj CategoryTheory.Limits.WalkingParallelPair.one)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasPushouts C<GOAL>CategoryTheory.Limits.HasCoequalizers C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Coyoneda.colimitCocone X).pt = PUnit.{v + 1}
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : Cᵒᵖ<VAR>X_1 : C<VAR>a : (CategoryTheory.coyoneda.obj X).obj X_1<GOAL>(CategoryTheory.Coyoneda.colimitCocone X).ι.app X_1 a = id PUnit.unit
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : Cᵒᵖ<VAR>s : CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)<GOAL>∀ (x : (CategoryTheory.Coyoneda.colimitCocone X).pt), (CategoryTheory.Coyoneda.colimitCoconeIsColimit X).desc s x = s.ι.app (Opposite.unop X) (𝟙 (Opposite.unop X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.Category.{t, w} J<VAR>F : J ⥤ Cᵒᵖ<VAR>X : C<VAR>s : ↑(F ⋙ CategoryTheory.yoneda.obj X).sections<GOAL>(CategoryTheory.Limits.coneOfSectionCompYoneda F X s).pt = Opposite.op X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.Category.{t, w} J<VAR>F : J ⥤ Cᵒᵖ<VAR>X : C<VAR>s : ↑(F ⋙ CategoryTheory.yoneda.obj X).sections<GOAL>(CategoryTheory.Limits.coneOfSectionCompYoneda F X s).π = (CategoryTheory.Limits.compYonedaSectionsEquiv F X) s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.Category.{t, w} J<VAR>F : J ⥤ C<VAR>X : Cᵒᵖ<VAR>s : ↑(F ⋙ CategoryTheory.coyoneda.obj X).sections<GOAL>(CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s).pt = Opposite.unop X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.Category.{t, w} J<VAR>F : J ⥤ C<VAR>X : Cᵒᵖ<VAR>s : ↑(F ⋙ CategoryTheory.coyoneda.obj X).sections<GOAL>(CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s).π = (CategoryTheory.Limits.compCoyonedaSectionsEquiv F (Opposite.unop X)) s
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : D ⥤ C<VAR>e.IsEquivalence<VAR>CategoryTheory.Limits.HasInitial C<GOAL>CategoryTheory.Limits.HasInitial D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>CategoryTheory.Limits.HasInitial C ↔ CategoryTheory.Limits.HasInitial D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : D ⥤ C<VAR>e.IsEquivalence<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>CategoryTheory.Limits.HasTerminal D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>CategoryTheory.Limits.HasTerminal C ↔ CategoryTheory.Limits.HasTerminal D
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>self : CategoryTheory.ShiftMkCore C A<VAR>m₁ m₂ m₃ : A<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X) ((self.F m₃).map ((self.add m₁ m₂).hom.app X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X) ((self.add m₂ m₃).hom.app ((self.F m₁).obj X)))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>self : CategoryTheory.ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(self.add n 0).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (self.zero.inv.app ((self.F n).obj X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>self : CategoryTheory.ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(self.add 0 n).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((self.F n).map (self.zero.inv.app X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>h : CategoryTheory.ShiftMkCore C A<VAR>m₁ m₂ m₃ : A<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((h.F m₃).map ((h.add m₁ m₂).inv.app X)) ((h.add (m₁ + m₂) m₃).inv.app X) = CategoryTheory.CategoryStruct.comp ((h.add m₂ m₃).inv.app ((h.F m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((h.add m₁ (m₂ + m₃)).inv.app X) (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>h : CategoryTheory.ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(h.add 0 n).inv.app X = CategoryTheory.CategoryStruct.comp ((h.F n).map (h.zero.hom.app X)) (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>h : CategoryTheory.ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(h.add n 0).inv.app X = CategoryTheory.CategoryStruct.comp (h.zero.hom.app ((h.F n).obj X)) (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>h : CategoryTheory.ShiftMkCore C A<GOAL>CategoryTheory.HasShift.shift.toFunctor = CategoryTheory.Discrete.functor h.F
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>h : CategoryTheory.ShiftMkCore C A<VAR>m n : CategoryTheory.Discrete A<GOAL>CategoryTheory.HasShift.shift.μ m n = (h.add m.as n.as).inv
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>h : CategoryTheory.ShiftMkCore C A<GOAL>CategoryTheory.HasShift.shift.ε = h.zero.inv
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>i j : A<GOAL>CategoryTheory.shiftFunctorAdd' C i j (i + j) ⋯ = CategoryTheory.shiftFunctorAdd C i j
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>h : CategoryTheory.ShiftMkCore C A<VAR>a : A<GOAL>CategoryTheory.shiftFunctor C a = h.F a
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>h : CategoryTheory.ShiftMkCore C A<GOAL>CategoryTheory.shiftFunctorZero C A = h.zero
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>h : CategoryTheory.ShiftMkCore C A<VAR>a b : A<GOAL>CategoryTheory.shiftFunctorAdd C a b = h.add a b
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<GOAL>CategoryTheory.shiftFunctorAdd' C 0 a a ⋯ = (CategoryTheory.shiftFunctor C a).leftUnitor.symm ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C A).symm (CategoryTheory.shiftFunctor C a)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<GOAL>CategoryTheory.shiftFunctorAdd' C a 0 a ⋯ = (CategoryTheory.shiftFunctor C a).rightUnitor.symm ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C a) (CategoryTheory.shiftFunctorZero C A).symm
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A<VAR>h₁₂ : a₁ + a₂ = a₁₂<VAR>h₂₃ : a₂ + a₃ = a₂₃<VAR>h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃<GOAL>CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯ ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) (CategoryTheory.shiftFunctor C a₃) ≪≫ (CategoryTheory.shiftFunctor C a₁).associator (CategoryTheory.shiftFunctor C a₂) (CategoryTheory.shiftFunctor C a₃) = CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯ ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C a₁) (CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a₁ a₂ a₃ : A<GOAL>CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C a₁ a₂) (CategoryTheory.shiftFunctor C a₃) ≪≫ (CategoryTheory.shiftFunctor C a₁).associator (CategoryTheory.shiftFunctor C a₂) (CategoryTheory.shiftFunctor C a₃) = CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C a₁) (CategoryTheory.shiftFunctorAdd C a₂ a₃)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd' C 0 a a ⋯).hom.app X = (CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).inv.app X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd C 0 a).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd' C 0 a a ⋯).inv.app X = (CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).hom.app X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd C 0 a).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).hom.app X)) (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd' C a 0 a ⋯).hom.app X = (CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C a).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd C a 0).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C a).obj X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd' C a 0 a ⋯).inv.app X = (CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd C a 0).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A<VAR>h₁₂ : a₁ + a₂ = a₁₂<VAR>h₂₃ : a₂ + a₃ = a₂₃<VAR>h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).hom.app X) ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).hom.app X) ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A<VAR>h₁₂ : a₁ + a₂ = a₁₂<VAR>h₂₃ : a₂ + a₃ = a₂₃<VAR>h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)) ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X)) ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X) ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X) ((CategoryTheory.shiftFunctorAdd C a₂ a₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).inv.app X)) ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C a₂ a₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X)) ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).inv.app X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>n : A<VAR>X : C<GOAL>(CategoryTheory.HasShift.shift.obj { as := n }).obj X = (CategoryTheory.shiftFunctor C n).obj X
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>(CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftAdd X i j).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C (i + j)).map f) (CategoryTheory.shiftAdd Y i j).hom)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.shiftFunctor C 0).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftZero A X).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.shiftZero A Y).inv)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>i j : A<VAR>h : i + j = 0<GOAL>(CategoryTheory.shiftEquiv' C i j h).functor = CategoryTheory.shiftFunctor C i
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>i j : A<VAR>h : i + j = 0<GOAL>(CategoryTheory.shiftEquiv' C i j h).unitIso = (CategoryTheory.shiftFunctorCompIsoId C i j h).symm
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>i j : A<VAR>h : i + j = 0<GOAL>(CategoryTheory.shiftEquiv' C i j h).inverse = CategoryTheory.shiftFunctor C j
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>i j : A<VAR>h : i + j = 0<GOAL>(CategoryTheory.shiftEquiv' C i j h).counitIso = CategoryTheory.shiftFunctorCompIsoId C j i ⋯
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : A<GOAL>(CategoryTheory.shiftFunctor C (-i)).map ((CategoryTheory.shiftFunctor C i).map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i (-i) ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C i (-i) ⋯).inv.app Y))