ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>D₃ : Type u_6<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_9, u_2} C₂<VAR>CategoryTheory.Category.{u_10, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} D₁<VAR>CategoryTheory.Category.{u_12, u_5} D₂<VAR>CategoryTheory.Category.{u_13, u_6} D₃<VAR>F₁₂ : CategoryTheory.Functor C₁ C₂<VAR>F₂₃ : CategoryTheory.Functor C₂ C₃<VAR>F₁₃ : CategoryTheory.Functor C₁ C₃<VAR>α : F₁₃ ⟶ F₁₂.comp F₂₃<VAR>G₁₂ : CategoryTheory.Functor D₁ D₂<VAR>G₂₃ : CategoryTheory.Functor D₂ D₃<VAR>G₁₃ : CategoryTheory.Functor D₁ D₃<VAR>β : G₁₂.comp G₂₃ ⟶ G₁₃<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₃ : CategoryTheory.Functor C₃ D₃<VAR>e₁₂ : F₁₂.comp L₂ ⟶ L₁.comp G₁₂<VAR>e₂₃ : F₂₃.comp L₃ ⟶ L₂.comp G₂₃<VAR>e₁₃ : F₁₃.comp L₃ ⟶ L₁.comp G₁₃<VAR>A : Type u_7<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C₁ A<VAR>CategoryTheory.HasShift C₂ A<VAR>CategoryTheory.HasShift C₃ A<VAR>CategoryTheory.HasShift D₁ A<VAR>CategoryTheory.HasShift D₂ A<VAR>CategoryTheory.HasShift D₃ A<VAR>F₁₂.CommShift A<VAR>F₂₃.CommShift A<VAR>F₁₃.CommShift A<VAR>CategoryTheory.NatTrans.CommShift α A<VAR>G₁₂.CommShift A<VAR>G₂₃.CommShift A<VAR>G₁₃.CommShift A<VAR>CategoryTheory.NatTrans.CommShift β A<VAR>L₁.CommShift A<VAR>L₂.CommShift A<VAR>L₃.CommShift A<VAR>CategoryTheory.NatTrans.CommShift e₁₂ A<VAR>CategoryTheory.NatTrans.CommShift e₂₃ A<VAR>h₁₃ : e₁₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α L₃) (CategoryTheory.CategoryStruct.comp (F₁₂.associator F₂₃ L₃).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F₁₂ e₂₃) (CategoryTheory.CategoryStruct.comp (F₁₂.associator L₂ G₂₃).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e₁₂ G₂₃) (CategoryTheory.CategoryStruct.comp (L₁.associator G₁₂ G₂₃).hom (CategoryTheory.whiskerLeft L₁ β))))))<GOAL>CategoryTheory.NatTrans.CommShift e₁₃ A
<VAR>C : Type u_5<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_5} C<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_3<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>X : C<GOAL>(CategoryTheory.HasShift.Induced.zero F s i).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_4} C<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>X : C<GOAL>(CategoryTheory.HasShift.Induced.zero F s i).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorZero C A).inv.app X)) ((i 0).inv.app X)
<VAR>C : Type u_5<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_5} C<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_3<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>a b : A<VAR>X : C<GOAL>(CategoryTheory.HasShift.Induced.add F s i a b).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)) ((s b).map ((i a).inv.app X))))
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_4} C<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>a b : A<VAR>X : C<GOAL>(CategoryTheory.HasShift.Induced.add F s i a b).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X)) ((i (a + b)).inv.app X)))
<VAR>C : Type u_4<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_3<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>a : A<GOAL>CategoryTheory.shiftFunctor D a = s a
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_3<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_4} C<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorZero C A).inv.app X)) ((i 0).inv.app X)
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_3<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>a b : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)) ((s b).map ((i a).inv.app X))))
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_3<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>a b : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X) = CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X)) ((i (a + b)).inv.app X)))
<VAR>C : Type u_1<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_2, u_3} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>s : A → CategoryTheory.Functor D D<VAR>i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Full<VAR>((CategoryTheory.whiskeringLeft C D D).obj F).Faithful<VAR>a : A<GOAL>F.commShiftIso a = (i a).symm
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>(CategoryTheory.Limits.zeroProdIso X).hom = CategoryTheory.Limits.prod.snd
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>(CategoryTheory.Limits.zeroProdIso X).inv ≫ CategoryTheory.Limits.prod.snd = 𝟙 X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>(CategoryTheory.Limits.prodZeroIso X).hom = CategoryTheory.Limits.prod.fst
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>(CategoryTheory.Limits.prodZeroIso X).inv ≫ CategoryTheory.Limits.prod.fst = 𝟙 X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.Limits.coprod.inr ≫ (CategoryTheory.Limits.zeroCoprodIso X).hom = 𝟙 X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>(CategoryTheory.Limits.zeroCoprodIso X).inv = CategoryTheory.Limits.coprod.inr
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.Limits.coprod.inl ≫ (CategoryTheory.Limits.coprodZeroIso X).hom = 𝟙 X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>(CategoryTheory.Limits.coprodZeroIso X).inv = CategoryTheory.Limits.coprod.inl
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<GOAL>(CategoryTheory.Limits.pullbackZeroZeroIso X Y).inv ≫ CategoryTheory.Limits.pullback.fst 0 0 = CategoryTheory.Limits.prod.fst
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<GOAL>(CategoryTheory.Limits.pullbackZeroZeroIso X Y).inv ≫ CategoryTheory.Limits.pullback.snd 0 0 = CategoryTheory.Limits.prod.snd
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<GOAL>(CategoryTheory.Limits.pullbackZeroZeroIso X Y).hom ≫ CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.pullback.fst 0 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<GOAL>(CategoryTheory.Limits.pullbackZeroZeroIso X Y).hom ≫ CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.pullback.snd 0 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<GOAL>CategoryTheory.Limits.pushout.inl 0 0 ≫ (CategoryTheory.Limits.pushoutZeroZeroIso X Y).hom = CategoryTheory.Limits.coprod.inl
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<GOAL>CategoryTheory.Limits.pushout.inr 0 0 ≫ (CategoryTheory.Limits.pushoutZeroZeroIso X Y).hom = CategoryTheory.Limits.coprod.inr
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<GOAL>CategoryTheory.Limits.coprod.inl ≫ (CategoryTheory.Limits.pushoutZeroZeroIso X Y).inv = CategoryTheory.Limits.pushout.inl 0 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<GOAL>CategoryTheory.Limits.coprod.inr ≫ (CategoryTheory.Limits.pushoutZeroZeroIso X Y).inv = CategoryTheory.Limits.pushout.inr 0 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>α : Type w<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>F : CategoryTheory.Discrete α ⥤ C<GOAL>∀ {x Y : Finset (CategoryTheory.Discrete α)} (h : x ⟶ Y), (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset F).map h = CategoryTheory.Limits.Sigma.desc fun y => CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>α : Type w<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>F : CategoryTheory.Discrete α ⥤ C<VAR>s : Finset (CategoryTheory.Discrete α)<GOAL>(CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset F).obj s = ∐ fun x => F.obj ↑x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>α : Type w<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C<VAR>F : CategoryTheory.Discrete α ⥤ C<VAR>j : CategoryTheory.Discrete α<GOAL>(CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).cocone.ι.app j = CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩ ≫ CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset F) {j}
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>α : Type w<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C<VAR>F : CategoryTheory.Discrete α ⥤ C<GOAL>(CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).cocone.pt = CategoryTheory.Limits.colimit (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>α : Type w<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C<VAR>F : CategoryTheory.Discrete α ⥤ C<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).isColimit.desc s = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset F) { pt := s.pt, ι := { app := fun t => CategoryTheory.Limits.Sigma.desc fun x => s.ι.app ↑x, naturality := ⋯ } }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C<GOAL>CategoryTheory.Limits.HasCoproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteColimits C<VAR>CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C<GOAL>CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C<GOAL>CategoryTheory.Limits.HasProducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteLimits C<VAR>CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>self : CategoryTheory.FinallySmall J<GOAL>∃ S x F, F.Final
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>S : Type w<VAR>CategoryTheory.SmallCategory S<VAR>F : S ⥤ J<VAR>F.Final<GOAL>CategoryTheory.FinallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.EssentiallySmall.{w, v, u} J<GOAL>CategoryTheory.FinallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} K<VAR>F : K ⥤ J<VAR>F.Final<VAR>CategoryTheory.FinallySmall K<GOAL>CategoryTheory.FinallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} K<VAR>F : K ⥤ J<VAR>F.Final<VAR>CategoryTheory.EssentiallySmall.{w, v₁, u₁} K<GOAL>CategoryTheory.FinallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>self : CategoryTheory.InitiallySmall J<GOAL>∃ S x F, F.Initial
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>S : Type w<VAR>CategoryTheory.SmallCategory S<VAR>F : S ⥤ J<VAR>F.Initial<GOAL>CategoryTheory.InitiallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.EssentiallySmall.{w, v, u} J<GOAL>CategoryTheory.InitiallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} K<VAR>F : K ⥤ J<VAR>F.Initial<VAR>CategoryTheory.InitiallySmall K<GOAL>CategoryTheory.InitiallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} K<VAR>F : K ⥤ J<VAR>F.Initial<VAR>CategoryTheory.EssentiallySmall.{w, v₁, u₁} K<GOAL>CategoryTheory.InitiallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.FinallySmall J<GOAL>∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.IsFilteredOrEmpty J<VAR>s : Set J<VAR>Small.{v, u} ↑s<VAR>hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)<GOAL>CategoryTheory.FinallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.IsFilteredOrEmpty J<GOAL>CategoryTheory.FinallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.InitiallySmall J<GOAL>∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>s : Set J<VAR>Small.{v, u} ↑s<VAR>hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)<GOAL>CategoryTheory.InitiallySmall J
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.IsCofilteredOrEmpty J<GOAL>CategoryTheory.InitiallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.FinallySmall J<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasColimitsOfSize.{w, w, v₁, u₁} C<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.InitiallySmall J<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasLimitsOfSize.{w, w, v₁, u₁} C<GOAL>CategoryTheory.Limits.HasLimitsOfShape J C
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.prod.fst ≫ f) (CategoryTheory.Limits.prod.snd ≫ g))<GOAL>CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasEqualizers C<GOAL>CategoryTheory.Limits.HasPullbacks C
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair Y Z)<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair (f ≫ CategoryTheory.Limits.coprod.inl) (g ≫ CategoryTheory.Limits.coprod.inr))<GOAL>CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasCoequalizers C<GOAL>CategoryTheory.Limits.HasPushouts C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ₑ D<GOAL>(CategoryTheory.LeftExactFunctor.ofExact C D).obj F = { obj := F.obj, property := ⋯ }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ₑ D<GOAL>(CategoryTheory.RightExactFunctor.ofExact C D).obj F = { obj := F.obj, property := ⋯ }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ₑ D<VAR>α : F ⟶ G<GOAL>(CategoryTheory.LeftExactFunctor.ofExact C D).map α = α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ₑ D<VAR>α : F ⟶ G<GOAL>(CategoryTheory.RightExactFunctor.ofExact C D).map α = α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ₗ D<GOAL>(CategoryTheory.LeftExactFunctor.forget C D).obj F = F.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ᵣ D<GOAL>(CategoryTheory.RightExactFunctor.forget C D).obj F = F.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ₑ D<GOAL>(CategoryTheory.ExactFunctor.forget C D).obj F = F.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ₗ D<VAR>α : F ⟶ G<GOAL>(CategoryTheory.LeftExactFunctor.forget C D).map α = α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ᵣ D<VAR>α : F ⟶ G<GOAL>(CategoryTheory.RightExactFunctor.forget C D).map α = α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ₑ D<VAR>α : F ⟶ G<GOAL>(CategoryTheory.ExactFunctor.forget C D).map α = α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<GOAL>(CategoryTheory.LeftExactFunctor.of F).obj = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesFiniteColimits F<GOAL>(CategoryTheory.RightExactFunctor.of F).obj = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<VAR>CategoryTheory.Limits.PreservesFiniteColimits F<GOAL>(CategoryTheory.ExactFunctor.of F).obj = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<GOAL>(CategoryTheory.LeftExactFunctor.forget C D).obj (CategoryTheory.LeftExactFunctor.of F) = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesFiniteColimits F<GOAL>(CategoryTheory.RightExactFunctor.forget C D).obj (CategoryTheory.RightExactFunctor.of F) = F