ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasLimit (F ⋙ G)<VAR>j : J<GOAL>CategoryTheory.Limits.limit.post F G ≫ CategoryTheory.Limits.limit.π (F ⋙ G) j = G.map (CategoryTheory.Limits.limit.π F j)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasLimit (F ⋙ G)<VAR>c : CategoryTheory.Limits.Cone F<GOAL>G.map (CategoryTheory.Limits.limit.lift F c) ≫ CategoryTheory.Limits.limit.post F G = CategoryTheory.Limits.limit.lift (F ⋙ G) (G.mapCone c)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasLimit (F ⋙ G)<VAR>E : Type u''<VAR>CategoryTheory.Category.{v'', u''} E<VAR>H : D ⥤ E<VAR>h : CategoryTheory.Limits.HasLimit ((F ⋙ G) ⋙ H)<GOAL>H.map (CategoryTheory.Limits.limit.post F G) ≫ CategoryTheory.Limits.limit.post (F ⋙ G) H = CategoryTheory.Limits.limit.post F (G ⋙ H)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>E : K ⥤ J<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasLimit F<VAR>CategoryTheory.Limits.HasLimit (E ⋙ F)<VAR>CategoryTheory.Limits.HasLimit (F ⋙ G)<VAR>h : CategoryTheory.Limits.HasLimit ((E ⋙ F) ⋙ G)<GOAL>G.map (CategoryTheory.Limits.limit.pre F E) ≫ CategoryTheory.Limits.limit.post (E ⋙ F) G = CategoryTheory.Limits.limit.post F G ≫ CategoryTheory.Limits.limit.pre (F ⋙ G) E
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>e : K ≌ J<VAR>CategoryTheory.Limits.HasLimit (e.functor ⋙ F)<GOAL>CategoryTheory.Limits.HasLimit F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<GOAL>∀ {X Y : J ⥤ C} (α : X ⟶ Y), CategoryTheory.Limits.lim.map α = CategoryTheory.Limits.limMap α
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F : J ⥤ C<GOAL>CategoryTheory.Limits.lim.obj F = CategoryTheory.Limits.limit F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<VAR>E : K ⥤ J<GOAL>CategoryTheory.Limits.lim.map α ≫ CategoryTheory.Limits.limit.pre G E = CategoryTheory.Limits.limit.pre F E ≫ CategoryTheory.Limits.lim.map (CategoryTheory.whiskerLeft E α)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<VAR>F : J ⥤ C<VAR>E₁ E₂ : K ⥤ J<VAR>α : E₁ ⟶ E₂<GOAL>CategoryTheory.Limits.limit.pre F E₂ = CategoryTheory.Limits.limit.pre F E₁ ≫ CategoryTheory.Limits.lim.map (CategoryTheory.whiskerRight α F)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F : J ⥤ C<GOAL>CategoryTheory.Limits.limit.pre F (𝟭 J) = CategoryTheory.Limits.lim.map F.leftUnitor.inv
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasLimitsOfShape J D<VAR>H : C ⥤ D<GOAL>H.map (CategoryTheory.Limits.limMap α) ≫ CategoryTheory.Limits.limit.post G H = CategoryTheory.Limits.limit.post F H ≫ CategoryTheory.Limits.limMap (CategoryTheory.whiskerRight α H)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>L : (J ⥤ C) ⥤ C<VAR>adj : CategoryTheory.Functor.const J ⊣ L<VAR>F : J ⥤ C<GOAL>(CategoryTheory.Limits.coneOfAdj adj F).pt = L.obj F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>L : (J ⥤ C) ⥤ C<VAR>adj : CategoryTheory.Functor.const J ⊣ L<VAR>F : J ⥤ C<GOAL>(CategoryTheory.Limits.coneOfAdj adj F).π = adj.counit.app F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>L : (J ⥤ C) ⥤ C<VAR>adj : CategoryTheory.Functor.const J ⊣ L<VAR>F : J ⥤ C<VAR>s : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.isLimitConeOfAdj adj F).lift s = (adj.homEquiv s.pt F) s.π
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J' : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J'<VAR>e : J ≌ J'<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<GOAL>CategoryTheory.Limits.HasLimitsOfShape J' C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>UnivLE.{v₂, v₁}<VAR>UnivLE.{u₂, u₁}<VAR>CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>self : CategoryTheory.Limits.HasColimit F<GOAL>Nonempty (CategoryTheory.Limits.ColimitCocone F)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>d : CategoryTheory.Limits.ColimitCocone F<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : J ⥤ C<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>J : Type v<VAR>CategoryTheory.Category.{v, v} J<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>j : J<GOAL>(CategoryTheory.Limits.colimit.cocone F).ι.app j = CategoryTheory.Limits.colimit.ι F j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<GOAL>(CategoryTheory.Limits.colimit.cocone F).pt = CategoryTheory.Limits.colimit F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ CategoryTheory.Limits.colimit.ι F j' = CategoryTheory.Limits.colimit.ι F j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.colimit.isColimit F).desc c = CategoryTheory.Limits.colimit.desc F c
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>c : CategoryTheory.Limits.Cocone F<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι F j ≫ CategoryTheory.Limits.colimit.desc F c = c.ι.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasColimit G<VAR>α : F ⟶ G<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι F j ≫ CategoryTheory.Limits.colimMap α = α.app j ≫ CategoryTheory.Limits.colimit.ι G j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.colimit.coconeMorphism c).hom = CategoryTheory.Limits.colimit.desc F c
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>c : CategoryTheory.Limits.Cocone F<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι F j ≫ (CategoryTheory.Limits.colimit.coconeMorphism c).hom = c.ι.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι F j ≫ ((CategoryTheory.Limits.colimit.isColimit F).coconePointUniqueUpToIso hc).hom = c.ι.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι F j ≫ (hc.coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit F)).inv = c.ι.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>t : CategoryTheory.Limits.Cocone F<GOAL>∃! d, ∀ (j : J), CategoryTheory.Limits.colimit.ι F j ≫ d = t.ι.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>t : CategoryTheory.Limits.ColimitCocone F<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι F j ≫ (CategoryTheory.Limits.colimit.isoColimitCocone t).hom = t.cocone.ι.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>t : CategoryTheory.Limits.ColimitCocone F<VAR>j : J<GOAL>t.cocone.ι.app j ≫ (CategoryTheory.Limits.colimit.isoColimitCocone t).inv = CategoryTheory.Limits.colimit.ι F j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>X : C<VAR>f f' : CategoryTheory.Limits.colimit F ⟶ X<VAR>w : ∀ (j : J), CategoryTheory.Limits.colimit.ι F j ≫ f = CategoryTheory.Limits.colimit.ι F j ≫ f'<GOAL>f = f'
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<GOAL>CategoryTheory.Limits.colimit.desc F (CategoryTheory.Limits.colimit.cocone F) = 𝟙 (CategoryTheory.Limits.colimit F)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>W : C<VAR>f : ULift.{u₁, v} (CategoryTheory.Limits.colimit F ⟶ W)<GOAL>(CategoryTheory.Limits.colimit.homIso F W).hom f = (CategoryTheory.Limits.colimit.cocone F).ι ≫ (CategoryTheory.Functor.const J).map f.down
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>c : CategoryTheory.Limits.Cocone F<VAR>X : C<VAR>f : c.pt ⟶ X<GOAL>CategoryTheory.Limits.colimit.desc F (c.extend f) = CategoryTheory.Limits.colimit.desc F c ≫ f
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>α : G ≅ F<GOAL>CategoryTheory.Limits.HasColimit G
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>K : Type u₁<VAR>CategoryTheory.Category.{v₂, u₁} K<VAR>F : J ⥤ C<VAR>G : K ⥤ C<VAR>h : F.cocones ≅ G.cocones<VAR>CategoryTheory.Limits.HasColimit F<GOAL>CategoryTheory.Limits.HasColimit G
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasColimit G<VAR>w : F ≅ G<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι F j ≫ (CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom = w.hom.app j ≫ CategoryTheory.Limits.colimit.ι G j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasColimit G<VAR>w : F ≅ G<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι G j ≫ (CategoryTheory.Limits.HasColimit.isoOfNatIso w).inv = w.inv.app j ≫ CategoryTheory.Limits.colimit.ι F j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasColimit G<VAR>t : CategoryTheory.Limits.Cocone G<VAR>w : F ≅ G<GOAL>(CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom ≫ CategoryTheory.Limits.colimit.desc G t = CategoryTheory.Limits.colimit.desc F ((CategoryTheory.Limits.Cocones.precompose w.hom).obj t)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasColimit G<VAR>t : CategoryTheory.Limits.Cocone F<VAR>w : F ≅ G<GOAL>(CategoryTheory.Limits.HasColimit.isoOfNatIso w).inv ≫ CategoryTheory.Limits.colimit.desc F t = CategoryTheory.Limits.colimit.desc G ((CategoryTheory.Limits.Cocones.precompose w.inv).obj t)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>G : K ⥤ C<VAR>CategoryTheory.Limits.HasColimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι F j ≫ (CategoryTheory.Limits.HasColimit.isoOfEquivalence e w).hom = F.map (e.unit.app j) ≫ w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫ CategoryTheory.Limits.colimit.ι G (e.functor.obj ((e.functor ⋙ e.inverse).obj j))
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>G : K ⥤ C<VAR>CategoryTheory.Limits.HasColimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι G k ≫ (CategoryTheory.Limits.HasColimit.isoOfEquivalence e w).inv = G.map (e.counitInv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ CategoryTheory.Limits.colimit.ι F (e.inverse.obj k)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>E : K ⥤ J<VAR>CategoryTheory.Limits.HasColimit (E ⋙ F)<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι (E ⋙ F) k ≫ CategoryTheory.Limits.colimit.pre F E = CategoryTheory.Limits.colimit.ι F (E.obj k)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>E : K ⥤ J<VAR>CategoryTheory.Limits.HasColimit (E ⋙ F)<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>CategoryTheory.Limits.colimit.pre F E ≫ CategoryTheory.Limits.colimit.desc F c = CategoryTheory.Limits.colimit.desc (E ⋙ F) (CategoryTheory.Limits.Cocone.whisker E c)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>E : K ⥤ J<VAR>CategoryTheory.Limits.HasColimit (E ⋙ F)<VAR>L : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} L<VAR>D : L ⥤ K<VAR>h : CategoryTheory.Limits.HasColimit (D ⋙ E ⋙ F)<GOAL>CategoryTheory.Limits.colimit.pre (E ⋙ F) D ≫ CategoryTheory.Limits.colimit.pre F E = CategoryTheory.Limits.colimit.pre F (D ⋙ E)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>E : K ⥤ J<VAR>CategoryTheory.Limits.HasColimit (E ⋙ F)<VAR>s : CategoryTheory.Limits.ColimitCocone (E ⋙ F)<VAR>t : CategoryTheory.Limits.ColimitCocone F<GOAL>CategoryTheory.Limits.colimit.pre F E = (CategoryTheory.Limits.colimit.isoColimitCocone s).hom ≫ s.isColimit.desc (CategoryTheory.Limits.Cocone.whisker E t.cocone) ≫ (CategoryTheory.Limits.colimit.isoColimitCocone t).inv
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasColimit F<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasColimit (F ⋙ G)<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι (F ⋙ G) j ≫ CategoryTheory.Limits.colimit.post F G = G.map (CategoryTheory.Limits.colimit.ι F j)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasColimit F<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasColimit (F ⋙ G)<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>CategoryTheory.Limits.colimit.post F G ≫ G.map (CategoryTheory.Limits.colimit.desc F c) = CategoryTheory.Limits.colimit.desc (F ⋙ G) (G.mapCocone c)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasColimit F<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasColimit (F ⋙ G)<VAR>E : Type u''<VAR>CategoryTheory.Category.{v'', u''} E<VAR>H : D ⥤ E<VAR>h : CategoryTheory.Limits.HasColimit ((F ⋙ G) ⋙ H)<GOAL>CategoryTheory.Limits.colimit.post (F ⋙ G) H ≫ H.map (CategoryTheory.Limits.colimit.post F G) = CategoryTheory.Limits.colimit.post F (G ⋙ H)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>E : K ⥤ J<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasColimit (E ⋙ F)<VAR>CategoryTheory.Limits.HasColimit (F ⋙ G)<VAR>h : CategoryTheory.Limits.HasColimit ((E ⋙ F) ⋙ G)<GOAL>CategoryTheory.Limits.colimit.post (E ⋙ F) G ≫ G.map (CategoryTheory.Limits.colimit.pre F E) = CategoryTheory.Limits.colimit.pre (F ⋙ G) E ≫ CategoryTheory.Limits.colimit.post F G
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>e : K ≌ J<VAR>CategoryTheory.Limits.HasColimit (e.functor ⋙ F)<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : J ⥤ C<GOAL>CategoryTheory.Limits.colim.obj F = CategoryTheory.Limits.colimit F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<GOAL>∀ {X Y : J ⥤ C} (α : X ⟶ Y), CategoryTheory.Limits.colim.map α = CategoryTheory.Limits.colimMap α
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι F j ≫ CategoryTheory.Limits.colim.map α = α.app j ≫ CategoryTheory.Limits.colimit.ι G j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>c : CategoryTheory.Limits.Cocone G<GOAL>CategoryTheory.Limits.colimMap α ≫ CategoryTheory.Limits.colimit.desc G c = CategoryTheory.Limits.colimit.desc F ((CategoryTheory.Limits.Cocones.precompose α).obj c)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>E : K ⥤ J<GOAL>CategoryTheory.Limits.colimit.pre F E ≫ CategoryTheory.Limits.colim.map α = CategoryTheory.Limits.colim.map (CategoryTheory.whiskerLeft E α) ≫ CategoryTheory.Limits.colimit.pre G E
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>F : J ⥤ C<VAR>E₁ E₂ : K ⥤ J<VAR>α : E₁ ⟶ E₂<GOAL>CategoryTheory.Limits.colimit.pre F E₁ = CategoryTheory.Limits.colim.map (CategoryTheory.whiskerRight α F) ≫ CategoryTheory.Limits.colimit.pre F E₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : J ⥤ C<GOAL>CategoryTheory.Limits.colimit.pre F (𝟭 J) = CategoryTheory.Limits.colim.map F.leftUnitor.hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasColimitsOfShape J D<VAR>H : C ⥤ D<GOAL>CategoryTheory.Limits.colimit.post F H ≫ H.map (CategoryTheory.Limits.colim.map α) = CategoryTheory.Limits.colim.map (CategoryTheory.whiskerRight α H) ≫ CategoryTheory.Limits.colimit.post G H
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J' : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J'<VAR>e : J ≌ J'<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<GOAL>CategoryTheory.Limits.HasColimitsOfShape J' C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>UnivLE.{v₂, v₁}<VAR>UnivLE.{u₂, u₁}<VAR>CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C<GOAL>CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C<GOAL>CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasFiniteProducts C<VAR>n : ℕ<GOAL>CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete (Fin n)) C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<GOAL>CategoryTheory.Limits.HasFiniteProducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasFiniteCoproducts C<VAR>n : ℕ<GOAL>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (Fin n)) C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasCoproducts C<GOAL>CategoryTheory.Limits.HasFiniteCoproducts C