ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : CategoryTheory.InjectiveResolution X<VAR>Q : CategoryTheory.InjectiveResolution Y<VAR>φ : P.cocomplex ⟶ Q.cocomplex<VAR>comm : CategoryTheory.CategoryStruct.comp (P.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (Q.ι.f 0)<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.CategoryStruct.comp (F.map f) (Q.toRightDerivedZero' F) = CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F) (HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>X : C<VAR>I : CategoryTheory.InjectiveResolution X<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>F.toRightDerivedZero.app X = CategoryTheory.CategoryStruct.comp (I.toRightDerivedZero' F) (CategoryTheory.CategoryStruct.comp (CochainComplex.isoHomologyπ₀ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)).hom (I.isoRightDerivedObj F 0).inv)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<GOAL>F.rightDerivedZeroIsoSelf.inv = F.toRightDerivedZero
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<GOAL>CategoryTheory.CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom F.toRightDerivedZero = CategoryTheory.CategoryStruct.id (F.rightDerived 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<GOAL>CategoryTheory.CategoryStruct.comp F.toRightDerivedZero F.rightDerivedZeroIsoSelf.hom = CategoryTheory.CategoryStruct.id F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) (F.toRightDerivedZero.app X) = CategoryTheory.CategoryStruct.id ((F.rightDerived 0).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (F.toRightDerivedZero.app X) (F.rightDerivedZeroIsoSelf.hom.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : F' ⟶ F<VAR>X : D<GOAL>((adj1.natTransEquiv adj2).symm f).app X = adj2.unit.app (G.obj X) ≫ G'.map (f.app (G.obj X) ≫ adj1.counit.app X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : G ⟶ G'<VAR>X : C<GOAL>((adj1.natTransEquiv adj2) f).app X = F'.map ((adj1.unit ≫ CategoryTheory.whiskerLeft F f).app X) ≫ adj2.counit.app (F.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<GOAL>(adj.natTransEquiv adj) (𝟙 G) = 𝟙 F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<GOAL>(adj.natTransEquiv adj).symm (𝟙 F) = 𝟙 G
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>adj3 : F'' ⊣ G''<VAR>f : G ⟶ G'<VAR>g : G' ⟶ G''<GOAL>(adj2.natTransEquiv adj3) g ≫ (adj1.natTransEquiv adj2) f = (adj1.natTransEquiv adj3) (f ≫ g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>adj3 : F'' ⊣ G''<VAR>f : F' ⟶ F<VAR>g : F'' ⟶ F'<GOAL>(adj1.natTransEquiv adj2).symm f ≫ (adj2.natTransEquiv adj3).symm g = (adj1.natTransEquiv adj3).symm (g ≫ f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>i : F' ≅ F<GOAL>((adj1.natIsoEquiv adj2).symm i).inv = (adj2.natTransEquiv adj1).symm i.inv
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>i : G ≅ G'<GOAL>((adj1.natIsoEquiv adj2) i).inv = (adj2.natTransEquiv adj1) i.inv
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>i : F' ≅ F<GOAL>((adj1.natIsoEquiv adj2).symm i).hom = (adj1.natTransEquiv adj2).symm i.hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>i : G ≅ G'<GOAL>((adj1.natIsoEquiv adj2) i).hom = (adj1.natTransEquiv adj2) i.hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : C<GOAL>(adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<GOAL>adj1.unit ≫ CategoryTheory.whiskerRight (adj1.leftAdjointUniq adj2).hom G = adj2.unit
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : C<GOAL>adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<GOAL>CategoryTheory.whiskerLeft G (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit = adj1.counit
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : D<GOAL>(adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : C<GOAL>(adj1.leftAdjointUniq adj2).inv.app x = (adj2.leftAdjointUniq adj1).hom.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>adj3 : F'' ⊣ G<GOAL>(adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom = (adj1.leftAdjointUniq adj3).hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>adj3 : F'' ⊣ G<VAR>x : C<GOAL>(adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x = (adj1.leftAdjointUniq adj3).hom.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<GOAL>(adj1.leftAdjointUniq adj1).hom = 𝟙 F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>x : D<GOAL>(adj2.homEquiv (G.obj x) x).symm ((adj1.rightAdjointUniq adj2).hom.app x) = adj1.counit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>x : C<GOAL>adj1.unit.app x ≫ (adj1.rightAdjointUniq adj2).hom.app (F.obj x) = adj2.unit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<GOAL>adj1.unit ≫ CategoryTheory.whiskerLeft F (adj1.rightAdjointUniq adj2).hom = adj2.unit
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>x : D<GOAL>F.map ((adj1.rightAdjointUniq adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<GOAL>CategoryTheory.whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit = adj1.counit
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>x : D<GOAL>(adj1.rightAdjointUniq adj2).inv.app x = (adj2.rightAdjointUniq adj1).hom.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>adj3 : F ⊣ G''<GOAL>(adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom = (adj1.rightAdjointUniq adj3).hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>adj3 : F ⊣ G''<VAR>x : D<GOAL>(adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x = (adj1.rightAdjointUniq adj3).hom.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<GOAL>(adj1.rightAdjointUniq adj1).hom = 𝟙 G
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<VAR>j : J<GOAL>c.toStructuredArrow.obj j = CategoryTheory.StructuredArrow.mk (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 : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>∀ {X Y : J} (f : X ⟶ Y), c.toStructuredArrow.map f = CategoryTheory.StructuredArrow.homMk f ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.HasLimit F<GOAL>∀ {X Y : J} (f : X ⟶ Y), (CategoryTheory.Limits.limit.toStructuredArrow F).map f = CategoryTheory.StructuredArrow.homMk f ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.HasLimit F<VAR>j : J<GOAL>(CategoryTheory.Limits.limit.toStructuredArrow F).obj j = CategoryTheory.StructuredArrow.mk (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 : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<VAR>X : J<GOAL>c.toStructuredArrowCompProj.inv.app X = CategoryTheory.CategoryStruct.id X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<VAR>X : J<GOAL>c.toStructuredArrowCompProj.hom.app X = CategoryTheory.CategoryStruct.id X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>c.toStructuredArrow.comp (CategoryTheory.StructuredArrow.proj c.pt F) = CategoryTheory.Functor.id J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<VAR>X : J<GOAL>c.toStructuredArrowCompToUnderCompForget.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<VAR>X : J<GOAL>c.toStructuredArrowCompToUnderCompForget.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>c.toStructuredArrow.comp ((CategoryTheory.StructuredArrow.toUnder c.pt F).comp (CategoryTheory.Under.forget c.pt)) = F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<VAR>j : J<GOAL>c.toUnder.π.app j = CategoryTheory.Under.homMk (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 : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>c.toUnder.pt = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id c.pt)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>c.mapConeToUnder.hom.hom = CategoryTheory.CategoryStruct.id c.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>c.mapConeToUnder.inv.hom = CategoryTheory.CategoryStruct.id 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 : CategoryTheory.Functor C D<VAR>X : D<VAR>G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)<GOAL>(CategoryTheory.Limits.Cone.fromStructuredArrow F G).pt = X
<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 : CategoryTheory.Functor C D<VAR>X : D<VAR>G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)<VAR>j : J<GOAL>(CategoryTheory.Limits.Cone.fromStructuredArrow F G).π.app j = (G.obj j).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>K : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone K<VAR>F : CategoryTheory.Functor C D<VAR>X : D<VAR>f : X ⟶ F.obj c.pt<GOAL>(c.toStructuredArrowCone F f).pt = CategoryTheory.StructuredArrow.mk f
<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>K : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone K<VAR>F : CategoryTheory.Functor C D<VAR>X : D<VAR>f : X ⟶ F.obj c.pt<VAR>j : J<GOAL>(c.toStructuredArrowCone F f).π.app j = CategoryTheory.StructuredArrow.homMk (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 : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cone.toCostructuredArrow F).map f = CategoryTheory.CostructuredArrow.homMk f.hom ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.Cone.toCostructuredArrow F).obj c = CategoryTheory.CostructuredArrow.mk c.π
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F<GOAL>((CategoryTheory.Limits.Cone.fromCostructuredArrow F).obj c).π = c.hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cone.fromCostructuredArrow F).map f).hom = f.left
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F<GOAL>((CategoryTheory.Limits.Cone.fromCostructuredArrow F).obj c).pt = c.left
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).inverse.obj c).pt = c.left
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.map f).left = f.hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).inverse.map f).hom = f.left
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.obj c).left = c.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.obj c).hom = c.π
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.map f).right = CategoryTheory.CategoryStruct.id { as := PUnit.unit }
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.obj c).right.as = PUnit.unit
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).inverse.obj c).π = c.hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cone.equivCostructuredArrow F).unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>CategoryTheory.Limits.HasLimit F ↔ CategoryTheory.Limits.HasTerminal (CategoryTheory.Limits.Cone F)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>CategoryTheory.Limits.HasLimitsOfShape J C ↔ (CategoryTheory.Functor.const J).IsLeftAdjoint
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cone F<GOAL>hc.liftConeMorphism s = (c.isLimitEquivIsTerminal hc).from s
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsTerminal c<VAR>s : CategoryTheory.Limits.Cone F<GOAL>hc.from s = (c.isLimitEquivIsTerminal.symm hc).liftConeMorphism s
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>j : J<GOAL>c.toCostructuredArrow.obj j = CategoryTheory.CostructuredArrow.mk (c.ι.app j)