ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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).counitIso = CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (((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)) ⋙ CategoryTheory.Limits.Cocones.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.Cocones.whiskeringEquivalence e).functor = CategoryTheory.Limits.Cocones.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.Cocones.whiskeringEquivalence e).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>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<VAR>X : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocones.equivalenceOfReindexing e α).functor.obj X = (CategoryTheory.Limits.Cocones.precompose α.inv).obj (CategoryTheory.Limits.Cocone.whisker e.functor 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>t : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocones.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>F : J ⥤ C<GOAL>∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cocones.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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>A : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Limits.Cocones.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<GOAL>∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocones.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>G : C ⥤ D<VAR>A : CategoryTheory.Limits.Cocone F<VAR>j : J<GOAL>((CategoryTheory.Limits.Cocones.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>e : C ≌ D<GOAL>(CategoryTheory.Limits.Cocones.functorialityEquivalence F e).counitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cocones.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.Cocones.functorialityEquivalence F e).unitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cocones.ext (e.unitIso.app ((𝟭 (CategoryTheory.Limits.Cocone 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.Cocones.functorialityEquivalence F e).functor = CategoryTheory.Limits.Cocones.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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>e : C ≌ D<GOAL>(CategoryTheory.Limits.Cocones.functorialityEquivalence F e).inverse = CategoryTheory.Limits.Cocones.functoriality (F ⋙ e.functor) e.inverse ⋙ (CategoryTheory.Limits.Cocones.precomposeEquivalence (F.associator e.functor e.inverse ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso.symm ≪≫ F.rightUnitor).symm).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>H : C ⥤ D<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(H.mapCone c).pt = H.obj 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>H : C ⥤ D<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<VAR>j : J<GOAL>(H.mapCone c).π.app j = H.map (c.π.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>H : C ⥤ D<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>(H.mapCocone c).pt = H.obj 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>H : C ⥤ D<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>j : J<GOAL>(H.mapCocone c).ι.app j = H.map (c.ι.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>H H' : C ⥤ D<VAR>α : H ≅ H'<VAR>X : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Functor.functorialityCompPostcompose α).inv.app X).hom = α.inv.app X.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>H H' : C ⥤ D<VAR>α : H ≅ H'<VAR>X : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Functor.functorialityCompPostcompose α).hom.app X).hom = α.hom.app X.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>H H' : C ⥤ D<VAR>α : H ≅ H'<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c).hom.hom = α.hom.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>H H' : C ⥤ D<VAR>α : H ≅ H'<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c).inv.hom = α.inv.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>H : C ⥤ D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>c : CategoryTheory.Limits.Cone F<GOAL>H.mapConePostcompose.hom.hom = 𝟙 (H.obj 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>H : C ⥤ D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>c : CategoryTheory.Limits.Cone F<GOAL>H.mapConePostcompose.inv.hom = 𝟙 (H.obj 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>H : C ⥤ D<VAR>F G : J ⥤ C<VAR>α : F ≅ G<VAR>c : CategoryTheory.Limits.Cone F<GOAL>H.mapConePostcomposeEquivalenceFunctor.hom.hom = 𝟙 (H.obj 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>H : C ⥤ D<VAR>F G : J ⥤ C<VAR>α : F ≅ G<VAR>c : CategoryTheory.Limits.Cone F<GOAL>H.mapConePostcomposeEquivalenceFunctor.inv.hom = 𝟙 (H.obj 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>H H' : C ⥤ D<VAR>α : H ≅ H'<VAR>X : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Functor.functorialityCompPrecompose α).hom.app X).hom = α.hom.app X.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>H H' : C ⥤ D<VAR>α : H ≅ H'<VAR>X : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Functor.functorialityCompPrecompose α).inv.app X).hom = α.inv.app X.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>H H' : C ⥤ D<VAR>α : H ≅ H'<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).inv.hom = α.inv.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>H H' : C ⥤ D<VAR>α : H ≅ H'<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).hom.hom = α.hom.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>H : C ⥤ D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>c : CategoryTheory.Limits.Cocone G<GOAL>H.mapCoconePrecompose.inv.hom = 𝟙 (H.obj 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>H : C ⥤ D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>c : CategoryTheory.Limits.Cocone G<GOAL>H.mapCoconePrecompose.hom.hom = 𝟙 (H.obj 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>H : C ⥤ D<VAR>F G : J ⥤ C<VAR>α : F ≅ G<VAR>c : CategoryTheory.Limits.Cocone G<GOAL>H.mapCoconePrecomposeEquivalenceFunctor.inv.hom = 𝟙 (H.obj 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>H : C ⥤ D<VAR>F G : J ⥤ C<VAR>α : F ≅ G<VAR>c : CategoryTheory.Limits.Cocone G<GOAL>H.mapCoconePrecomposeEquivalenceFunctor.hom.hom = 𝟙 (H.obj c.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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>H : C ⥤ D<VAR>F : J ⥤ C<VAR>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cone F<GOAL>H.mapConeWhisker.inv.hom = 𝟙 (H.obj c.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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>H : C ⥤ D<VAR>F : J ⥤ C<VAR>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cone F<GOAL>H.mapConeWhisker.hom.hom = 𝟙 (H.obj c.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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>H : C ⥤ D<VAR>F : J ⥤ C<VAR>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>H.mapCoconeWhisker.hom.hom = 𝟙 (H.obj c.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>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>H : C ⥤ D<VAR>F : J ⥤ C<VAR>E : K ⥤ J<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>H.mapCoconeWhisker.inv.hom = 𝟙 (H.obj 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>c.op.pt = Opposite.op 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>c.op.π = CategoryTheory.NatTrans.op 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>c : CategoryTheory.Limits.Cone F<GOAL>c.op.ι = CategoryTheory.NatTrans.op 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>c : CategoryTheory.Limits.Cone F<GOAL>c.op.pt = Opposite.op 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.op<GOAL>c.unop.π = CategoryTheory.NatTrans.removeOp 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>c : CategoryTheory.Limits.Cocone F.op<GOAL>c.unop.pt = Opposite.unop 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.op<GOAL>c.unop.pt = Opposite.unop 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.op<GOAL>c.unop.ι = CategoryTheory.NatTrans.removeOp 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>c : CategoryTheory.Limits.Cocone F.leftOp<GOAL>(CategoryTheory.Limits.coneOfCoconeLeftOp c).pt = Opposite.op 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.leftOp<VAR>X : J<GOAL>(CategoryTheory.Limits.coneOfCoconeLeftOp c).π.app X = (c.ι.app (Opposite.op X)).op
<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 : Jᵒᵖ<GOAL>(CategoryTheory.Limits.coconeLeftOpOfCone c).ι.app X = (c.π.app (Opposite.unop X)).unop
<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.coconeLeftOpOfCone c).pt = Opposite.unop 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.leftOp<GOAL>(CategoryTheory.Limits.coconeOfConeLeftOp c).pt = Opposite.op 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.leftOp<VAR>j : J<GOAL>(CategoryTheory.Limits.coconeOfConeLeftOp c).ι.app j = (c.π.app (Opposite.op j)).op
<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.coneLeftOpOfCocone c).pt = Opposite.unop 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 : Jᵒᵖ<GOAL>(CategoryTheory.Limits.coneLeftOpOfCocone c).π.app X = (c.ι.app (Opposite.unop X)).unop
<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.rightOp<GOAL>(CategoryTheory.Limits.coneOfCoconeRightOp c).pt = Opposite.unop 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.rightOp<GOAL>(CategoryTheory.Limits.coneOfCoconeRightOp c).π = CategoryTheory.NatTrans.removeRightOp 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>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.coconeRightOpOfCone c).pt = Opposite.op 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.coconeRightOpOfCone c).ι = CategoryTheory.NatTrans.rightOp 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>c : CategoryTheory.Limits.Cone F.rightOp<GOAL>(CategoryTheory.Limits.coconeOfConeRightOp c).ι = CategoryTheory.NatTrans.removeRightOp 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>c : CategoryTheory.Limits.Cone F.rightOp<GOAL>(CategoryTheory.Limits.coconeOfConeRightOp c).pt = Opposite.unop 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.coneRightOpOfCocone c).π = CategoryTheory.NatTrans.rightOp 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>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.coneRightOpOfCocone c).pt = Opposite.op 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.unop<GOAL>(CategoryTheory.Limits.coneOfCoconeUnop c).pt = Opposite.op 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.unop<GOAL>(CategoryTheory.Limits.coneOfCoconeUnop c).π = CategoryTheory.NatTrans.removeUnop 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>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.coconeUnopOfCone c).ι = CategoryTheory.NatTrans.unop 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>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.coconeUnopOfCone c).pt = Opposite.unop 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.unop<GOAL>(CategoryTheory.Limits.coconeOfConeUnop c).ι = CategoryTheory.NatTrans.removeUnop 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>c : CategoryTheory.Limits.Cone F.unop<GOAL>(CategoryTheory.Limits.coconeOfConeUnop c).pt = Opposite.op 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.coneUnopOfCocone c).pt = Opposite.unop 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.coneUnopOfCocone c).π = CategoryTheory.NatTrans.unop c.ι
<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>t : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Functor.mapConeOp G t).hom.hom = 𝟙 (Opposite.op (G.obj 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>t : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Functor.mapConeOp G t).inv.hom = 𝟙 (Opposite.op (G.obj 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>t : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Functor.mapCoconeOp G).hom.hom = 𝟙 (Opposite.op (G.obj 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>t : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Functor.mapCoconeOp G).inv.hom = 𝟙 (Opposite.op (G.obj t.pt))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>e : C ≌ D<VAR>B : C<VAR>α : Type u_3<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>W : D<VAR>ε : (a : α) → e.functor.obj (X a) ⟶ W<VAR>h : ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)), CategoryTheory.CategoryStruct.comp g₁ (e.functor.map (π a₁)) = CategoryTheory.CategoryStruct.comp g₂ (e.functor.map (π a₂)) → CategoryTheory.CategoryStruct.comp g₁ (ε a₁) = CategoryTheory.CategoryStruct.comp g₂ (ε a₂)<VAR>Z : C<VAR>a₁ a₂ : α<VAR>g₁ : Z ⟶ X a₁<VAR>g₂ : Z ⟶ X a₂<VAR>hg : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂)<GOAL>CategoryTheory.CategoryStruct.comp g₁ ((fun a => CategoryTheory.CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₁) = CategoryTheory.CategoryStruct.comp g₂ ((fun a => CategoryTheory.CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.PreservesEffectiveEpis<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.EffectiveEpi f<GOAL>CategoryTheory.EffectiveEpi (F.map f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.PreservesEffectiveEpiFamilies<VAR>α : Type u<VAR>B : C<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>CategoryTheory.EffectiveEpiFamily X π<GOAL>CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.PreservesFiniteEffectiveEpiFamilies<VAR>α : Type<VAR>Finite α<VAR>B : C<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>CategoryTheory.EffectiveEpiFamily X π<GOAL>CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.ReflectsEffectiveEpis<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.EffectiveEpi (F.map f) → CategoryTheory.EffectiveEpi f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.ReflectsEffectiveEpis<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : CategoryTheory.EffectiveEpi (F.map f)<GOAL>CategoryTheory.EffectiveEpi f