ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>X₂.HasTensor X₃<VAR>X₃.HasTensor X₄<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃).HasTensor X₄<VAR>X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃).HasTensor X₄<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)).HasTensor X₄<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄)<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>X₁.HasGoodTensor₁₂Tensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄<VAR>X₁.HasGoodTensorTensor₂₃ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄<VAR>X₂.HasGoodTensor₁₂Tensor X₃ X₄<VAR>X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄<VAR>X₁.HasGoodTensor₁₂Tensor X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>X₁.HasGoodTensorTensor₂₃ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>X₁.HasTensor₄ObjExt X₂ X₃ X₄<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.GradedObject.Monoidal.associator X₂ X₃ X₄).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄).inv (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).inv (CategoryTheory.CategoryStruct.id X₄))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)).inv (CategoryTheory.GradedObject.Monoidal.associator (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ X₄).inv
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>X₂.HasTensor X₃<VAR>X₃.HasTensor X₄<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃).HasTensor X₄<VAR>X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃).HasTensor X₄<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)).HasTensor X₄<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄)<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>X₁.HasGoodTensor₁₂Tensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄<VAR>X₁.HasGoodTensorTensor₂₃ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄<VAR>X₂.HasGoodTensor₁₂Tensor X₃ X₄<VAR>X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄<VAR>X₁.HasGoodTensor₁₂Tensor X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>X₁.HasGoodTensorTensor₂₃ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>X₁.HasTensor₄ObjExt X₂ X₃ X₄<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom (CategoryTheory.CategoryStruct.id X₄)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄).hom (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.GradedObject.Monoidal.associator X₂ X₃ X₄).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ X₄).hom (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)).hom
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>(X₂ : C) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)<VAR>X : CategoryTheory.GradedObject I C<VAR>i : I<GOAL>(CategoryTheory.GradedObject.Monoidal.leftUnitor X).inv i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (X i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight CategoryTheory.GradedObject.Monoidal.tensorUnit₀.inv (X i)) (CategoryTheory.GradedObject.Monoidal.ιTensorObj CategoryTheory.GradedObject.Monoidal.tensorUnit X 0 i i ⋯))
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>(X₂ : C) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)<VAR>X X' : CategoryTheory.GradedObject I C<VAR>φ : X ⟶ X'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit) φ) (CategoryTheory.GradedObject.Monoidal.leftUnitor X').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.leftUnitor X).hom φ
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>(X₁ : C) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)<VAR>X : CategoryTheory.GradedObject I C<VAR>i : I<GOAL>(CategoryTheory.GradedObject.Monoidal.rightUnitor X).inv i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (X i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (X i) CategoryTheory.GradedObject.Monoidal.tensorUnit₀.inv) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X CategoryTheory.GradedObject.Monoidal.tensorUnit i 0 i ⋯))
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>(X₁ : C) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)<VAR>X X' : CategoryTheory.GradedObject I C<VAR>φ : X ⟶ X'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom φ (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit)) (CategoryTheory.GradedObject.Monoidal.rightUnitor X').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.rightUnitor X).hom φ
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>(X₁ : C) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)<VAR>(X₂ : C) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)<VAR>X₁ X₃ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₃<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ CategoryTheory.GradedObject.Monoidal.tensorUnit).HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj CategoryTheory.GradedObject.Monoidal.tensorUnit X₃)<VAR>X₁.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.Monoidal.tensorUnit X₃<VAR>X₁.HasGoodTensorTensor₂₃ CategoryTheory.GradedObject.Monoidal.tensorUnit X₃<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X₁ CategoryTheory.GradedObject.Monoidal.tensorUnit X₃).hom (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.GradedObject.Monoidal.leftUnitor X₃).hom) = CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.rightUnitor X₁).hom (CategoryTheory.CategoryStruct.id X₃)
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor J C<VAR>α : F ⟶ G<VAR>CategoryTheory.IsIso α<GOAL>CategoryTheory.NatTrans.Equifibered α
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G H : CategoryTheory.Functor J C<VAR>α : F ⟶ G<VAR>β : G ⟶ H<VAR>hα : CategoryTheory.NatTrans.Equifibered α<VAR>hβ : CategoryTheory.NatTrans.Equifibered β<GOAL>CategoryTheory.NatTrans.Equifibered (CategoryTheory.CategoryStruct.comp α β)
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>F G : CategoryTheory.Functor J C<VAR>α : F ⟶ G<VAR>hα : CategoryTheory.NatTrans.Equifibered α<VAR>H : CategoryTheory.Functor C D<VAR>(i j : J) → (f : j ⟶ i) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (α.app i) (G.map f)) H<GOAL>CategoryTheory.NatTrans.Equifibered (CategoryTheory.whiskerRight α H)
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>K : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} K<VAR>F G : CategoryTheory.Functor J C<VAR>α : F ⟶ G<VAR>hα : CategoryTheory.NatTrans.Equifibered α<VAR>H : CategoryTheory.Functor K J<GOAL>CategoryTheory.NatTrans.Equifibered (CategoryTheory.whiskerLeft H α)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F' : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C<VAR>α : F ⟶ F'<GOAL>CategoryTheory.NatTrans.Equifibered α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_3<VAR>F G : CategoryTheory.Functor (CategoryTheory.Discrete ι) C<VAR>α : F ⟶ G<GOAL>CategoryTheory.NatTrans.Equifibered α
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>H : CategoryTheory.IsVanKampenColimit c<GOAL>CategoryTheory.IsUniversalColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>X : C<VAR>h : CategoryTheory.Limits.IsInitial X<GOAL>CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.asEmptyCocone X)
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor J C<VAR>c c' : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.IsUniversalColimit c<VAR>e : c ≅ c'<GOAL>CategoryTheory.IsUniversalColimit c'
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor J C<VAR>c c' : CategoryTheory.Limits.Cocone F<VAR>H : CategoryTheory.IsVanKampenColimit c<VAR>e : c ≅ c'<GOAL>CategoryTheory.IsVanKampenColimit c'
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor J C<VAR>α : F ⟶ G<VAR>CategoryTheory.IsIso α<VAR>c : CategoryTheory.Limits.Cocone G<VAR>hc : CategoryTheory.IsVanKampenColimit c<GOAL>CategoryTheory.IsVanKampenColimit ((CategoryTheory.Limits.Cocones.precompose α).obj c)
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor J C<VAR>α : F ⟶ G<VAR>CategoryTheory.IsIso α<VAR>c : CategoryTheory.Limits.Cocone G<VAR>hc : CategoryTheory.IsUniversalColimit c<GOAL>CategoryTheory.IsUniversalColimit ((CategoryTheory.Limits.Cocones.precompose α).obj c)
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor J C<VAR>α : F ⟶ G<VAR>CategoryTheory.IsIso α<VAR>c : CategoryTheory.Limits.Cocone G<GOAL>CategoryTheory.IsVanKampenColimit ((CategoryTheory.Limits.Cocones.precompose α).obj c) ↔ CategoryTheory.IsVanKampenColimit c
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G<VAR>CategoryTheory.Limits.ReflectsColimitsOfShape J G<VAR>hc : CategoryTheory.IsUniversalColimit (G.mapCocone c)<GOAL>CategoryTheory.IsUniversalColimit c
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>(i j : J) → (X : C) → (f : X ⟶ F.obj j) → (g : i ⟶ j) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (F.map g)) G<VAR>(i : J) → (X : C) → (f : X ⟶ c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.ι.app i)) G<VAR>CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan G<VAR>CategoryTheory.Limits.PreservesColimitsOfShape J G<VAR>CategoryTheory.Limits.ReflectsColimitsOfShape J G<VAR>H : CategoryTheory.IsVanKampenColimit (G.mapCocone c)<GOAL>CategoryTheory.IsVanKampenColimit c
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>G.IsEquivalence<GOAL>CategoryTheory.IsVanKampenColimit (G.mapCocone c) ↔ CategoryTheory.IsVanKampenColimit c
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>K : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : CategoryTheory.Functor K C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.IsUniversalColimit c<GOAL>CategoryTheory.IsUniversalColimit (CategoryTheory.Limits.Cocone.whisker e.functor c)
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>K : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : CategoryTheory.Functor K C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>CategoryTheory.IsUniversalColimit (CategoryTheory.Limits.Cocone.whisker e.functor c) ↔ CategoryTheory.IsUniversalColimit c
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>K : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : CategoryTheory.Functor K C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.IsVanKampenColimit c<GOAL>CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.Cocone.whisker e.functor c)
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>K : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : CategoryTheory.Functor K C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.Cocone.whisker e.functor c) ↔ CategoryTheory.IsVanKampenColimit c
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Limits.HasPullbacks D<VAR>CategoryTheory.Limits.HasColimitsOfShape J D<VAR>F : CategoryTheory.Functor J (CategoryTheory.Functor C D)<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : ∀ (x : C), CategoryTheory.IsVanKampenColimit (((CategoryTheory.evaluation C D).obj x).mapCocone c)<GOAL>CategoryTheory.IsVanKampenColimit c
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>Gl : CategoryTheory.Functor C D<VAR>Gr : CategoryTheory.Functor D C<VAR>adj : Gl ⊣ Gr<VAR>Gr.Full<VAR>Gr.Faithful<VAR>F : CategoryTheory.Functor J D<VAR>c : CategoryTheory.Limits.Cocone (F.comp Gr)<VAR>H : CategoryTheory.IsUniversalColimit c<VAR>∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>(X : D) → (f : X ⟶ Gl.obj c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl<GOAL>CategoryTheory.IsUniversalColimit (Gl.mapCocone c)
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>Gl : CategoryTheory.Functor C D<VAR>Gr : CategoryTheory.Functor D C<VAR>adj : Gl ⊣ Gr<VAR>Gr.Full<VAR>Gr.Faithful<VAR>F : CategoryTheory.Functor J D<VAR>c : CategoryTheory.Limits.Cocone (F.comp Gr)<VAR>H : CategoryTheory.IsVanKampenColimit c<VAR>∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>(X : D) → (f : X ⟶ Gl.obj c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>(X : C) → (i : J) → (f : X ⟶ c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.ι.app i)) Gl<GOAL>CategoryTheory.IsVanKampenColimit (Gl.mapCocone c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>H : CategoryTheory.IsUniversalColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.id (⊥_ C)) (CategoryTheory.CategoryStruct.id (⊥_ C)))<GOAL>CategoryTheory.Limits.HasStrictInitialObjects C
<VAR>J : Type v'<VAR>CategoryTheory.Category.{u', v'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>IsEmpty J<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsVanKampenColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<GOAL>CategoryTheory.IsVanKampenColimit c ↔ ∀ {X' Y' : C} (c' : CategoryTheory.Limits.BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt), CategoryTheory.CategoryStruct.comp αX c.inl = CategoryTheory.CategoryStruct.comp c'.inl f → CategoryTheory.CategoryStruct.comp αY c.inr = CategoryTheory.CategoryStruct.comp c'.inr f → (Nonempty (CategoryTheory.Limits.IsColimit c') ↔ CategoryTheory.IsPullback c'.inl αX f c.inl ∧ CategoryTheory.IsPullback c'.inr αY f c.inr)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<VAR>cofans : (X Y : C) → CategoryTheory.Limits.BinaryCofan X Y<VAR>colimits : (X Y : C) → CategoryTheory.Limits.IsColimit (cofans X Y)<VAR>cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PullbackCone f g<VAR>limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.IsLimit (cones f g)<VAR>h₁ : ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt), CategoryTheory.CategoryStruct.comp αX c.inl = CategoryTheory.CategoryStruct.comp (cofans X' Y').inl f → CategoryTheory.CategoryStruct.comp αY c.inr = CategoryTheory.CategoryStruct.comp (cofans X' Y').inr f → CategoryTheory.IsPullback (cofans X' Y').inl αX f c.inl ∧ CategoryTheory.IsPullback (cofans X' Y').inr αY f c.inr<VAR>h₂ : {Z : C} → (f : Z ⟶ c.pt) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)<GOAL>CategoryTheory.IsVanKampenColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>X Y : C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<VAR>h : CategoryTheory.IsVanKampenColimit c<GOAL>CategoryTheory.Mono c.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasInitial C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<VAR>h : CategoryTheory.IsVanKampenColimit c<GOAL>CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ<VAR>c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt<VAR>t₁ : CategoryTheory.IsUniversalColimit c₁<VAR>t₂ : CategoryTheory.IsUniversalColimit c₂<VAR>∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback c₂.inr i<GOAL>CategoryTheory.IsUniversalColimit (CategoryTheory.extendCofan c₁ c₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ<VAR>c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt<VAR>t₁ : CategoryTheory.IsVanKampenColimit c₁<VAR>t₂ : CategoryTheory.IsVanKampenColimit c₂<VAR>∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback c₂.inr i<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.IsVanKampenColimit (CategoryTheory.extendCofan c₁ c₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>ι : Type u_3<VAR>X : ι → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>hc : CategoryTheory.IsVanKampenColimit c<VAR>i j : ι<VAR>DecidableEq ι<GOAL>CategoryTheory.IsPullback (if h : j = i then CategoryTheory.eqToHom ⋯ else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X i))) (if h : j = i then CategoryTheory.eqToHom ⋯ else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X j))) (c.inj i) (c.inj j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>ι : Type u_3<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.IsVanKampenColimit c<VAR>i j : CategoryTheory.Discrete ι<VAR>hi : i ≠ j<GOAL>CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (F.obj i)) (CategoryTheory.Limits.initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>ι : Type u_3<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.IsVanKampenColimit c<VAR>i : CategoryTheory.Discrete ι<GOAL>CategoryTheory.Mono (c.ι.app i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X : C<VAR>f g : X ⟶ 𝟙_ C<GOAL>f = g