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>F : J ⥤ C<VAR>s t : CategoryTheory.Limits.Cone F<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<GOAL>(P.uniqueUpToIso Q).hom = Q.liftConeMorphism s
<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>s t : CategoryTheory.Limits.Cone F<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<GOAL>(P.uniqueUpToIso Q).inv = P.liftConeMorphism t
<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>s t : CategoryTheory.Limits.Cone F<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>f : s ⟶ t<GOAL>CategoryTheory.IsIso 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>s t : CategoryTheory.Limits.Cone F<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>j : J<GOAL>(P.conePointUniqueUpToIso Q).hom ≫ t.π.app j = s.π.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>s t : CategoryTheory.Limits.Cone F<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>j : J<GOAL>(P.conePointUniqueUpToIso Q).inv ≫ s.π.app 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>r s t : CategoryTheory.Limits.Cone F<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<GOAL>P.lift r ≫ (P.conePointUniqueUpToIso Q).hom = Q.lift r
<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>r s t : CategoryTheory.Limits.Cone F<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<GOAL>Q.lift r ≫ (P.conePointUniqueUpToIso Q).inv = P.lift r
<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>r t : CategoryTheory.Limits.Cone F<VAR>P : CategoryTheory.Limits.IsLimit r<VAR>i : r ≅ t<VAR>s : CategoryTheory.Limits.Cone F<GOAL>(P.ofIsoLimit i).lift s = P.lift s ≫ i.hom.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>r t : CategoryTheory.Limits.Cone F<VAR>i : r ≅ t<VAR>P : CategoryTheory.Limits.IsLimit r<GOAL>(CategoryTheory.Limits.IsLimit.equivIsoLimit i) P = P.ofIsoLimit i
<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>r t : CategoryTheory.Limits.Cone F<VAR>i : r ≅ t<VAR>P : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.IsLimit.equivIsoLimit i).symm P = P.ofIsoLimit i.symm
<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>t : CategoryTheory.Limits.Cone F<VAR>h : CategoryTheory.Limits.IsLimit t<VAR>W : C<VAR>m : W ⟶ t.pt<GOAL>m = h.lift { pt := W, π := { app := fun b => m ≫ t.π.app b, naturality := ⋯ } }
<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>t : CategoryTheory.Limits.Cone F<VAR>h : CategoryTheory.Limits.IsLimit t<VAR>W : C<VAR>f f' : W ⟶ t.pt<VAR>w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j<GOAL>f = 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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>G : K ⥤ D<VAR>h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F<VAR>c : CategoryTheory.Limits.Cone G<VAR>P : CategoryTheory.Limits.IsLimit (h.functor.obj c)<VAR>s : CategoryTheory.Limits.Cone G<GOAL>((CategoryTheory.Limits.IsLimit.ofConeEquiv h) P).lift s = ((h.unitIso.hom.app s).hom ≫ (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom) ≫ (h.unitIso.inv.app c).hom
<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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>G : K ⥤ D<VAR>h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F<VAR>c : CategoryTheory.Limits.Cone G<VAR>P : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.IsLimit.ofConeEquiv h).symm P).lift s = (h.counitIso.inv.app s).hom ≫ (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom
<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>s : CategoryTheory.Limits.Cone F<VAR>t : CategoryTheory.Limits.Cone G<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>w : F ≅ G<GOAL>(P.conePointsIsoOfNatIso Q w).inv = CategoryTheory.Limits.IsLimit.map t P w.inv
<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>s : CategoryTheory.Limits.Cone F<VAR>t : CategoryTheory.Limits.Cone G<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>w : F ≅ G<GOAL>(P.conePointsIsoOfNatIso Q w).hom = CategoryTheory.Limits.IsLimit.map s Q w.hom
<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>s : CategoryTheory.Limits.Cone F<VAR>t : CategoryTheory.Limits.Cone G<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>w : F ≅ G<VAR>j : J<GOAL>(P.conePointsIsoOfNatIso Q w).hom ≫ t.π.app j = s.π.app 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>s : CategoryTheory.Limits.Cone F<VAR>t : CategoryTheory.Limits.Cone G<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>w : F ≅ G<VAR>j : J<GOAL>(P.conePointsIsoOfNatIso Q w).inv ≫ s.π.app j = t.π.app 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>r s : CategoryTheory.Limits.Cone F<VAR>t : CategoryTheory.Limits.Cone G<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>w : F ≅ G<GOAL>P.lift r ≫ (P.conePointsIsoOfNatIso Q w).hom = CategoryTheory.Limits.IsLimit.map r Q w.hom
<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>r s : CategoryTheory.Limits.Cone G<VAR>t : CategoryTheory.Limits.Cone F<VAR>P : CategoryTheory.Limits.IsLimit t<VAR>Q : CategoryTheory.Limits.IsLimit s<VAR>w : F ≅ G<GOAL>Q.lift r ≫ (P.conePointsIsoOfNatIso Q w).inv = CategoryTheory.Limits.IsLimit.map r P w.inv
<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>s : CategoryTheory.Limits.Cone F<VAR>G : K ⥤ C<VAR>t : CategoryTheory.Limits.Cone G<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<GOAL>(P.conePointsIsoOfEquivalence Q e w).inv = P.lift ((CategoryTheory.Limits.Cones.equivalenceOfReindexing e w).functor.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>s : CategoryTheory.Limits.Cone F<VAR>G : K ⥤ C<VAR>t : CategoryTheory.Limits.Cone G<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>Q : CategoryTheory.Limits.IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<GOAL>(P.conePointsIsoOfEquivalence Q e w).hom = Q.lift ((CategoryTheory.Limits.Cones.equivalenceOfReindexing e.symm ((CategoryTheory.isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G)).functor.obj s)
<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>t : CategoryTheory.Limits.Cone F<VAR>h : CategoryTheory.Limits.IsLimit t<VAR>W : C<VAR>f : ULift.{u₁, v₃} (W ⟶ t.pt)<GOAL>(h.homIso W).hom f = (t.extend 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>X : C<VAR>h : CategoryTheory.yoneda.obj X ⋙ CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>s : CategoryTheory.Limits.Cone F<GOAL>CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h (CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h s) = s
<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>X : C<VAR>h : CategoryTheory.yoneda.obj X ⋙ CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h (CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h 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>X : C<VAR>h : CategoryTheory.yoneda.obj X ⋙ CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h f = (CategoryTheory.Limits.IsLimit.OfNatIso.limitCone h).extend 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>X : C<VAR>h : CategoryTheory.yoneda.obj X ⋙ CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>s : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.IsLimit.OfNatIso.limitCone h).extend (CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h s) = s
<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>t : CategoryTheory.Limits.Cocone F<VAR>self : CategoryTheory.Limits.IsColimit t<VAR>s : CategoryTheory.Limits.Cocone F<VAR>m : t.pt ⟶ s.pt<GOAL>(∀ (j : J), t.ι.app j ≫ m = s.ι.app j) → m = self.desc s
<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>t : CategoryTheory.Limits.Cocone F<VAR>self : CategoryTheory.Limits.IsColimit t<VAR>s : CategoryTheory.Limits.Cocone F<VAR>j : J<GOAL>t.ι.app j ≫ self.desc s = s.ι.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>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>d : CategoryTheory.Limits.Cocone G<VAR>α : F ⟶ G<VAR>j : J<GOAL>c.ι.app j ≫ hc.map d α = α.app j ≫ d.ι.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>t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<GOAL>h.desc t = 𝟙 t.pt
<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>t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>(h.descCoconeMorphism s).hom = h.desc s
<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>s t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<VAR>f f' : t ⟶ s<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>t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>∃! d, ∀ (j : J), t.ι.app j ≫ d = s.ι.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>t : CategoryTheory.Limits.Cocone F<VAR>desc : (s : CategoryTheory.Limits.Cocone F) → t ⟶ s<VAR>uniq' : ∀ (s : CategoryTheory.Limits.Cocone F) (m : t ⟶ s), m = desc s<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.IsColimit.mkCoconeMorphism desc uniq').desc s = (desc s).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>s t : CategoryTheory.Limits.Cocone F<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<GOAL>(P.uniqueUpToIso Q).inv = Q.descCoconeMorphism s
<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>s t : CategoryTheory.Limits.Cocone F<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<GOAL>(P.uniqueUpToIso Q).hom = P.descCoconeMorphism t
<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>s t : CategoryTheory.Limits.Cocone F<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>f : s ⟶ t<GOAL>CategoryTheory.IsIso 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>s t : CategoryTheory.Limits.Cocone F<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>j : J<GOAL>s.ι.app j ≫ (P.coconePointUniqueUpToIso Q).hom = 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>s t : CategoryTheory.Limits.Cocone F<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>j : J<GOAL>t.ι.app j ≫ (P.coconePointUniqueUpToIso Q).inv = s.ι.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>r s t : CategoryTheory.Limits.Cocone F<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<GOAL>(P.coconePointUniqueUpToIso Q).hom ≫ Q.desc r = P.desc r
<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>r s t : CategoryTheory.Limits.Cocone F<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<GOAL>(P.coconePointUniqueUpToIso Q).inv ≫ P.desc r = Q.desc r
<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>r t : CategoryTheory.Limits.Cocone F<VAR>P : CategoryTheory.Limits.IsColimit r<VAR>i : r ≅ t<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>(P.ofIsoColimit i).desc s = i.inv.hom ≫ P.desc s
<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>r t : CategoryTheory.Limits.Cocone F<VAR>i : r ≅ t<VAR>P : CategoryTheory.Limits.IsColimit r<GOAL>(CategoryTheory.Limits.IsColimit.equivIsoColimit i) P = P.ofIsoColimit i
<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>r t : CategoryTheory.Limits.Cocone F<VAR>i : r ≅ t<VAR>P : CategoryTheory.Limits.IsColimit t<GOAL>(CategoryTheory.Limits.IsColimit.equivIsoColimit i).symm P = P.ofIsoColimit i.symm
<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>t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<VAR>W : C<VAR>m : t.pt ⟶ W<GOAL>m = h.desc { pt := W, ι := { app := fun b => t.ι.app b ≫ m, naturality := ⋯ } }
<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>t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<VAR>W : C<VAR>f f' : t.pt ⟶ W<VAR>w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'<GOAL>f = 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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>G : K ⥤ D<VAR>h : CategoryTheory.Limits.Cocone G ≌ CategoryTheory.Limits.Cocone F<VAR>c : CategoryTheory.Limits.Cocone G<VAR>P : CategoryTheory.Limits.IsColimit (h.functor.obj c)<VAR>s : CategoryTheory.Limits.Cocone G<GOAL>((CategoryTheory.Limits.IsColimit.ofCoconeEquiv h) P).desc s = (h.unit.app c).hom ≫ (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))).hom ≫ (h.unitInv.app s).hom
<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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>G : K ⥤ D<VAR>h : CategoryTheory.Limits.Cocone G ≌ CategoryTheory.Limits.Cocone F<VAR>c : CategoryTheory.Limits.Cocone G<VAR>P : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Limits.IsColimit.ofCoconeEquiv h).symm P).desc s = (h.functor.map (P.descCoconeMorphism (h.inverse.obj s))).hom ≫ (h.counit.app s).hom
<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>s : CategoryTheory.Limits.Cocone F<VAR>t : CategoryTheory.Limits.Cocone G<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>w : F ≅ G<GOAL>(P.coconePointsIsoOfNatIso Q w).hom = P.map t w.hom
<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>s : CategoryTheory.Limits.Cocone F<VAR>t : CategoryTheory.Limits.Cocone G<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>w : F ≅ G<GOAL>(P.coconePointsIsoOfNatIso Q w).inv = Q.map s w.inv
<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>s : CategoryTheory.Limits.Cocone F<VAR>t : CategoryTheory.Limits.Cocone G<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>w : F ≅ G<VAR>j : J<GOAL>s.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).hom = w.hom.app 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 G : J ⥤ C<VAR>s : CategoryTheory.Limits.Cocone F<VAR>t : CategoryTheory.Limits.Cocone G<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>w : F ≅ G<VAR>j : J<GOAL>t.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).inv = w.inv.app j ≫ s.ι.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>s : CategoryTheory.Limits.Cocone F<VAR>r t : CategoryTheory.Limits.Cocone G<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>w : F ≅ G<GOAL>(P.coconePointsIsoOfNatIso Q w).hom ≫ Q.desc r = P.map r w.hom
<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>s : CategoryTheory.Limits.Cocone G<VAR>r t : CategoryTheory.Limits.Cocone F<VAR>P : CategoryTheory.Limits.IsColimit t<VAR>Q : CategoryTheory.Limits.IsColimit s<VAR>w : F ≅ G<GOAL>(P.coconePointsIsoOfNatIso Q w).inv ≫ P.desc r = Q.map r w.inv
<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>s : CategoryTheory.Limits.Cocone F<VAR>G : K ⥤ C<VAR>t : CategoryTheory.Limits.Cocone G<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<GOAL>(P.coconePointsIsoOfEquivalence Q e w).inv = Q.desc ((CategoryTheory.Limits.Cocones.equivalenceOfReindexing e.symm ((CategoryTheory.isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G)).functor.obj s)
<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>s : CategoryTheory.Limits.Cocone F<VAR>G : K ⥤ C<VAR>t : CategoryTheory.Limits.Cocone G<VAR>P : CategoryTheory.Limits.IsColimit s<VAR>Q : CategoryTheory.Limits.IsColimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<GOAL>(P.coconePointsIsoOfEquivalence Q e w).hom = P.desc ((CategoryTheory.Limits.Cocones.equivalenceOfReindexing e w).functor.obj t)
<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>t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<VAR>W : C<VAR>f : t.pt ⟶ W<GOAL>(h.homEquiv W) f = (t.extend 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>t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<VAR>W : C<VAR>f : ULift.{u₁, v₃} (t.pt ⟶ W)<GOAL>(h.homIso W).hom f = (t.extend 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>X : C<VAR>h : CategoryTheory.coyoneda.obj (Opposite.op X) ⋙ CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h (CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h s) = s
<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>X : C<VAR>h : CategoryTheory.coyoneda.obj (Opposite.op X) ⋙ CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h (CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h 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>X : C<VAR>h : CategoryTheory.coyoneda.obj (Opposite.op X) ⋙ CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h f = (CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone h).extend 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>X : C<VAR>h : CategoryTheory.coyoneda.obj (Opposite.op X) ⋙ CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone h).extend (CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h s) = s
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>f : J → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct fun j => G.obj (f j)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G<GOAL>(CategoryTheory.Limits.PreservesProduct.iso G f).hom = CategoryTheory.Limits.piComparison G f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>f : J → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G<GOAL>(CategoryTheory.Limits.PreservesCoproduct.iso G f).inv = CategoryTheory.Limits.sigmaComparison G f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.NormalMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ 0 ⋯)<GOAL>CategoryTheory.Epi f