ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>∀ (X_1 : C), ((CategoryTheory.Over.star X).obj X_1).hom = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>∀ {X_1 Y : C} (f : X_1 ⟶ Y), ((CategoryTheory.Over.star X).map f).left = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x : CategoryTheory.Under X<GOAL>(CategoryTheory.Under.pushout f).obj x = CategoryTheory.Under.mk (CategoryTheory.Limits.pushout.inr x.hom f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x : CategoryTheory.Under X<VAR>x' : CategoryTheory.Under X<VAR>u : x ⟶ x'<GOAL>(CategoryTheory.Under.pushout f).map u = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.comp u.right (CategoryTheory.Limits.pushout.inl x'.hom f)) (CategoryTheory.Limits.pushout.inr x'.hom f) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>∀ (Y_1 : CategoryTheory.Under Y), (CategoryTheory.Under.mapPushoutAdj f).counit.app Y_1 = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.id Y_1.right) Y_1.hom ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>∀ (X_1 : CategoryTheory.Under X), (CategoryTheory.Under.mapPushoutAdj f).unit.app X_1 = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.inl X_1.hom f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<GOAL>CategoryTheory.IsPreconnected C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofilteredOrEmpty C<GOAL>CategoryTheory.IsPreconnected C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFiltered C<GOAL>CategoryTheory.IsConnected C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofiltered C<GOAL>CategoryTheory.IsConnected C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>α : Type w<VAR>f : α → C<GOAL>Small.{max v w, u} (CategoryTheory.FullSubcategory (CategoryTheory.IsFiltered.FilteredClosure f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofilteredOrEmpty C<VAR>α : Type w<VAR>f : α → C<GOAL>Small.{max v w, u} (CategoryTheory.FullSubcategory (CategoryTheory.IsCofiltered.CofilteredClosure f))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>X : C<VAR>self : CategoryTheory.PreGaloisCategory.IsGalois X<GOAL>Nonempty (CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>X : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected X<GOAL>CategoryTheory.PreGaloisCategory.IsGalois X ↔ Nonempty (CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected X<GOAL>CategoryTheory.PreGaloisCategory.IsGalois X ↔ MulAction.IsPretransitive (CategoryTheory.Aut X) ↑(F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A : C<VAR>CategoryTheory.PreGaloisCategory.IsGalois A<VAR>a : ↑(F.obj A)<GOAL>Function.Surjective fun f => F.map f.hom a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A : C<VAR>CategoryTheory.PreGaloisCategory.IsGalois A<VAR>a : ↑(F.obj A)<GOAL>Function.Bijective fun f => F.map f.hom a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A : C<VAR>CategoryTheory.PreGaloisCategory.IsGalois A<VAR>a : ↑(F.obj A)<VAR>φ : CategoryTheory.Aut A<GOAL>(CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a) φ = F.map φ.hom a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A : C<VAR>CategoryTheory.PreGaloisCategory.IsGalois A<VAR>a b : ↑(F.obj A)<GOAL>F.map ((CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a).symm b).hom a = b
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>A B : C<VAR>f : A ⟶ B<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>CategoryTheory.PreGaloisCategory.IsGalois B<VAR>σ : CategoryTheory.Aut A<GOAL>∃! τ, CategoryTheory.CategoryStruct.comp f τ.hom = CategoryTheory.CategoryStruct.comp σ.hom f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>A B : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>CategoryTheory.PreGaloisCategory.IsGalois B<VAR>f : A ⟶ B<VAR>σ : CategoryTheory.Aut A<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.PreGaloisCategory.autMap f σ).hom = CategoryTheory.CategoryStruct.comp σ.hom f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A B : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>CategoryTheory.PreGaloisCategory.IsGalois B<VAR>f : A ⟶ B<VAR>σ : CategoryTheory.Aut A<VAR>a : ↑(F.obj A)<GOAL>F.map (CategoryTheory.PreGaloisCategory.autMap f σ).hom (F.map f a) = F.map f (F.map σ.hom a)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>A B : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>CategoryTheory.PreGaloisCategory.IsGalois B<VAR>f : A ⟶ B<VAR>σ : CategoryTheory.Aut A<VAR>τ : CategoryTheory.Aut B<VAR>h : CategoryTheory.CategoryStruct.comp f τ.hom = CategoryTheory.CategoryStruct.comp σ.hom f<GOAL>CategoryTheory.PreGaloisCategory.autMap f σ = τ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>A : C<VAR>CategoryTheory.PreGaloisCategory.IsGalois A<GOAL>CategoryTheory.PreGaloisCategory.autMap (CategoryTheory.CategoryStruct.id A) = id
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>X Y Z : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected X<VAR>CategoryTheory.PreGaloisCategory.IsGalois Y<VAR>CategoryTheory.PreGaloisCategory.IsGalois Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.PreGaloisCategory.autMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.PreGaloisCategory.autMap g ∘ CategoryTheory.PreGaloisCategory.autMap f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>A B : C<VAR>CategoryTheory.PreGaloisCategory.IsGalois A<VAR>CategoryTheory.PreGaloisCategory.IsGalois B<VAR>f : A ⟶ B<GOAL>Function.Surjective (CategoryTheory.PreGaloisCategory.autMap f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>A B : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>CategoryTheory.PreGaloisCategory.IsGalois B<VAR>f : A ⟶ B<VAR>σ τ : CategoryTheory.Aut A<GOAL>CategoryTheory.PreGaloisCategory.autMap f (σ * τ) = CategoryTheory.PreGaloisCategory.autMap f σ * CategoryTheory.PreGaloisCategory.autMap f τ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>A B : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>CategoryTheory.PreGaloisCategory.IsGalois B<VAR>f : A ⟶ B<VAR>σ : CategoryTheory.Aut A<GOAL>(CategoryTheory.PreGaloisCategory.autMapHom f) σ = CategoryTheory.PreGaloisCategory.autMap f σ
<VAR>G : Type u<VAR>Group G<VAR>X : Action FintypeCat (MonCat.of G)<VAR>CategoryTheory.PreGaloisCategory.IsConnected X<GOAL>MulAction.IsPretransitive G ↑X.V
<VAR>G : Type u<VAR>Group G<VAR>X : FintypeCat<VAR>MulAction G ↑X<VAR>MulAction.IsPretransitive G ↑X<VAR>h : Nonempty ↑X<GOAL>CategoryTheory.PreGaloisCategory.IsConnected (Action.FintypeCat.ofMulAction G X)
<VAR>G : Type u<VAR>Group G<VAR>X : Action FintypeCat (MonCat.of G)<VAR>Nonempty ↑X.V<GOAL>CategoryTheory.PreGaloisCategory.IsConnected X ↔ MulAction.IsPretransitive G ↑X.V
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C × D ⥤ E<VAR>X : C<VAR>Y : D<GOAL>F.map (𝟙 X, 𝟙 Y) = 𝟙 (F.obj (X, Y))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C × D ⥤ E<VAR>W : C<VAR>X Y Z : D<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>F.map (𝟙 W, f ≫ g) = F.map (𝟙 W, f) ≫ F.map (𝟙 W, g)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C × D ⥤ E<VAR>X Y Z : C<VAR>W : D<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>F.map (f ≫ g, 𝟙 W) = F.map (f, 𝟙 W) ≫ F.map (g, 𝟙 W)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C × D ⥤ E<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Y' : D<VAR>g : Y ⟶ Y'<GOAL>F.map (𝟙 X, g) ≫ F.map (f, 𝟙 Y') = F.map (f, g)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C × D ⥤ E<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Y' : D<VAR>g : Y ⟶ Y'<GOAL>F.map (f, 𝟙 Y) ≫ F.map (𝟙 X', g) = F.map (f, g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Discrete PUnit.{w + 1} × C<GOAL>(CategoryTheory.prod.leftUnitor C).obj X = X.2
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Discrete PUnit.{w + 1} × C} (f : X ⟶ Y), (CategoryTheory.prod.leftUnitor C).map f = f.2
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C × CategoryTheory.Discrete PUnit.{w + 1}<GOAL>(CategoryTheory.prod.rightUnitor C).obj X = X.1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : C × CategoryTheory.Discrete PUnit.{w + 1}} (f : X ⟶ Y), (CategoryTheory.prod.rightUnitor C).map f = f.1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(CategoryTheory.prod.leftInverseUnitor C).obj X = ({ as := PUnit.unit }, X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.prod.leftInverseUnitor C).map f = (𝟙 ((fun X => ({ as := PUnit.unit }, X)) X).1, f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.prod.rightInverseUnitor C).map f = (f, 𝟙 ((fun X => (X, { as := PUnit.unit })) X).2)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(CategoryTheory.prod.rightInverseUnitor C).obj X = (X, { as := PUnit.unit })
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.prod.leftUnitorEquivalence C).functor = CategoryTheory.prod.leftUnitor C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.prod.leftUnitorEquivalence C).inverse = CategoryTheory.prod.leftInverseUnitor C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.prod.leftUnitorEquivalence C).counitIso = CategoryTheory.Iso.refl (CategoryTheory.prod.leftInverseUnitor C ⋙ CategoryTheory.prod.leftUnitor C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.prod.leftUnitorEquivalence C).unitIso = CategoryTheory.Iso.refl (𝟭 (CategoryTheory.Discrete PUnit.{w + 1} × C))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.prod.rightUnitorEquivalence C).unitIso = CategoryTheory.Iso.refl (𝟭 (C × CategoryTheory.Discrete PUnit.{w + 1}))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.prod.rightUnitorEquivalence C).counitIso = CategoryTheory.Iso.refl (CategoryTheory.prod.rightInverseUnitor C ⋙ CategoryTheory.prod.rightUnitor C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.prod.rightUnitorEquivalence C).functor = CategoryTheory.prod.rightUnitor C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.prod.rightUnitorEquivalence C).inverse = CategoryTheory.prod.rightInverseUnitor C
<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>self : F.Final<VAR>d : D<GOAL>CategoryTheory.IsConnected (CategoryTheory.StructuredArrow d 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>self : F.Initial<VAR>d : D<GOAL>CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow F d)
<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>F.op.Initial<GOAL>F.Final
<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>F.op.Final<GOAL>F.Initial
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>adj : L ⊣ R<GOAL>R.Final
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>adj : L ⊣ R<GOAL>L.Initial
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>F.Final<VAR>i : F ≅ F'<GOAL>F'.Final
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>i : F ≅ F'<GOAL>F.Final ↔ F'.Final
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>F.Initial<VAR>i : F ≅ F'<GOAL>F'.Initial
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>i : F ≅ F'<GOAL>F.Initial ↔ F'.Initial
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>c : CategoryTheory.Limits.Cocone (F.comp G)<GOAL>(CategoryTheory.Functor.Final.extendCocone.obj c).pt = c.pt
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>c : CategoryTheory.Limits.Cocone (F.comp G)<VAR>X : D<GOAL>(CategoryTheory.Functor.Final.extendCocone.obj c).ι.app X = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.Final.homToLift F X)) (c.ι.app (CategoryTheory.Functor.Final.lift F X))
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>∀ {X Y : CategoryTheory.Limits.Cocone (F.comp G)} (f : X ⟶ Y), (CategoryTheory.Functor.Final.extendCocone.map f).hom = f.hom
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>s : CategoryTheory.Limits.Cocone (F.comp G)<VAR>j : C<GOAL>CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.Final.homToLift F (F.obj j))) (s.ι.app (CategoryTheory.Functor.Final.lift F (F.obj j))) = s.ι.app j
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>(CategoryTheory.Functor.Final.coconesEquiv F G).inverse = CategoryTheory.Limits.Cocones.whiskering 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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>(CategoryTheory.Functor.Final.coconesEquiv F G).unitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone (F.comp G))).obj c).pt) ⋯) ⋯
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>(CategoryTheory.Functor.Final.coconesEquiv F G).functor = CategoryTheory.Functor.Final.extendCocone
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>(CategoryTheory.Functor.Final.coconesEquiv F G).counitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (((CategoryTheory.Limits.Cocones.whiskering F).comp CategoryTheory.Functor.Final.extendCocone).obj c).pt) ⋯) ⋯
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>t : CategoryTheory.Limits.ColimitCocone G<GOAL>(CategoryTheory.Functor.Final.colimitCoconeComp F t).isColimit = (CategoryTheory.Functor.Final.isColimitWhiskerEquiv F t.cocone).symm t.isColimit
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>t : CategoryTheory.Limits.ColimitCocone G<GOAL>(CategoryTheory.Functor.Final.colimitCoconeComp F t).cocone = CategoryTheory.Limits.Cocone.whisker F t.cocone
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>t : CategoryTheory.Limits.ColimitCocone (F.comp G)<GOAL>(CategoryTheory.Functor.Final.colimitCoconeOfComp F t).isColimit = (CategoryTheory.Functor.Final.isColimitExtendCoconeEquiv F t.cocone).symm t.isColimit
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>t : CategoryTheory.Limits.ColimitCocone (F.comp G)<GOAL>(CategoryTheory.Functor.Final.colimitCoconeOfComp F t).cocone = CategoryTheory.Functor.Final.extendCocone.obj t.cocone
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>CategoryTheory.Limits.HasColimit (F.comp G)<GOAL>CategoryTheory.Limits.HasColimit G
<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>F.Final<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.Limits.HasColimitsOfShape C E<GOAL>CategoryTheory.Limits.HasColimitsOfShape D E
<VAR>C : Type v<VAR>CategoryTheory.Category.{v, v} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v, u₁} D<VAR>F : CategoryTheory.Functor C D<VAR>d : D<VAR>f₁ f₂ : (X : C) × (d ⟶ F.obj X)<VAR>t : EqvGen (CategoryTheory.Limits.Types.Quot.Rel (F.comp (CategoryTheory.coyoneda.obj (Opposite.op d)))) f₁ f₂<GOAL>CategoryTheory.Zigzag (CategoryTheory.StructuredArrow.mk f₁.snd) (CategoryTheory.StructuredArrow.mk f₂.snd)
<VAR>C : Type v<VAR>CategoryTheory.Category.{v, v} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v, u₁} D<VAR>F : CategoryTheory.Functor C D<VAR>I : (d : D) → CategoryTheory.Limits.colimit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op d))) ≅ PUnit.{v + 1}<GOAL>F.Final
<VAR>C : Type v<VAR>CategoryTheory.Category.{v, v} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v, u₁} D<VAR>F : CategoryTheory.Functor C D<VAR>h : CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda))<GOAL>F.Final
<VAR>C : Type v<VAR>CategoryTheory.Category.{v, v} C<VAR>D : Type v<VAR>CategoryTheory.Category.{v, v} D<VAR>F : CategoryTheory.Functor C D<GOAL>F.Final ↔ ∀ (G : CategoryTheory.Functor D (Type v)), CategoryTheory.IsIso (CategoryTheory.Limits.colimit.pre G 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>F.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>∀ {X Y : CategoryTheory.Limits.Cone (F.comp G)} (f : X ⟶ Y), (CategoryTheory.Functor.Initial.extendCone.map f).hom = f.hom
<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>F.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>c : CategoryTheory.Limits.Cone (F.comp G)<GOAL>(CategoryTheory.Functor.Initial.extendCone.obj c).pt = c.pt
<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>F.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>c : CategoryTheory.Limits.Cone (F.comp G)<VAR>d : D<GOAL>(CategoryTheory.Functor.Initial.extendCone.obj c).π.app d = CategoryTheory.CategoryStruct.comp (c.π.app (CategoryTheory.Functor.Initial.lift F d)) (G.map (CategoryTheory.Functor.Initial.homToLift F d))
<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>F.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>s : CategoryTheory.Limits.Cone (F.comp G)<VAR>j : C<GOAL>CategoryTheory.CategoryStruct.comp (s.π.app (CategoryTheory.Functor.Initial.lift F (F.obj j))) (G.map (CategoryTheory.Functor.Initial.homToLift F (F.obj j))) = s.π.app j
<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>F.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>(CategoryTheory.Functor.Initial.conesEquiv F G).counitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (((CategoryTheory.Limits.Cones.whiskering F).comp CategoryTheory.Functor.Initial.extendCone).obj c).pt) ⋯) ⋯