ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>E : CategoryTheory.Functor C D<VAR>E.IsEquivalence<VAR>CategoryTheory.Limits.HasColimitsOfShape J D<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : CategoryTheory.Functor C D<VAR>E.IsEquivalence<VAR>CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D<GOAL>CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : CategoryTheory.Functor J D<VAR>c : CategoryTheory.Limits.Cone (K.comp G)<GOAL>((adj.functorialityUnit' K).app c).hom = adj.unit.app c.pt
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : CategoryTheory.Functor J D<VAR>c : CategoryTheory.Limits.Cone K<GOAL>((adj.functorialityCounit' K).app c).hom = adj.counit.app c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : CategoryTheory.Functor J D<VAR>E : CategoryTheory.Functor D C<VAR>E.IsEquivalence<VAR>CategoryTheory.Limits.HasLimit K<GOAL>CategoryTheory.Limits.HasLimit (K.comp E)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : CategoryTheory.Functor J D<VAR>E : CategoryTheory.Functor D C<VAR>E.IsEquivalence<VAR>CategoryTheory.Limits.HasLimit (K.comp E)<GOAL>CategoryTheory.Limits.HasLimit K
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>E : CategoryTheory.Functor D C<VAR>E.IsEquivalence<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<GOAL>CategoryTheory.Limits.HasLimitsOfShape J D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : CategoryTheory.Functor D C<VAR>E.IsEquivalence<VAR>CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X Y : C<GOAL>CategoryTheory.IsIsomorphic X Y ↔ Nonempty (X ⟶ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Abelian C<GOAL>CategoryTheory.Limits.HasKernels C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Abelian C<GOAL>CategoryTheory.Limits.HasCokernels C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Abelian C<GOAL>CategoryTheory.Limits.HasFiniteProducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e = CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π f) f ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).m = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).I = CategoryTheory.Abelian.image f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e = CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f) ≫ CategoryTheory.Abelian.coimageImageComparison f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)<GOAL>CategoryTheory.Limits.HasImages C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<GOAL>CategoryTheory.Limits.HasFiniteBiproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : CategoryTheory.Limits.kernel.ι f = 0<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : CategoryTheory.Limits.cokernel.π f = 0<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>R : C<VAR>g : Q ⟶ R<VAR>h : f ≫ g = 0<GOAL>CategoryTheory.Abelian.image.ι f ≫ g = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>R : C<VAR>g : Q ⟶ R<VAR>h : f ≫ g = 0<GOAL>f ≫ CategoryTheory.Abelian.coimage.π g = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>(CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).I = CategoryTheory.Abelian.image f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>(CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).e = CategoryTheory.Abelian.factorThruImage f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>(CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).m = CategoryTheory.Abelian.image.ι f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>(CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).m = CategoryTheory.Abelian.factorThruCoimage f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>(CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).I = CategoryTheory.Abelian.coimage f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>(CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).e = CategoryTheory.Abelian.coimage.π f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Abelian.coimageIsoImage' f).hom = CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.Limits.factorThruImage f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.factorThruImage f ≫ (CategoryTheory.Abelian.coimageIsoImage' f).inv = CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Abelian.imageIsoImage f).hom ≫ CategoryTheory.Limits.image.ι f = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Abelian.imageIsoImage f).inv = CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.Limits.image.ι f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>T : C<VAR>g : X ⟶ T<VAR>hg : CategoryTheory.Limits.kernel.ι f ≫ g = 0<GOAL>f ≫ CategoryTheory.Abelian.epiDesc f g hg = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>T : C<VAR>g : T ⟶ Y<VAR>hg : g ≫ CategoryTheory.Limits.cokernel.π f = 0<GOAL>CategoryTheory.Abelian.monoLift f g hg ≫ f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Epi f<VAR>s : CategoryTheory.Limits.PullbackCone f g<VAR>hs : CategoryTheory.Limits.IsLimit s<GOAL>CategoryTheory.Epi s.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Epi g<VAR>s : CategoryTheory.Limits.PullbackCone f g<VAR>hs : CategoryTheory.Limits.IsLimit s<GOAL>CategoryTheory.Epi s.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>g₁ : Y ⟶ W<VAR>CategoryTheory.Epi g₁<VAR>g₂ : W ⟶ Z<VAR>CategoryTheory.Mono g₂<VAR>hg : g₁ ≫ g₂ = g<VAR>f' : X ⟶ W<VAR>hf : f' ≫ g₂ = f<VAR>t : CategoryTheory.Limits.PullbackCone f g<VAR>ht : CategoryTheory.Limits.IsLimit t<GOAL>CategoryTheory.Epi t.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Mono f<VAR>s : CategoryTheory.Limits.PushoutCocone f g<VAR>hs : CategoryTheory.Limits.IsColimit s<GOAL>CategoryTheory.Mono s.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Mono g<VAR>s : CategoryTheory.Limits.PushoutCocone f g<VAR>hs : CategoryTheory.Limits.IsColimit s<GOAL>CategoryTheory.Mono s.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>g₁ : X ⟶ W<VAR>CategoryTheory.Epi g₁<VAR>g₂ : W ⟶ Z<VAR>CategoryTheory.Mono g₂<VAR>hg : g₁ ≫ g₂ = g<VAR>f' : W ⟶ Y<VAR>hf : g₁ ≫ f' = f<VAR>t : CategoryTheory.Limits.PushoutCocone f g<VAR>ht : CategoryTheory.Limits.IsColimit t<GOAL>CategoryTheory.Mono t.inl
<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>G : CategoryTheory.Functor D C<VAR>self : F ⊣ G<VAR>X : C<VAR>Y : D<VAR>g : X ⟶ G.obj Y<GOAL>(self.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (self.counit.app Y)
<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>G : CategoryTheory.Functor D C<VAR>self : F ⊣ G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<GOAL>(self.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (self.unit.app X) (G.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>left : CategoryTheory.Functor C D<VAR>self : left.IsLeftAdjoint<GOAL>∃ right, Nonempty (left ⊣ right)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>right : CategoryTheory.Functor D C<VAR>self : right.IsRightAdjoint<GOAL>∃ left, Nonempty (left ⊣ right)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<GOAL>F.IsLeftAdjoint
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<GOAL>G.IsRightAdjoint
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X : C<GOAL>(adj.homEquiv X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X)) = adj.unit.app X
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X : D<GOAL>(adj.homEquiv (G.obj X) X).symm (CategoryTheory.CategoryStruct.id (G.obj X)) = adj.counit.app X
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y<GOAL>(adj.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y).symm g)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y<GOAL>(adj.homEquiv X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X : C<VAR>Y Y' : D<VAR>f : F.obj X ⟶ Y<VAR>g : Y ⟶ Y'<GOAL>(adj.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y) f) (G.map g)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X : C<VAR>Y Y' : D<VAR>f : X ⟶ G.obj Y<VAR>g : Y ⟶ Y'<GOAL>(adj.homEquiv X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y'<VAR>h : F.obj X' ⟶ Y<VAR>k : Y ⟶ Y'<VAR>w : CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h k<GOAL>CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y') g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y) h) (G.map k)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y'<VAR>h : X' ⟶ G.obj Y<VAR>k : Y ⟶ Y'<VAR>w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h (G.map k)<GOAL>CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y').symm g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y).symm h) k
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y'<VAR>h : F.obj X' ⟶ Y<VAR>k : Y ⟶ Y'<GOAL>CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y') g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y) h) (G.map k) ↔ CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h k
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y'<VAR>h : X' ⟶ G.obj Y<VAR>k : Y ⟶ Y'<GOAL>CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y').symm g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y).symm h) k ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h (G.map k)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight adj.unit F) (CategoryTheory.whiskerLeft F adj.counit) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).comp F)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G adj.unit) (CategoryTheory.whiskerRight adj.counit G) = CategoryTheory.CategoryStruct.id (G.comp (CategoryTheory.Functor.id C))
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (F.map (adj.unit.app X)) (adj.counit.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>Y : D<GOAL>CategoryTheory.CategoryStruct.comp (adj.unit.app (G.obj Y)) (G.map (adj.counit.app Y)) = CategoryTheory.CategoryStruct.id (G.obj Y)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (F.map (G.map f)) (adj.counit.app Y) = CategoryTheory.CategoryStruct.comp (adj.counit.app X) f
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map (F.map f)) = CategoryTheory.CategoryStruct.comp f (adj.unit.app Y)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>A : C<VAR>B : D<VAR>f : F.obj A ⟶ B<VAR>g : A ⟶ G.obj B<GOAL>(adj.homEquiv A B) f = g ↔ f = (adj.homEquiv A B).symm g
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>A : C<VAR>B : D<VAR>f : F.obj A ⟶ B<VAR>g : A ⟶ G.obj B<GOAL>g = (adj.homEquiv A B) f ↔ (adj.homEquiv A B).symm g = f
<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>G : CategoryTheory.Functor D C<VAR>self : CategoryTheory.Adjunction.CoreHomEquiv F G<VAR>X : C<VAR>Y Y' : D<VAR>f : F.obj X ⟶ Y<VAR>g : Y ⟶ Y'<GOAL>(self.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((self.homEquiv X Y) f) (G.map g)
<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>G : CategoryTheory.Functor D C<VAR>self : CategoryTheory.Adjunction.CoreHomEquiv F G<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y<GOAL>(self.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) ((self.homEquiv X Y).symm g)
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreHomEquiv F G<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' (F.obj X)) (F.map f)) (G.map g) = CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreHomEquiv F G<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y<GOAL>(adj.homEquiv X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreHomEquiv F G<VAR>X : C<VAR>Y Y' : D<VAR>f : X ⟶ G.obj Y<VAR>g : Y ⟶ Y'<GOAL>CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv (G.obj Y) Y').symm (G.map g)) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreHomEquiv F G<VAR>X : C<VAR>Y Y' : D<VAR>f : X ⟶ G.obj Y<VAR>g : Y ⟶ Y'<GOAL>(adj.homEquiv X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g
<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>G : CategoryTheory.Functor D C<VAR>self : CategoryTheory.Adjunction.CoreUnitCounit F G<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight self.unit F) (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (CategoryTheory.whiskerLeft F self.counit)) = CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F)
<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>G : CategoryTheory.Functor D C<VAR>self : CategoryTheory.Adjunction.CoreUnitCounit F G<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G self.unit) (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.whiskerRight self.counit G)) = CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C))
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreHomEquiv F G<VAR>Y : D<GOAL>(CategoryTheory.Adjunction.mkOfHomEquiv adj).counit.app Y = (adj.homEquiv (G.obj Y) ((CategoryTheory.Functor.id D).obj Y)).invFun (CategoryTheory.CategoryStruct.id (G.obj Y))
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreHomEquiv F G<VAR>X : C<GOAL>(CategoryTheory.Adjunction.mkOfHomEquiv adj).unit.app X = (adj.homEquiv X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X))
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreHomEquiv F G<VAR>X : C<VAR>Y : D<GOAL>(CategoryTheory.Adjunction.mkOfHomEquiv adj).homEquiv X Y = adj.homEquiv X Y