ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<GOAL>Nat.card (CategoryTheory.Aut A) ≤ Nat.card ↑(F.obj A)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>self : CategoryTheory.GaloisCategory C<GOAL>∃ F, Nonempty (CategoryTheory.PreGaloisCategory.FiberFunctor F)
<VAR>X : Type u<VAR>Y : Type v<VAR>Preorder X<VAR>Preorder Y<VAR>L : CategoryTheory.Functor X Y<VAR>R : CategoryTheory.Functor Y X<VAR>adj : L ⊣ R<GOAL>GaloisConnection L.obj R.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D<VAR>c : C<VAR>d : D<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.evaluationLeftAdjoint D c).obj d).map f = CategoryTheory.Limits.Sigma.desc fun g => CategoryTheory.Limits.Sigma.ι (fun x => d) (CategoryTheory.CategoryStruct.comp g f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D<VAR>c : C<VAR>d : D<VAR>t : C<GOAL>((CategoryTheory.evaluationLeftAdjoint D c).obj d).obj t = ∐ fun x => d
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D<VAR>c : C<GOAL>∀ {x d₂ : D} (f : x ⟶ d₂) (e : C), ((CategoryTheory.evaluationLeftAdjoint D c).map f).app e = CategoryTheory.Limits.Sigma.desc fun h => CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Sigma.ι (fun x => d₂) h)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D<VAR>c : C<VAR>Y : CategoryTheory.Functor C D<VAR>e : C<GOAL>((CategoryTheory.evaluationAdjunctionRight D c).counit.app Y).app e = CategoryTheory.Limits.Sigma.desc fun h => Y.map h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D<VAR>c : C<VAR>X : D<GOAL>(CategoryTheory.evaluationAdjunctionRight D c).unit.app X = CategoryTheory.Limits.Sigma.ι (fun x => X) (CategoryTheory.CategoryStruct.id c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D<VAR>F G : CategoryTheory.Functor C D<VAR>η : F ⟶ G<GOAL>CategoryTheory.Mono η ↔ ∀ (c : C), CategoryTheory.Mono (η.app c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D<VAR>c : C<GOAL>∀ {X Y : D} (f : X ⟶ Y) (t : C), ((CategoryTheory.evaluationRightAdjoint D c).map f).app t = CategoryTheory.Limits.Pi.lift fun g => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) g) f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D<VAR>c : C<VAR>d : D<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.evaluationRightAdjoint D c).obj d).map f = CategoryTheory.Limits.Pi.lift fun g => CategoryTheory.Limits.Pi.π (fun x => d) (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D<VAR>c : C<VAR>d : D<VAR>t : C<GOAL>((CategoryTheory.evaluationRightAdjoint D c).obj d).obj t = ∏ᶜ fun x => d
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D<VAR>c : C<VAR>Y : D<GOAL>(CategoryTheory.evaluationAdjunctionLeft D c).counit.app Y = CategoryTheory.Limits.Pi.π (fun x => Y) (CategoryTheory.CategoryStruct.id c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D<VAR>c : C<VAR>X : CategoryTheory.Functor C D<VAR>t : C<GOAL>((CategoryTheory.evaluationAdjunctionLeft D c).unit.app X).app t = CategoryTheory.Limits.Pi.lift fun g => X.map g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D<VAR>F G : CategoryTheory.Functor C D<VAR>η : F ⟶ G<GOAL>CategoryTheory.Epi η ↔ ∀ (c : C), CategoryTheory.Epi (η.app c)
<VAR>obj : Type u<VAR>self : CategoryTheory.Category.{v, u} obj<VAR>W X Y Z : obj<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
<VAR>obj : Type u<VAR>self : CategoryTheory.Category.{v, u} obj<VAR>X Y : obj<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
<VAR>obj : Type u<VAR>self : CategoryTheory.Category.{v, u} obj<VAR>X Y : obj<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>w : f = g<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<VAR>w : g = h<GOAL>CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : ∀ {Z : C} (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Y Z : C<VAR>f g : Y ⟶ Z<VAR>w : ∀ {X : C} (h : X ⟶ Y), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : (fun {Z} h => CategoryTheory.CategoryStruct.comp f h) = fun {Z} h => CategoryTheory.CategoryStruct.comp g h<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Y Z : C<VAR>f g : Y ⟶ Z<VAR>w : (fun {X} h => CategoryTheory.CategoryStruct.comp h f) = fun {X} h => CategoryTheory.CategoryStruct.comp h g<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f : X ⟶ X<VAR>w : ∀ {Y : C} (g : X ⟶ Y), CategoryTheory.CategoryStruct.comp f g = g<GOAL>f = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f : X ⟶ X<VAR>w : ∀ {Y : C} (g : Y ⟶ X), CategoryTheory.CategoryStruct.comp g f = g<GOAL>f = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : Prop<VAR>Decidable P<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g g' : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f (if P then g else g') = if P then CategoryTheory.CategoryStruct.comp f g else CategoryTheory.CategoryStruct.comp f g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : Prop<VAR>Decidable P<VAR>X Y Z : C<VAR>f f' : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (if P then f else f') g = if P then CategoryTheory.CategoryStruct.comp f g else CategoryTheory.CategoryStruct.comp f' g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : Prop<VAR>Decidable P<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : P → (Y ⟶ Z)<VAR>g' : ¬P → (Y ⟶ Z)<GOAL>CategoryTheory.CategoryStruct.comp f (if h : P then g h else g' h) = if h : P then CategoryTheory.CategoryStruct.comp f (g h) else CategoryTheory.CategoryStruct.comp f (g' h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : Prop<VAR>Decidable P<VAR>X Y Z : C<VAR>f : P → (X ⟶ Y)<VAR>f' : ¬P → (X ⟶ Y)<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (if h : P then f h else f' h) g = if h : P then CategoryTheory.CategoryStruct.comp (f h) g else CategoryTheory.CategoryStruct.comp (f' h) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.Epi f<VAR>Z : C<VAR>g h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h → g = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.Mono f<VAR>Z : C<VAR>g h : Z ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f → g = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>g h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h ↔ g = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>g h : Z ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f ↔ g = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>h : Y ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f h = f ↔ h = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>g : X ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp g f = f ↔ g = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Epi g<GOAL>CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Mono g<GOAL>CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp f g)<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : X ⟶ Z<VAR>CategoryTheory.Mono h<VAR>w : CategoryTheory.CategoryStruct.comp f g = h<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)<GOAL>CategoryTheory.Epi g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : X ⟶ Z<VAR>CategoryTheory.Epi h<VAR>w : CategoryTheory.CategoryStruct.comp f g = h<GOAL>CategoryTheory.Epi g
<GOAL>∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y), CategoryTheory.Quiv.forget.map F = F.toPrefunctor
<VAR>C : CategoryTheory.Cat<GOAL>CategoryTheory.Quiv.forget.obj C = CategoryTheory.Quiv.of ↑C
<GOAL>∀ {X Y : CategoryTheory.Quiv} (F : X ⟶ Y) {X_1 Y_1 : ↑((fun V => CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)) X)} (f : X_1 ⟶ Y_1), (CategoryTheory.Cat.free.map F).map f = Prefunctor.mapPath F f
<VAR>V : CategoryTheory.Quiv<GOAL>CategoryTheory.Cat.free.obj V = CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)
<GOAL>∀ {X Y : CategoryTheory.Quiv} (F : X ⟶ Y) (X_1 : ↑((fun V => CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)) X)), (CategoryTheory.Cat.free.map F).obj X_1 = F.obj X_1
<VAR>V : Type u<VAR>Quiver V<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F : V ⥤q C<GOAL>∀ {X Y : CategoryTheory.Paths V} (f : X ⟶ Y), (CategoryTheory.Quiv.lift F).map f = CategoryTheory.composePath (F.mapPath f)
<VAR>V : Type u<VAR>Quiver V<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F : V ⥤q C<VAR>X : CategoryTheory.Paths V<GOAL>(CategoryTheory.Quiv.lift F).obj X = F.obj X
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<GOAL>↑(CategoryTheory.Grpd.of C) = C
<VAR>C D E : CategoryTheory.Grpd<VAR>f : C ⟶ D<VAR>g : D ⟶ E<GOAL>CategoryTheory.CategoryStruct.comp f g = CategoryTheory.Functor.comp f g
<VAR>C : CategoryTheory.Grpd<GOAL>CategoryTheory.Functor.id ↑C = CategoryTheory.CategoryStruct.id C
<VAR>J : Type u<VAR>f : J → CategoryTheory.Grpd<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Grpd.piIsoPi J f).hom (CategoryTheory.Limits.Pi.π f j) = CategoryTheory.Pi.eval (fun i => ↑(f i)) j
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>self : CategoryTheory.Limits.Bicone F<VAR>j j' : J<GOAL>self.ι j ≫ self.π j' = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<VAR>j : J<GOAL>B.ι j ≫ B.π j = 𝟙 (F j)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<VAR>j j' : J<VAR>h : j ≠ j'<GOAL>B.ι j ≫ B.π j' = 0
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>A B : CategoryTheory.Limits.Bicone F<VAR>self : CategoryTheory.Limits.BiconeMorphism A B<VAR>j : J<GOAL>A.ι j ≫ self.hom = B.ι j
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>A B : CategoryTheory.Limits.Bicone F<VAR>self : CategoryTheory.Limits.BiconeMorphism A B<VAR>j : J<GOAL>self.hom ≫ B.π j = A.π j
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<GOAL>(𝟙 B).hom = 𝟙 B.pt
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<GOAL>∀ {X Y Z : CategoryTheory.Limits.Bicone F} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g).hom = f.hom ≫ g.hom
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>c c' : CategoryTheory.Limits.Bicone F<VAR>f g : c ⟶ c'<VAR>w : f.hom = g.hom<GOAL>f = g
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>c c' : CategoryTheory.Limits.Bicone F<VAR>φ : c.pt ≅ c'.pt<VAR>wι : ∀ (j : J), c.ι j ≫ φ.hom = c'.ι j := by aesop_cat<VAR>wπ : ∀ (j : J), φ.hom ≫ c'.π j = c.π j := by aesop_cat<GOAL>(CategoryTheory.Limits.Bicones.ext φ wι wπ).inv.hom = φ.inv
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>c c' : CategoryTheory.Limits.Bicone F<VAR>φ : c.pt ≅ c'.pt<VAR>wι : ∀ (j : J), c.ι j ≫ φ.hom = c'.ι j := by aesop_cat<VAR>wπ : ∀ (j : J), φ.hom ≫ c'.π j = c.π j := by aesop_cat<GOAL>(CategoryTheory.Limits.Bicones.ext φ wι wπ).hom.hom = φ.hom
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : J → C<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>A : CategoryTheory.Limits.Bicone F<VAR>j : J<GOAL>((CategoryTheory.Limits.Bicones.functoriality F G).obj A).π j = G.map (A.π j)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : J → C<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>A : CategoryTheory.Limits.Bicone F<VAR>j : J<GOAL>((CategoryTheory.Limits.Bicones.functoriality F G).obj A).ι j = G.map (A.ι j)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : J → C<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<GOAL>∀ {X Y : CategoryTheory.Limits.Bicone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Bicones.functoriality F G).map f).hom = G.map f.hom
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : J → C<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>A : CategoryTheory.Limits.Bicone F<GOAL>((CategoryTheory.Limits.Bicones.functoriality F G).obj A).pt = G.obj A.pt
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<GOAL>B.toCone.pt = B.pt
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<VAR>j : CategoryTheory.Discrete J<GOAL>B.toCone.π.app j = B.π j.as
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<VAR>j : J<GOAL>B.toCone.π.app { as := j } = B.π j
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<VAR>j : J<GOAL>CategoryTheory.Limits.Fan.proj B.toCone j = B.π j
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<GOAL>B.toCocone.pt = B.pt
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<VAR>j : CategoryTheory.Discrete J<GOAL>B.toCocone.ι.app j = B.ι j.as
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<VAR>j : J<GOAL>CategoryTheory.Limits.Cofan.inj B.toCocone j = B.ι j
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>B : CategoryTheory.Limits.Bicone F<VAR>j : J<GOAL>B.toCocone.ι.app { as := j } = B.ι j
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)<VAR>ht : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.Bicone.ofLimitCone ht).pt = t.pt
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>j : J<GOAL>(CategoryTheory.Limits.Bicone.ofLimitCone ht).ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>j : J<GOAL>(CategoryTheory.Limits.Bicone.ofLimitCone ht).π j = t.π.app { as := j }
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>t : CategoryTheory.Limits.Bicone f<VAR>ht : CategoryTheory.Limits.IsLimit t.toCone<VAR>j : J<GOAL>t.ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>j : J<GOAL>(CategoryTheory.Limits.Bicone.ofColimitCocone ht).ι j = t.ι.app { as := j }
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>j : J<GOAL>(CategoryTheory.Limits.Bicone.ofColimitCocone ht).π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)<VAR>ht : CategoryTheory.Limits.IsColimit t<GOAL>(CategoryTheory.Limits.Bicone.ofColimitCocone ht).pt = t.pt
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>t : CategoryTheory.Limits.Bicone f<VAR>ht : CategoryTheory.Limits.IsColimit t.toCocone<VAR>j : J<GOAL>t.π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type w'<VAR>f : J → C<VAR>c : CategoryTheory.Limits.Bicone f<VAR>g : K ≃ J<VAR>k : K<GOAL>(c.whisker g).π k = c.π (g k)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type w'<VAR>f : J → C<VAR>c : CategoryTheory.Limits.Bicone f<VAR>g : K ≃ J<GOAL>(c.whisker g).pt = c.pt
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type w'<VAR>f : J → C<VAR>c : CategoryTheory.Limits.Bicone f<VAR>g : K ≃ J<VAR>k : K<GOAL>(c.whisker g).ι k = c.ι (g k)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>self : CategoryTheory.Limits.HasBiproduct F<GOAL>Nonempty (CategoryTheory.Limits.LimitBicone F)
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : J → C<VAR>d : CategoryTheory.Limits.LimitBicone F<GOAL>CategoryTheory.Limits.HasBiproduct F
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>self : CategoryTheory.Limits.HasBiproductsOfShape J C<VAR>F : J → C<GOAL>CategoryTheory.Limits.HasBiproduct F
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>self : CategoryTheory.Limits.HasFiniteBiproducts C<VAR>n : ℕ<GOAL>CategoryTheory.Limits.HasBiproductsOfShape (Fin n) C
<VAR>J : Type w<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type w'<VAR>CategoryTheory.Limits.HasBiproductsOfShape K C<VAR>e : J ≃ K<GOAL>CategoryTheory.Limits.HasBiproductsOfShape J C
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>b : J<GOAL>(CategoryTheory.Limits.biproduct.bicone f).π b = CategoryTheory.Limits.biproduct.π f b
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>b : J<GOAL>(CategoryTheory.Limits.biproduct.bicone f).ι b = CategoryTheory.Limits.biproduct.ι f b
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>DecidableEq J<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>j j' : J<GOAL>CategoryTheory.Limits.biproduct.ι f j ≫ CategoryTheory.Limits.biproduct.π f j' = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>j : J<GOAL>CategoryTheory.Limits.biproduct.ι f j ≫ CategoryTheory.Limits.biproduct.π f j = 𝟙 (f j)