ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>R X Y Z : C<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>comm : CategoryTheory.CategoryStruct.comp a f₁ = CategoryTheory.CategoryStruct.comp b f₁<VAR>big_k : CategoryTheory.IsKernelPair (CategoryTheory.CategoryStruct.comp f₁ f₂) a b<GOAL>CategoryTheory.IsKernelPair f₁ a b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>R X Y Z : C<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>CategoryTheory.Mono f₂<VAR>big_k : CategoryTheory.IsKernelPair (CategoryTheory.CategoryStruct.comp f₁ f₂) a b<GOAL>CategoryTheory.IsKernelPair f₁ a b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>R X Y Z : C<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>CategoryTheory.Mono f₂<VAR>small_k : CategoryTheory.IsKernelPair f₁ a b<GOAL>CategoryTheory.IsKernelPair (CategoryTheory.CategoryStruct.comp f₁ f₂) a b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z A : C<VAR>g : Y ⟶ Z<VAR>a₁ a₂ : A ⟶ Y<VAR>h : CategoryTheory.IsKernelPair g a₁ a₂<VAR>f : X ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp a₁ g)<GOAL>CategoryTheory.IsKernelPair (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp a₁ g) f g (CategoryTheory.CategoryStruct.id X) a₁ (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) (CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp a₁ g) f g (CategoryTheory.CategoryStruct.id X) a₂ (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>R X Y : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>h : CategoryTheory.IsKernelPair f a b<VAR>CategoryTheory.IsIso a<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>R X Y : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>h : CategoryTheory.IsKernelPair f a b<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.IsIso a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>R X Y : C<VAR>f : X ⟶ Y<VAR>a : R ⟶ X<VAR>CategoryTheory.IsIso a<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.IsKernelPair f a a
<VAR>M : Type v<VAR>Monoid M<VAR>J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)<VAR>s : ↑J.sections<GOAL>↑((CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints J) s) = ↑s (CategoryTheory.SingleObj.star M)
<VAR>M : Type v<VAR>Monoid M<VAR>J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)<VAR>p : ↑(MulAction.fixedPoints M (J.obj (CategoryTheory.SingleObj.star M)))<GOAL>∀ (x : CategoryTheory.SingleObj M), ↑((CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints J).symm p) x = ↑p
<VAR>M : Type v<VAR>Monoid M<VAR>J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)<GOAL>∀ (a : CategoryTheory.Limits.limit J), ↑((CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints J) a) = CategoryTheory.Limits.limit.π J (CategoryTheory.SingleObj.star M) a
<VAR>M : Type v<VAR>Monoid M<VAR>J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)<GOAL>∀ (a : ↑(MulAction.fixedPoints M (J.obj (CategoryTheory.SingleObj.star M)))), (CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints J).symm a = (CategoryTheory.Limits.Types.limitEquivSections J).symm ((CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints J).symm a)
<VAR>G : Type v<VAR>Group G<VAR>J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)<VAR>x y : J.obj (CategoryTheory.SingleObj.star G)<GOAL>CategoryTheory.Limits.Types.Quot.Rel J ⟨CategoryTheory.SingleObj.star G, x⟩ ⟨CategoryTheory.SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (CategoryTheory.SingleObj.star G))).Rel x y
<VAR>G : Type v<VAR>Group G<VAR>J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)<VAR>a : Quot (CategoryTheory.Limits.Types.Quot.Rel J)<GOAL>(CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient J) a = Quot.lift (fun p => ⟦p.snd⟧) ⋯ a
<VAR>G : Type v<VAR>Group G<VAR>J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)<VAR>a : Quot Setoid.r<GOAL>(CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient J).symm a = Quot.lift (fun x => Quot.mk (CategoryTheory.Limits.Types.Quot.Rel J) ⟨CategoryTheory.SingleObj.star G, x⟩) ⋯ a
<VAR>G : Type v<VAR>Group G<VAR>J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)<GOAL>∀ (a : CategoryTheory.Limits.colimit J), (CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient J) a = Quot.lift (fun p => ⟦p.snd⟧) ⋯ ((CategoryTheory.Limits.Types.colimitEquivQuot J) a)
<VAR>G : Type v<VAR>Group G<VAR>J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)<GOAL>∀ (a : MulAction.orbitRel.Quotient G (J.obj (CategoryTheory.SingleObj.star G))), (CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient J).symm a = (CategoryTheory.Limits.Types.colimitEquivQuot J).symm (Quot.lift (fun x => Quot.mk (CategoryTheory.Limits.Types.Quot.Rel J) ⟨CategoryTheory.SingleObj.star G, x⟩) ⋯ a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>self : CategoryTheory.IsSplitCoequalizer f g π<GOAL>CategoryTheory.CategoryStruct.comp self.leftSection f = CategoryTheory.CategoryStruct.comp π self.rightSection
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>self : CategoryTheory.IsSplitCoequalizer f g π<GOAL>CategoryTheory.CategoryStruct.comp self.rightSection π = CategoryTheory.CategoryStruct.id Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>self : CategoryTheory.IsSplitCoequalizer f g π<GOAL>CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>self : CategoryTheory.IsSplitCoequalizer f g π<GOAL>CategoryTheory.CategoryStruct.comp self.leftSection g = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>q : CategoryTheory.IsSplitCoequalizer f g π<VAR>F : CategoryTheory.Functor C D<GOAL>(q.map F).leftSection = F.map q.leftSection
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>q : CategoryTheory.IsSplitCoequalizer f g π<VAR>F : CategoryTheory.Functor C D<GOAL>(q.map F).rightSection = F.map q.rightSection
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>t : CategoryTheory.IsSplitCoequalizer f g h<GOAL>t.asCofork.pt = Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>t : CategoryTheory.IsSplitCoequalizer f g h<GOAL>t.asCofork.π = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>self : CategoryTheory.HasSplitCoequalizer f g<GOAL>∃ Z h, Nonempty (CategoryTheory.IsSplitCoequalizer f g h)
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>self : CategoryTheory.Limits.DiagramOfCones F<VAR>j : J<GOAL>(self.map (𝟙 j)).hom = 𝟙 ((CategoryTheory.Limits.Cones.postcompose (F.map (𝟙 j))).obj (self.obj j)).pt
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>self : CategoryTheory.Limits.DiagramOfCones F<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<GOAL>(self.map (f ≫ g)).hom = (self.map f).hom ≫ (self.map g).hom
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>self : CategoryTheory.Limits.DiagramOfCocones F<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<GOAL>(self.map (f ≫ g)).hom = (self.map f).hom ≫ (self.map g).hom
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>self : CategoryTheory.Limits.DiagramOfCocones F<VAR>j : J<GOAL>(self.map (𝟙 j)).hom = 𝟙 (self.obj j).pt
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : CategoryTheory.Limits.DiagramOfCones F<GOAL>∀ {X Y : J} (f : X ⟶ Y), D.conePoints.map f = (D.map f).hom
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : CategoryTheory.Limits.DiagramOfCones F<VAR>j : J<GOAL>D.conePoints.obj j = (D.obj j).pt
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : CategoryTheory.Limits.DiagramOfCocones F<VAR>j : J<GOAL>D.coconePoints.obj j = (D.obj j).pt
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : CategoryTheory.Limits.DiagramOfCocones F<GOAL>∀ {X Y : J} (f : X ⟶ Y), D.coconePoints.map f = (D.map f).hom
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : CategoryTheory.Limits.DiagramOfCones F<VAR>Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)<VAR>c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)<GOAL>(CategoryTheory.Limits.coneOfConeUncurry Q c).pt = c.pt
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : CategoryTheory.Limits.DiagramOfCones F<VAR>Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)<VAR>c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)<VAR>j : J<GOAL>(CategoryTheory.Limits.coneOfConeUncurry Q c).π.app j = (Q j).lift { pt := c.pt, π := { app := fun k => c.π.app (j, k), naturality := ⋯ } }
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : CategoryTheory.Limits.DiagramOfCocones F<VAR>Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)<VAR>c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.obj F)<GOAL>(CategoryTheory.Limits.coconeOfCoconeUncurry Q c).pt = c.pt
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : CategoryTheory.Limits.DiagramOfCocones F<VAR>Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)<VAR>c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.obj F)<VAR>j : J<GOAL>(CategoryTheory.Limits.coconeOfCoconeUncurry Q c).ι.app j = (Q j).desc { pt := c.pt, ι := { app := fun k => c.ι.app (j, k), naturality := ⋯ } }
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<VAR>j : J<GOAL>(CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).obj j = CategoryTheory.Limits.limit.cone (F.obj j)
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<GOAL>∀ {j j' : J} (f : j ⟶ j'), ((CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).map f).hom = CategoryTheory.Limits.lim.map (F.map f)
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<GOAL>(CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).conePoints = F ⋙ CategoryTheory.Limits.lim
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)<VAR>CategoryTheory.Limits.HasLimit (F ⋙ CategoryTheory.Limits.lim)<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).hom ≫ CategoryTheory.Limits.limit.π (F ⋙ CategoryTheory.Limits.lim) j ≫ CategoryTheory.Limits.limit.π (F.obj j) k = CategoryTheory.Limits.limit.π (CategoryTheory.uncurry.obj F) (j, k)
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)<VAR>CategoryTheory.Limits.HasLimit (F ⋙ CategoryTheory.Limits.lim)<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).inv ≫ CategoryTheory.Limits.limit.π (CategoryTheory.uncurry.obj F) (j, k) = CategoryTheory.Limits.limit.π (F ⋙ CategoryTheory.Limits.lim) j ≫ CategoryTheory.Limits.limit.π (F.obj j) k
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<GOAL>∀ {j j' : J} (f : j ⟶ j'), ((CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).map f).hom = CategoryTheory.Limits.colim.map (F.map f)
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>j : J<GOAL>(CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).obj j = CategoryTheory.Limits.colimit.cocone (F.obj j)
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<GOAL>(CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).coconePoints = F ⋙ CategoryTheory.Limits.colim
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.obj F)<VAR>CategoryTheory.Limits.HasColimit (F ⋙ CategoryTheory.Limits.colim)<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι (F.obj j) k ≫ CategoryTheory.Limits.colimit.ι (F ⋙ CategoryTheory.Limits.colim) j ≫ (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).inv = CategoryTheory.Limits.colimit.ι (CategoryTheory.uncurry.obj F) (j, k)
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.obj F)<VAR>CategoryTheory.Limits.HasColimit (F ⋙ CategoryTheory.Limits.colim)<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι (CategoryTheory.uncurry.obj F) (j, k) ≫ (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).hom = CategoryTheory.Limits.colimit.ι (F.obj j) k ≫ CategoryTheory.Limits.colimit.ι (F ⋙ CategoryTheory.Limits.colim) j
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<VAR>CategoryTheory.Limits.HasLimitsOfShape (J × K) C<VAR>CategoryTheory.Limits.HasLimitsOfShape (K × J) C<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).hom ≫ CategoryTheory.Limits.limit.π (F ⋙ CategoryTheory.Limits.lim) j ≫ CategoryTheory.Limits.limit.π (F.obj j) k = CategoryTheory.Limits.limit.π (F.flip ⋙ CategoryTheory.Limits.lim) k ≫ CategoryTheory.Limits.limit.π (F.flip.obj k) j
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<VAR>CategoryTheory.Limits.HasLimitsOfShape (J × K) C<VAR>CategoryTheory.Limits.HasLimitsOfShape (K × J) C<VAR>k : K<VAR>j : J<GOAL>(CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).inv ≫ CategoryTheory.Limits.limit.π (F.flip ⋙ CategoryTheory.Limits.lim) k ≫ CategoryTheory.Limits.limit.π (F.flip.obj k) j = CategoryTheory.Limits.limit.π (F ⋙ CategoryTheory.Limits.lim) j ≫ CategoryTheory.Limits.limit.π (F.obj j) k
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>CategoryTheory.Limits.HasColimitsOfShape (J × K) C<VAR>CategoryTheory.Limits.HasColimitsOfShape (K × J) C<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι (F.flip.obj k) j ≫ CategoryTheory.Limits.colimit.ι (F.flip ⋙ CategoryTheory.Limits.colim) k ≫ (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).hom = CategoryTheory.Limits.colimit.ι (F.obj j) k ≫ CategoryTheory.Limits.colimit.ι (F ⋙ CategoryTheory.Limits.colim) j
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>CategoryTheory.Limits.HasColimitsOfShape (J × K) C<VAR>CategoryTheory.Limits.HasColimitsOfShape (K × J) C<VAR>k : K<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι (F.obj j) k ≫ CategoryTheory.Limits.colimit.ι (F ⋙ CategoryTheory.Limits.colim) j ≫ (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).inv = CategoryTheory.Limits.colimit.ι (F.flip.obj k) j ≫ CategoryTheory.Limits.colimit.ι (F.flip ⋙ CategoryTheory.Limits.colim) k
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : J × K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<VAR>CategoryTheory.Limits.HasLimit G<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.lim)<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limitIsoLimitCurryCompLim G).hom ≫ CategoryTheory.Limits.limit.π (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.lim) j ≫ CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k = CategoryTheory.Limits.limit.π G (j, k)
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : J × K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape K C<VAR>CategoryTheory.Limits.HasLimit G<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.lim)<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limitIsoLimitCurryCompLim G).inv ≫ CategoryTheory.Limits.limit.π G (j, k) = CategoryTheory.Limits.limit.π (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.lim) j ≫ CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : J × K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>CategoryTheory.Limits.HasColimit G<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.colim)<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k ≫ CategoryTheory.Limits.colimit.ι (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.colim) j ≫ (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).inv = CategoryTheory.Limits.colimit.ι G (j, k)
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : J × K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>CategoryTheory.Limits.HasColimit G<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.colim)<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι G (j, k) ≫ (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).hom = CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k ≫ CategoryTheory.Limits.colimit.ι (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.colim) j
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : J × K ⥤ C<VAR>CategoryTheory.Limits.HasLimits C<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim G).hom ≫ CategoryTheory.Limits.limit.π (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.lim) j ≫ CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k = CategoryTheory.Limits.limit.π (CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ G) ⋙ CategoryTheory.Limits.lim) k ≫ CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ G)).obj k) j
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : J × K ⥤ C<VAR>CategoryTheory.Limits.HasLimits C<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim G).inv ≫ CategoryTheory.Limits.limit.π (CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ G) ⋙ CategoryTheory.Limits.lim) k ≫ CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ G)).obj k) j = CategoryTheory.Limits.limit.π (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.lim) j ≫ CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : J × K ⥤ C<VAR>CategoryTheory.Limits.HasColimits C<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ G)).obj k) j ≫ CategoryTheory.Limits.colimit.ι (CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ G) ⋙ CategoryTheory.Limits.colim) k ≫ (CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim G).hom = CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k ≫ CategoryTheory.Limits.colimit.ι (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.colim) j
<VAR>J K : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.SmallCategory K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : J × K ⥤ C<VAR>CategoryTheory.Limits.HasColimits C<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k ≫ CategoryTheory.Limits.colimit.ι (CategoryTheory.curry.obj G ⋙ CategoryTheory.Limits.colim) j ≫ (CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim G).inv = CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ G)).obj k) j ≫ CategoryTheory.Limits.colimit.ι (CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ G) ⋙ CategoryTheory.Limits.colim) k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)<GOAL>CategoryTheory.Limits.PullbackCone.fst (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) = CategoryTheory.Limits.pullback.fst f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)<GOAL>CategoryTheory.Limits.PullbackCone.snd (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) = CategoryTheory.Limits.pullback.snd f g