ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>∀ (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair), (CategoryTheory.FunctorToTypes.binaryCoproductCocone F G).ι.app x = match x.as with | CategoryTheory.Limits.WalkingPair.left => CategoryTheory.FunctorToTypes.coprod.inl | CategoryTheory.Limits.WalkingPair.right => CategoryTheory.FunctorToTypes.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<GOAL>(CategoryTheory.FunctorToTypes.binaryCoproductCocone F G).pt.obj a = (F.obj a ⊕ G.obj a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>∀ {X Y : C} (f : X ⟶ Y) (x : F.obj X ⊕ G.obj X), (CategoryTheory.FunctorToTypes.binaryCoproductCocone F G).pt.map f x = Sum.rec (motive := fun t => x = t → F.obj Y ⊕ G.obj Y) (fun val h => Sum.inl (F.map f val)) (fun val h => Sum.inr (G.map f val)) x ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>s : CategoryTheory.Limits.BinaryCofan F G<GOAL>(CategoryTheory.FunctorToTypes.binaryCoproductColimit F G).desc s = CategoryTheory.FunctorToTypes.coprod.desc s.inl s.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom = CategoryTheory.FunctorToTypes.coprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>x : F.obj a<GOAL>(CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom.app a (CategoryTheory.Limits.coprod.inl.app a x) = Sum.inl x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom = CategoryTheory.FunctorToTypes.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>x : G.obj a<GOAL>(CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom.app a (CategoryTheory.Limits.coprod.inr.app a x) = Sum.inr x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inl (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv = CategoryTheory.Limits.coprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>x : F.obj a<GOAL>(CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a (Sum.inl x) = CategoryTheory.Limits.coprod.inl.app a x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<GOAL>CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inr (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv = CategoryTheory.Limits.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>x : G.obj a<GOAL>(CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a (Sum.inr x) = CategoryTheory.Limits.coprod.inr.app a x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>z : F.obj a ⊕ G.obj a<GOAL>(CategoryTheory.FunctorToTypes.binaryCoproductEquiv F G a).symm z = (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>a : C<VAR>z : (F ⨿ G).obj a<GOAL>(CategoryTheory.FunctorToTypes.binaryCoproductEquiv F G a) z = (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom.app a z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>J : Type w<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<VAR>c : CategoryTheory.Limits.Cone F<VAR>X : CategoryTheory.Limits.WidePullbackShape J<GOAL>(CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c).π.app X = Option.casesOn X c.pt.hom fun j => (c.π.app { as := j }).left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>J : Type w<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c).pt = c.pt.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>J : Type w<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<GOAL>∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).map f).hom = f.hom.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>J : Type w<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).obj c = CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>J : Type w<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<VAR>c : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)<GOAL>((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).obj c).pt = CategoryTheory.Over.mk (c.π.app none)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>J : Type w<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<VAR>c : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)<GOAL>∀ (x : CategoryTheory.Discrete J), ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).obj c).π.app x = match x with | { as := j } => CategoryTheory.Over.homMk (c.π.app (some j)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>J : Type w<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<GOAL>∀ {X Y : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)} (f : X ⟶ Y), ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).map f).hom = CategoryTheory.Over.homMk f.hom ⋯
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<GOAL>(CategoryTheory.Over.ConstructProducts.conesEquiv B F).functor = CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<GOAL>(CategoryTheory.Over.ConstructProducts.conesEquiv B F).unitIso = CategoryTheory.Over.ConstructProducts.conesEquivUnitIso B F
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<GOAL>(CategoryTheory.Over.ConstructProducts.conesEquiv B F).inverse = CategoryTheory.Over.ConstructProducts.conesEquivInverse B F
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<GOAL>(CategoryTheory.Over.ConstructProducts.conesEquiv B F).counitIso = CategoryTheory.Over.ConstructProducts.conesEquivCounitIso B F
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>F : CategoryTheory.Discrete J ⥤ CategoryTheory.Over B<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)<GOAL>CategoryTheory.Limits.HasLimit F
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C<VAR>B : C<GOAL>CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.Over B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>B : C<GOAL>CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasWidePullbacks C<VAR>B : C<GOAL>CategoryTheory.Limits.HasProducts (CategoryTheory.Over B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteWidePullbacks C<VAR>B : C<GOAL>CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Over B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<GOAL>CategoryTheory.Limits.HasTerminal (CategoryTheory.Over B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>self : CategoryTheory.StrongEpi f<VAR>X Y : C<VAR>z : X ⟶ Y<VAR>CategoryTheory.Mono z<GOAL>CategoryTheory.HasLiftingProperty f z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>self : CategoryTheory.StrongEpi f<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>CategoryTheory.Epi f<VAR>hf : ∀ (X Y : C) (z : X ⟶ Y), CategoryTheory.Mono z → ∀ (u : P ⟶ X) (v : Q ⟶ Y) (sq : CategoryTheory.CommSq u f z v), sq.HasLift<GOAL>CategoryTheory.StrongEpi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>self : CategoryTheory.StrongMono f<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>self : CategoryTheory.StrongMono f<VAR>X Y : C<VAR>z : X ⟶ Y<VAR>CategoryTheory.Epi z<GOAL>CategoryTheory.HasLiftingProperty z f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>CategoryTheory.Mono f<VAR>hf : ∀ (X Y : C) (z : X ⟶ Y), CategoryTheory.Epi z → ∀ (u : X ⟶ P) (v : Y ⟶ Q) (sq : CategoryTheory.CommSq u z f v), sq.HasLift<GOAL>CategoryTheory.StrongMono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>CategoryTheory.StrongEpi f<VAR>CategoryTheory.StrongEpi g<GOAL>CategoryTheory.StrongEpi (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>CategoryTheory.StrongMono f<VAR>CategoryTheory.StrongMono g<GOAL>CategoryTheory.StrongMono (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>CategoryTheory.StrongEpi (CategoryTheory.CategoryStruct.comp f g)<GOAL>CategoryTheory.StrongEpi g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>CategoryTheory.StrongMono (CategoryTheory.CategoryStruct.comp f g)<GOAL>CategoryTheory.StrongMono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g<VAR>h : CategoryTheory.StrongEpi f<GOAL>CategoryTheory.StrongEpi g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g<VAR>h : CategoryTheory.StrongMono f<GOAL>CategoryTheory.StrongMono g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g<GOAL>CategoryTheory.StrongEpi f ↔ CategoryTheory.StrongEpi g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g<GOAL>CategoryTheory.StrongMono f ↔ CategoryTheory.StrongMono g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.StrongEpi f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>CategoryTheory.Epi f<VAR>CategoryTheory.StrongMono f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.StrongEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.StrongEpi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.StrongMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.StrongMono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>CategoryTheory.StrongEpiCategory C<VAR>f : P ⟶ Q<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.StrongEpi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>CategoryTheory.StrongMonoCategory C<VAR>f : P ⟶ Q<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.StrongMono 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>self : CategoryTheory.Limits.HasLimit F<GOAL>Nonempty (CategoryTheory.Limits.LimitCone 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.LimitCone 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>self : CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F : J ⥤ C<GOAL>CategoryTheory.Limits.HasLimit F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<GOAL>CategoryTheory.Limits.HasLimitsOfShape J C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimits C<VAR>J : Type v<VAR>CategoryTheory.Category.{v, v} J<GOAL>CategoryTheory.Limits.HasLimitsOfShape 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.HasLimit F<GOAL>(CategoryTheory.Limits.limit.cone F).pt = CategoryTheory.Limits.limit 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.HasLimit F<GOAL>(CategoryTheory.Limits.limit.cone F).π.app = CategoryTheory.Limits.limit.π 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.HasLimit F<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>CategoryTheory.Limits.limit.π F j ≫ F.map f = 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>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.limit.isLimit F).lift c = CategoryTheory.Limits.limit.lift 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.HasLimit F<VAR>c : CategoryTheory.Limits.Cone F<VAR>j : J<GOAL>CategoryTheory.Limits.limit.lift F c ≫ CategoryTheory.Limits.limit.π F j = 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.HasLimit F<VAR>CategoryTheory.Limits.HasLimit G<VAR>α : F ⟶ G<VAR>j : J<GOAL>CategoryTheory.Limits.limMap α ≫ CategoryTheory.Limits.limit.π G j = CategoryTheory.Limits.limit.π F j ≫ α.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.HasLimit F<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.limit.coneMorphism c).hom = CategoryTheory.Limits.limit.lift 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.HasLimit F<VAR>c : CategoryTheory.Limits.Cone F<VAR>j : J<GOAL>(CategoryTheory.Limits.limit.coneMorphism c).hom ≫ CategoryTheory.Limits.limit.π F j = 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.HasLimit F<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>j : J<GOAL>(hc.conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit F)).hom ≫ CategoryTheory.Limits.limit.π F j = 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.HasLimit F<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>j : J<GOAL>((CategoryTheory.Limits.limit.isLimit F).conePointUniqueUpToIso hc).inv ≫ CategoryTheory.Limits.limit.π F j = 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.HasLimit F<VAR>t : CategoryTheory.Limits.Cone F<GOAL>∃! l, ∀ (j : J), l ≫ CategoryTheory.Limits.limit.π F j = 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.HasLimit F<VAR>t : CategoryTheory.Limits.LimitCone F<VAR>j : J<GOAL>(CategoryTheory.Limits.limit.isoLimitCone t).hom ≫ t.cone.π.app j = 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>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<VAR>t : CategoryTheory.Limits.LimitCone F<VAR>j : J<GOAL>(CategoryTheory.Limits.limit.isoLimitCone t).inv ≫ CategoryTheory.Limits.limit.π F j = t.cone.π.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.HasLimit F<VAR>X : C<VAR>f f' : X ⟶ CategoryTheory.Limits.limit F<VAR>w : ∀ (j : J), f ≫ CategoryTheory.Limits.limit.π F j = f' ≫ CategoryTheory.Limits.limit.π F j<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 G : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<VAR>CategoryTheory.Limits.HasLimit G<VAR>c : CategoryTheory.Limits.Cone F<VAR>α : F ⟶ G<GOAL>CategoryTheory.Limits.limit.lift F c ≫ CategoryTheory.Limits.limMap α = CategoryTheory.Limits.limit.lift G ((CategoryTheory.Limits.Cones.postcompose α).obj 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.HasLimit F<GOAL>CategoryTheory.Limits.limit.lift F (CategoryTheory.Limits.limit.cone F) = 𝟙 (CategoryTheory.Limits.limit 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.HasLimit F<VAR>W : C<VAR>f : ULift.{u₁, v} (W ⟶ CategoryTheory.Limits.limit F)<GOAL>(CategoryTheory.Limits.limit.homIso F W).hom f = (CategoryTheory.Functor.const J).map f.down ≫ (CategoryTheory.Limits.limit.cone 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.HasLimit F<VAR>c : CategoryTheory.Limits.Cone F<VAR>X : C<VAR>f : X ⟶ c.pt<GOAL>CategoryTheory.Limits.limit.lift F (c.extend f) = f ≫ CategoryTheory.Limits.limit.lift F c
<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.HasLimit F<VAR>α : F ≅ G<GOAL>CategoryTheory.Limits.HasLimit G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J K : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.Category.{v₂, u₁} K<VAR>F : J ⥤ C<VAR>G : K ⥤ C<VAR>h : F.cones ≅ G.cones<VAR>CategoryTheory.Limits.HasLimit F<GOAL>CategoryTheory.Limits.HasLimit 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.HasLimit F<VAR>CategoryTheory.Limits.HasLimit G<VAR>w : F ≅ G<VAR>j : J<GOAL>(CategoryTheory.Limits.HasLimit.isoOfNatIso w).hom ≫ CategoryTheory.Limits.limit.π G j = CategoryTheory.Limits.limit.π F j ≫ w.hom.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.HasLimit F<VAR>CategoryTheory.Limits.HasLimit G<VAR>w : F ≅ G<VAR>j : J<GOAL>(CategoryTheory.Limits.HasLimit.isoOfNatIso w).inv ≫ CategoryTheory.Limits.limit.π F j = CategoryTheory.Limits.limit.π G j ≫ w.inv.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.HasLimit F<VAR>CategoryTheory.Limits.HasLimit G<VAR>t : CategoryTheory.Limits.Cone F<VAR>w : F ≅ G<GOAL>CategoryTheory.Limits.limit.lift F t ≫ (CategoryTheory.Limits.HasLimit.isoOfNatIso w).hom = CategoryTheory.Limits.limit.lift G ((CategoryTheory.Limits.Cones.postcompose 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.HasLimit F<VAR>CategoryTheory.Limits.HasLimit G<VAR>t : CategoryTheory.Limits.Cone G<VAR>w : F ≅ G<GOAL>CategoryTheory.Limits.limit.lift G t ≫ (CategoryTheory.Limits.HasLimit.isoOfNatIso w).inv = CategoryTheory.Limits.limit.lift F ((CategoryTheory.Limits.Cones.postcompose 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.HasLimit F<VAR>G : K ⥤ C<VAR>CategoryTheory.Limits.HasLimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>k : K<GOAL>(CategoryTheory.Limits.HasLimit.isoOfEquivalence e w).hom ≫ CategoryTheory.Limits.limit.π G k = CategoryTheory.Limits.limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app 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.HasLimit F<VAR>G : K ⥤ C<VAR>CategoryTheory.Limits.HasLimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>j : J<GOAL>(CategoryTheory.Limits.HasLimit.isoOfEquivalence e w).inv ≫ CategoryTheory.Limits.limit.π F j = CategoryTheory.Limits.limit.π G (e.functor.obj j) ≫ w.hom.app 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.HasLimit F<VAR>E : K ⥤ J<VAR>CategoryTheory.Limits.HasLimit (E ⋙ F)<VAR>k : K<GOAL>CategoryTheory.Limits.limit.pre F E ≫ CategoryTheory.Limits.limit.π (E ⋙ F) k = CategoryTheory.Limits.limit.π 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.HasLimit F<VAR>E : K ⥤ J<VAR>CategoryTheory.Limits.HasLimit (E ⋙ F)<VAR>c : CategoryTheory.Limits.Cone F<GOAL>CategoryTheory.Limits.limit.lift F c ≫ CategoryTheory.Limits.limit.pre F E = CategoryTheory.Limits.limit.lift (E ⋙ F) (CategoryTheory.Limits.Cone.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.HasLimit F<VAR>E : K ⥤ J<VAR>CategoryTheory.Limits.HasLimit (E ⋙ F)<VAR>L : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} L<VAR>D : L ⥤ K<VAR>h : CategoryTheory.Limits.HasLimit (D ⋙ E ⋙ F)<GOAL>CategoryTheory.Limits.limit.pre F E ≫ CategoryTheory.Limits.limit.pre (E ⋙ F) D = CategoryTheory.Limits.limit.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.HasLimit F<VAR>E : K ⥤ J<VAR>CategoryTheory.Limits.HasLimit (E ⋙ F)<VAR>s : CategoryTheory.Limits.LimitCone (E ⋙ F)<VAR>t : CategoryTheory.Limits.LimitCone F<GOAL>CategoryTheory.Limits.limit.pre F E = (CategoryTheory.Limits.limit.isoLimitCone t).hom ≫ s.isLimit.lift (CategoryTheory.Limits.Cone.whisker E t.cone) ≫ (CategoryTheory.Limits.limit.isoLimitCone s).inv