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>c : CategoryTheory.Limits.Cone F<VAR>X : C<VAR>f : X ⟶ c.pt<GOAL>(c.extend f).π = c.extensions.app (Opposite.op X) { down := 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>c : CategoryTheory.Limits.Cone F<VAR>X : C<VAR>f : X ⟶ c.pt<GOAL>(c.extend f).pt = X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cone.whisker E c).π = CategoryTheory.whiskerLeft 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>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cone.whisker E c).pt = c.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>c : CategoryTheory.Limits.Cocone F<VAR>X : C<VAR>f : (CategoryTheory.coyoneda.obj (Opposite.op c.pt) ⋙ CategoryTheory.uliftFunctor.{u₁, v₃}).obj X<GOAL>c.extensions.app X f = c.ι ≫ (CategoryTheory.Functor.const J).map f.down
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>Y : C<VAR>f : c.pt ⟶ Y<GOAL>(c.extend f).ι = c.extensions.app Y { down := 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>c : CategoryTheory.Limits.Cocone F<VAR>Y : C<VAR>f : c.pt ⟶ Y<GOAL>(c.extend f).pt = Y
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocone.whisker E c).ι = CategoryTheory.whiskerLeft 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>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocone.whisker E c).pt = c.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>A B : CategoryTheory.Limits.Cone F<VAR>self : CategoryTheory.Limits.ConeMorphism A B<VAR>j : J<GOAL>self.hom ≫ B.π.app j = A.π.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>B : CategoryTheory.Limits.Cone F<GOAL>(𝟙 B).hom = 𝟙 B.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<GOAL>∀ {X Y Z : CategoryTheory.Limits.Cone F} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g).hom = f.hom ≫ g.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>c c' : CategoryTheory.Limits.Cone F<VAR>f g : c ⟶ c'<VAR>w : f.hom = g.hom<GOAL>f = g
<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>c c' : CategoryTheory.Limits.Cone F<VAR>φ : c.pt ≅ c'.pt<VAR>w : ∀ (j : J), c.π.app j = φ.hom ≫ c'.π.app j := by aesop_cat<GOAL>(CategoryTheory.Limits.Cones.ext φ w).hom.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>c c' : CategoryTheory.Limits.Cone F<VAR>φ : c.pt ≅ c'.pt<VAR>w : ∀ (j : J), c.π.app j = φ.hom ≫ c'.π.app j := by aesop_cat<GOAL>(CategoryTheory.Limits.Cones.ext φ w).inv.hom = φ.inv
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cones.eta c).inv.hom = 𝟙 c.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>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cones.eta c).hom.hom = 𝟙 c.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>K : J ⥤ C<VAR>c d : CategoryTheory.Limits.Cone K<VAR>f : c ⟶ d<VAR>i : CategoryTheory.IsIso f.hom<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 : CategoryTheory.Limits.Cone F<VAR>X : C<VAR>f : X ⟶ s.pt<GOAL>(CategoryTheory.Limits.Cones.extend s f).hom = 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 : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cones.extendId s).hom.hom = 𝟙 s.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>s : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cones.extendId s).inv.hom = 𝟙 s.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>s : CategoryTheory.Limits.Cone F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ s.pt<GOAL>(CategoryTheory.Limits.Cones.extendComp s f g).inv.hom = 𝟙 X
<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 : CategoryTheory.Limits.Cone F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ s.pt<GOAL>(CategoryTheory.Limits.Cones.extendComp s f g).hom.hom = 𝟙 X
<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 : CategoryTheory.Limits.Cone F<VAR>X : C<VAR>f : X ≅ s.pt<GOAL>(CategoryTheory.Limits.Cones.extendIso s f).hom.hom = f.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 : CategoryTheory.Limits.Cone F<VAR>X : C<VAR>f : X ≅ s.pt<GOAL>(CategoryTheory.Limits.Cones.extendIso s f).inv.hom = f.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>α : F ⟶ G<VAR>c : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cones.postcompose α).obj c).pt = c.pt
<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>α : F ⟶ G<VAR>c : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cones.postcompose α).obj c).π = 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>α : F ⟶ G<GOAL>∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cones.postcompose α).map f).hom = f.hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F G H : J ⥤ C<VAR>α : F ⟶ G<VAR>β : G ⟶ H<VAR>X : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cones.postcomposeComp α β).inv.app X).hom = 𝟙 X.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F G H : J ⥤ C<VAR>α : F ⟶ G<VAR>β : G ⟶ H<VAR>X : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cones.postcomposeComp α β).hom.app X).hom = 𝟙 X.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>X : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cones.postcomposeId.inv.app X).hom = 𝟙 X.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>X : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cones.postcomposeId.hom.app X).hom = 𝟙 X.pt
<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>α : F ≅ G<GOAL>(CategoryTheory.Limits.Cones.postcomposeEquivalence α).counitIso = CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Limits.Cones.postcompose α.inv ⋙ CategoryTheory.Limits.Cones.postcompose α.hom).obj s).pt) ⋯) ⋯
<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>α : F ≅ G<GOAL>(CategoryTheory.Limits.Cones.postcomposeEquivalence α).inverse = CategoryTheory.Limits.Cones.postcompose α.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>α : F ≅ G<GOAL>(CategoryTheory.Limits.Cones.postcomposeEquivalence α).unitIso = CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((𝟭 (CategoryTheory.Limits.Cone F)).obj s).pt) ⋯) ⋯
<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>α : F ≅ G<GOAL>(CategoryTheory.Limits.Cones.postcomposeEquivalence α).functor = CategoryTheory.Limits.Cones.postcompose α.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>E : K ⥤ J<GOAL>∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cones.whiskering E).map f).hom = f.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>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cones.whiskering E).obj c = 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>e : K ≌ J<GOAL>(CategoryTheory.Limits.Cones.whiskeringEquivalence e).counitIso = CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (((CategoryTheory.Limits.Cones.whiskering e.inverse ⋙ CategoryTheory.Limits.Cones.postcompose (e.invFunIdAssoc F).hom) ⋙ CategoryTheory.Limits.Cones.whiskering e.functor).obj s).pt) ⋯) ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>e : K ≌ J<GOAL>(CategoryTheory.Limits.Cones.whiskeringEquivalence e).inverse = CategoryTheory.Limits.Cones.whiskering e.inverse ⋙ CategoryTheory.Limits.Cones.postcompose (e.invFunIdAssoc F).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>e : K ≌ J<GOAL>(CategoryTheory.Limits.Cones.whiskeringEquivalence e).functor = CategoryTheory.Limits.Cones.whiskering e.functor
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>e : K ≌ J<GOAL>(CategoryTheory.Limits.Cones.whiskeringEquivalence e).unitIso = CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((𝟭 (CategoryTheory.Limits.Cone F)).obj s).pt) ⋯) ⋯
<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>G : K ⥤ C<VAR>e : K ≌ J<VAR>α : e.functor ⋙ F ≅ G<GOAL>(CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).functor = CategoryTheory.Limits.Cones.whiskering e.functor ⋙ CategoryTheory.Limits.Cones.postcompose α.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>G : K ⥤ C<VAR>e : K ≌ J<VAR>α : e.functor ⋙ F ≅ G<GOAL>(CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).unitIso = CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯ ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.Limits.Cones.whiskering e.functor) (CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯) (CategoryTheory.Limits.Cones.whiskering e.inverse ⋙ CategoryTheory.Limits.Cones.postcompose (e.invFunIdAssoc F).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>G : K ⥤ C<VAR>e : K ≌ J<VAR>α : e.functor ⋙ F ≅ G<GOAL>(CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).inverse = CategoryTheory.Limits.Cones.postcompose α.inv ⋙ CategoryTheory.Limits.Cones.whiskering e.inverse ⋙ CategoryTheory.Limits.Cones.postcompose (e.invFunIdAssoc F).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>G : K ⥤ C<VAR>e : K ≌ J<VAR>α : e.functor ⋙ F ≅ G<GOAL>(CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).counitIso = CategoryTheory.isoWhiskerLeft (CategoryTheory.Limits.Cones.postcompose α.inv) (CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯) (CategoryTheory.Limits.Cones.postcompose α.hom)) ≪≫ CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.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<GOAL>∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cones.forget F).map f = f.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>t : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cones.forget F).obj t = t.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>A : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cones.functoriality F G).obj A).pt = G.obj A.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>A : CategoryTheory.Limits.Cone F<VAR>j : J<GOAL>((CategoryTheory.Limits.Cones.functoriality F G).obj A).π.app j = G.map (A.π.app j)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<GOAL>∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cones.functoriality F G).map f).hom = G.map f.hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>e : C ≌ D<GOAL>(CategoryTheory.Limits.Cones.functorialityEquivalence F e).unitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cones.ext (e.unitIso.app ((𝟭 (CategoryTheory.Limits.Cone F)).obj c).1) ⋯) ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>e : C ≌ D<GOAL>(CategoryTheory.Limits.Cones.functorialityEquivalence F e).counitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cones.ext (e.counitIso.app c.pt) ⋯) ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>e : C ≌ D<GOAL>(CategoryTheory.Limits.Cones.functorialityEquivalence F e).inverse = CategoryTheory.Limits.Cones.functoriality (F ⋙ e.functor) e.inverse ⋙ (CategoryTheory.Limits.Cones.postcomposeEquivalence (F.associator e.functor e.inverse ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso.symm ≪≫ F.rightUnitor)).functor
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>e : C ≌ D<GOAL>(CategoryTheory.Limits.Cones.functorialityEquivalence F e).functor = CategoryTheory.Limits.Cones.functoriality F e.functor
<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>A B : CategoryTheory.Limits.Cocone F<VAR>self : CategoryTheory.Limits.CoconeMorphism A B<VAR>j : J<GOAL>A.ι.app j ≫ self.hom = B.ι.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<GOAL>∀ {X Y Z : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g).hom = f.hom ≫ g.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>B : CategoryTheory.Limits.Cocone F<GOAL>(𝟙 B).hom = 𝟙 B.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>c c' : CategoryTheory.Limits.Cocone F<VAR>f g : c ⟶ c'<VAR>w : f.hom = g.hom<GOAL>f = g
<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>c c' : CategoryTheory.Limits.Cocone F<VAR>φ : c.pt ≅ c'.pt<VAR>w : ∀ (j : J), c.ι.app j ≫ φ.hom = c'.ι.app j := by aesop_cat<GOAL>(CategoryTheory.Limits.Cocones.ext φ w).inv.hom = φ.inv
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c c' : CategoryTheory.Limits.Cocone F<VAR>φ : c.pt ≅ c'.pt<VAR>w : ∀ (j : J), c.ι.app j ≫ φ.hom = c'.ι.app j := by aesop_cat<GOAL>(CategoryTheory.Limits.Cocones.ext φ w).hom.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>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocones.eta c).inv.hom = 𝟙 c.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>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocones.eta c).hom.hom = 𝟙 c.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>K : J ⥤ C<VAR>c d : CategoryTheory.Limits.Cocone K<VAR>f : c ⟶ d<VAR>i : CategoryTheory.IsIso f.hom<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 : CategoryTheory.Limits.Cocone F<VAR>X : C<VAR>f : s.pt ⟶ X<GOAL>(CategoryTheory.Limits.Cocones.extend s f).hom = 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 : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocones.extendId s).inv.hom = 𝟙 s.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>s : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocones.extendId s).hom.hom = 𝟙 s.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>s : CategoryTheory.Limits.Cocone F<VAR>X Y : C<VAR>f : s.pt ⟶ X<VAR>g : X ⟶ Y<GOAL>(CategoryTheory.Limits.Cocones.extendComp s f g).inv.hom = 𝟙 Y
<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 : CategoryTheory.Limits.Cocone F<VAR>X Y : C<VAR>f : s.pt ⟶ X<VAR>g : X ⟶ Y<GOAL>(CategoryTheory.Limits.Cocones.extendComp s f g).hom.hom = 𝟙 Y
<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 : CategoryTheory.Limits.Cocone F<VAR>X : C<VAR>f : s.pt ≅ X<GOAL>(CategoryTheory.Limits.Cocones.extendIso s f).inv.hom = f.inv
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>s : CategoryTheory.Limits.Cocone F<VAR>X : C<VAR>f : s.pt ≅ X<GOAL>(CategoryTheory.Limits.Cocones.extendIso s f).hom.hom = f.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>α : G ⟶ F<GOAL>∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocones.precompose α).map f).hom = f.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>α : G ⟶ F<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Limits.Cocones.precompose α).obj c).pt = c.pt
<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>α : G ⟶ F<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Limits.Cocones.precompose α).obj c).ι = α ≫ 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>α : G ≅ F<GOAL>(CategoryTheory.Limits.Cocones.precomposeEquivalence α).functor = CategoryTheory.Limits.Cocones.precompose α.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>α : G ≅ F<GOAL>(CategoryTheory.Limits.Cocones.precomposeEquivalence α).unitIso = CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((𝟭 (CategoryTheory.Limits.Cocone F)).obj s).pt) ⋯) ⋯
<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>α : G ≅ F<GOAL>(CategoryTheory.Limits.Cocones.precomposeEquivalence α).counitIso = CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Limits.Cocones.precompose α.inv ⋙ CategoryTheory.Limits.Cocones.precompose α.hom).obj s).pt) ⋯) ⋯
<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>α : G ≅ F<GOAL>(CategoryTheory.Limits.Cocones.precomposeEquivalence α).inverse = CategoryTheory.Limits.Cocones.precompose α.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>E : K ⥤ J<GOAL>∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocones.whiskering E).map f).hom = f.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>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocones.whiskering E).obj c = CategoryTheory.Limits.Cocone.whisker E c
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>e : K ≌ J<GOAL>(CategoryTheory.Limits.Cocones.whiskeringEquivalence e).inverse = CategoryTheory.Limits.Cocones.whiskering e.inverse ⋙ CategoryTheory.Limits.Cocones.precompose (F.leftUnitor.inv ≫ CategoryTheory.whiskerRight e.counitIso.inv F ≫ (e.inverse.associator e.functor F).inv)