ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A<VAR>x : F.obj (Opposite.op s)<GOAL>CategoryTheory.OverPresheafAux.YonedaCollection.snd (CategoryTheory.OverPresheafAux.counitForward F s x).val = F.map (CategoryTheory.eqToHom ⋯) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>η : F ⟶ G<VAR>s : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ<VAR>x : F.obj s<GOAL>CategoryTheory.OverPresheafAux.counitForward G (Opposite.unop s) (η.app s x) = (CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop s) x).map₁ (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>s t : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ<VAR>f : t ⟶ s<VAR>x : F.obj t<GOAL>CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop s) (F.map f x) = (CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop t) x).map₂ f.unop.left ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A<GOAL>CategoryTheory.OverPresheafAux.counitForward F s ∘ CategoryTheory.OverPresheafAux.counitBackward F s = id
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A<GOAL>CategoryTheory.OverPresheafAux.counitBackward F s ∘ CategoryTheory.OverPresheafAux.counitForward F s = id
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A<GOAL>∀ (a : F.obj (Opposite.op s)), (CategoryTheory.OverPresheafAux.counitAuxAux F s).hom a = CategoryTheory.OverPresheafAux.counitForward F s a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A<GOAL>∀ (a : CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s.hom), (CategoryTheory.OverPresheafAux.counitAuxAux F s).inv a = CategoryTheory.OverPresheafAux.counitBackward F s a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<GOAL>(CategoryTheory.OverPresheafAux.counitAux F).hom = { app := fun X => (CategoryTheory.OverPresheafAux.counitAuxAux F (Opposite.unop X)).hom, naturality := ⋯ }
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor D C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : G.obj A ⟶ X<VAR>v : G.obj B ⟶ Y<VAR>sq : CategoryTheory.CommSq u (G.map i) p v<VAR>adj : G ⊣ F<GOAL>CategoryTheory.CommSq ((adj.homEquiv A X) u) i (F.map p) ((adj.homEquiv B Y) v)
<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>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor D C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : G.obj A ⟶ X<VAR>v : G.obj B ⟶ Y<VAR>sq : CategoryTheory.CommSq u (G.map i) p v<VAR>adj : G ⊣ F<GOAL>⋯.HasLift ↔ sq.HasLift
<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>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor D C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : A ⟶ F.obj X<VAR>v : B ⟶ F.obj Y<VAR>sq : CategoryTheory.CommSq u i (F.map p) v<VAR>adj : G ⊣ F<GOAL>CategoryTheory.CommSq ((adj.homEquiv A X).symm u) (G.map i) p ((adj.homEquiv B Y).symm v)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor D C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : A ⟶ F.obj X<VAR>v : B ⟶ F.obj Y<VAR>sq : CategoryTheory.CommSq u i (F.map p) v<VAR>adj : G ⊣ F<GOAL>⋯.HasLift ↔ sq.HasLift
<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>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor D C<VAR>adj : G ⊣ F<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<GOAL>CategoryTheory.HasLiftingProperty (G.map i) p ↔ CategoryTheory.HasLiftingProperty i (F.map p)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y Z : C × D} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).1 = CategoryTheory.CategoryStruct.comp f.1 g.1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.CategoryStruct.id X).2 = CategoryTheory.CategoryStruct.id X.2
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X Y : C × D<GOAL>(X ⟶ Y) = ((X.1 ⟶ Y.1) × (X.2 ⟶ Y.2))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y Z : C × D} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).2 = CategoryTheory.CategoryStruct.comp f.2 g.2
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.CategoryStruct.id X).1 = CategoryTheory.CategoryStruct.id X.1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>Y : D<GOAL>CategoryTheory.CategoryStruct.id (X, Y) = (CategoryTheory.CategoryStruct.id X, CategoryTheory.CategoryStruct.id Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P Q R : C<VAR>S T U : D<VAR>f : (P, S) ⟶ (Q, T)<VAR>g : (Q, T) ⟶ (R, U)<GOAL>CategoryTheory.CategoryStruct.comp f g = (CategoryTheory.CategoryStruct.comp f.1 g.1, CategoryTheory.CategoryStruct.comp f.2 g.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P Q : C<VAR>S T : D<VAR>f : (P, S) ⟶ (Q, T)<GOAL>CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.1 ∧ CategoryTheory.IsIso f.2
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.prod.etaIso X).hom = (CategoryTheory.CategoryStruct.id (X.1, X.2).1, CategoryTheory.CategoryStruct.id (X.1, X.2).2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.prod.etaIso X).inv = (CategoryTheory.CategoryStruct.id X.1, CategoryTheory.CategoryStruct.id X.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P Q : C<VAR>S T : D<VAR>f : P ≅ Q<VAR>g : S ≅ T<GOAL>(f.prod g).hom = (f.hom, g.hom)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>P Q : C<VAR>S T : D<VAR>f : P ≅ Q<VAR>g : S ≅ T<GOAL>(f.prod g).inv = (f.inv, g.inv)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>Z : D<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.Prod.sectl C Z).map f = (f, CategoryTheory.CategoryStruct.id Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>Z : D<VAR>X : C<GOAL>(CategoryTheory.Prod.sectl C Z).obj X = (X, Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : D<GOAL>(CategoryTheory.Prod.sectr Z D).obj X = (Z, X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : D} (f : X ⟶ Y), (CategoryTheory.Prod.sectr Z D).map f = (CategoryTheory.CategoryStruct.id Z, f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : C × D} (f : X ⟶ Y), (CategoryTheory.Prod.fst C D).map f = f.1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.Prod.fst C D).obj X = X.1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : C × D} (f : X ⟶ Y), (CategoryTheory.Prod.snd C D).map f = f.2
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.Prod.snd C D).obj X = X.2
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.Prod.swap C D).obj X = (X.2, X.1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : C × D} (f : X ⟶ Y), (CategoryTheory.Prod.swap C D).map f = (f.2, f.1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.Prod.symmetry C D).hom.app X = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.Prod.symmetry C D).inv.app X = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : D × C} (f : X ⟶ Y), (CategoryTheory.Prod.braiding C D).inverse.map f = (f.2, f.1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : D × C<GOAL>(CategoryTheory.Prod.braiding C D).counitIso.hom.app X = (CategoryTheory.CategoryStruct.id X.1, CategoryTheory.CategoryStruct.id X.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.Prod.braiding C D).unitIso.inv.app X = (CategoryTheory.CategoryStruct.id X.1, CategoryTheory.CategoryStruct.id X.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : D × C<GOAL>(CategoryTheory.Prod.braiding C D).inverse.obj X = (X.2, X.1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : D × C<GOAL>(CategoryTheory.Prod.braiding C D).counitIso.inv.app X = (CategoryTheory.CategoryStruct.id X.1, CategoryTheory.CategoryStruct.id X.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.Prod.braiding C D).unitIso.hom.app X = (CategoryTheory.CategoryStruct.id X.1, CategoryTheory.CategoryStruct.id X.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : C × D} (f : X ⟶ Y), (CategoryTheory.Prod.braiding C D).functor.map f = (f.2, f.1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C × D<GOAL>(CategoryTheory.Prod.braiding C D).functor.obj X = (X.2, X.1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Functor C D<GOAL>((CategoryTheory.evaluation C D).map f).app F = F.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<GOAL>∀ {X_1 Y : CategoryTheory.Functor C D} (α : X_1 ⟶ Y), ((CategoryTheory.evaluation C D).obj X).map α = α.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>F : CategoryTheory.Functor C D<GOAL>((CategoryTheory.evaluation C D).obj X).obj F = F.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>x y : C × CategoryTheory.Functor C D<VAR>f : x ⟶ y<GOAL>(CategoryTheory.evaluationUncurried C D).map f = CategoryTheory.CategoryStruct.comp (x.2.map f.1) (f.2.app y.1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>p : C × CategoryTheory.Functor C D<GOAL>(CategoryTheory.evaluationUncurried C D).obj p = p.2.obj p.1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<GOAL>∀ (X_1 : D), (CategoryTheory.Functor.constCompEvaluationObj D X).hom.app X_1 = CategoryTheory.CategoryStruct.id X_1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<GOAL>∀ (X_1 : D), (CategoryTheory.Functor.constCompEvaluationObj D X).inv.app X_1 = CategoryTheory.CategoryStruct.id X_1
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor C D<VAR>X : A × C<GOAL>(F.prod G).obj X = (F.obj X.1, G.obj X.2)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor C D<GOAL>∀ {X Y : A × C} (f : X ⟶ Y), (F.prod G).map f = (F.map f.1, G.map f.2)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor A C<GOAL>∀ {X Y : A} (f : X ⟶ Y), (F.prod' G).map f = (F.map f, G.map f)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor A C<VAR>a : A<GOAL>(F.prod' G).obj a = (F.obj a, G.obj a)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor A C<VAR>X : A<GOAL>(F.prod'CompFst G).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor A C<VAR>X : A<GOAL>(F.prod'CompFst G).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor A C<VAR>X : A<GOAL>(F.prod'CompSnd G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj X)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor A C<VAR>X : A<GOAL>(F.prod'CompSnd G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj X)
<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>X : C<GOAL>(CategoryTheory.Functor.diag C).obj X = (X, X)
<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Functor.diag C).map f = (f, f)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F G : CategoryTheory.Functor A B<VAR>H I : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>β : H ⟶ I<VAR>X : A × C<GOAL>(CategoryTheory.NatTrans.prod α β).app X = (α.app X.1, β.app X.2)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F F' : CategoryTheory.Functor A B<VAR>G G' : CategoryTheory.Functor C D<VAR>e₁ : F ≅ F'<VAR>e₂ : G ≅ G'<GOAL>(CategoryTheory.NatIso.prod e₁ e₂).hom = CategoryTheory.NatTrans.prod e₁.hom e₂.hom
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F F' : CategoryTheory.Functor A B<VAR>G G' : CategoryTheory.Functor C D<VAR>e₁ : F ≅ F'<VAR>e₂ : G ≅ G'<GOAL>(CategoryTheory.NatIso.prod e₁ e₂).inv = CategoryTheory.NatTrans.prod e₁.inv e₂.inv
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>E₁ : A ≌ B<VAR>E₂ : C ≌ D<GOAL>(E₁.prod E₂).functor = E₁.functor.prod E₂.functor
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>E₁ : A ≌ B<VAR>E₂ : C ≌ D<GOAL>(E₁.prod E₂).unitIso = CategoryTheory.NatIso.prod E₁.unitIso E₂.unitIso
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>E₁ : A ≌ B<VAR>E₂ : C ≌ D<GOAL>(E₁.prod E₂).inverse = E₁.inverse.prod E₂.inverse
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>E₁ : A ≌ B<VAR>E₂ : C ≌ D<GOAL>(E₁.prod E₂).counitIso = CategoryTheory.NatIso.prod E₁.counitIso E₂.counitIso
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A (CategoryTheory.Functor B C)<VAR>a : A<VAR>X : B<GOAL>(CategoryTheory.flipCompEvaluation F a).hom.app X = CategoryTheory.CategoryStruct.id ((F.obj a).obj X)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A (CategoryTheory.Functor B C)<VAR>a : A<VAR>X : B<GOAL>(CategoryTheory.flipCompEvaluation F a).inv.app X = CategoryTheory.CategoryStruct.id ((F.obj a).obj X)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>∀ {X Y : CategoryTheory.Functor A B × CategoryTheory.Functor A C} (f : X ⟶ Y) (X_1 : A), ((CategoryTheory.prodFunctorToFunctorProd A B C).map f).app X_1 = (f.1.app X_1, f.2.app X_1)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A B × CategoryTheory.Functor A C<GOAL>(CategoryTheory.prodFunctorToFunctorProd A B C).obj F = F.1.prod' F.2
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>∀ {X Y : CategoryTheory.Functor A (B × C)} (α : X ⟶ Y), (CategoryTheory.functorProdToProdFunctor A B C).map α = ({ app := fun X_1 => (α.app X_1).1, naturality := ⋯ }, { app := fun X_1 => (α.app X_1).2, naturality := ⋯ })
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A (B × C)<GOAL>(CategoryTheory.functorProdToProdFunctor A B C).obj F = (F.comp (CategoryTheory.Prod.fst B C), F.comp (CategoryTheory.Prod.snd B C))
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>X : CategoryTheory.Functor A B × CategoryTheory.Functor A C<GOAL>(CategoryTheory.functorProdFunctorEquivUnitIso A B C).inv.app X = ((X.1.prod'CompFst X.2).hom, (X.1.prod'CompSnd X.2).hom)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>X : CategoryTheory.Functor A B × CategoryTheory.Functor A C<GOAL>(CategoryTheory.functorProdFunctorEquivUnitIso A B C).hom.app X = ((X.1.prod'CompFst X.2).inv, (X.1.prod'CompSnd X.2).inv)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>X : CategoryTheory.Functor A (B × C)<GOAL>∀ (X_1 : A), ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).hom.app X).app X_1 = (CategoryTheory.CategoryStruct.id (X.obj X_1).1, CategoryTheory.CategoryStruct.id (X.obj X_1).2)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>X : CategoryTheory.Functor A (B × C)<GOAL>∀ (X_1 : A), ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).inv.app X).app X_1 = (CategoryTheory.CategoryStruct.id (X.obj X_1).1, CategoryTheory.CategoryStruct.id (X.obj X_1).2)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>(CategoryTheory.functorProdFunctorEquiv A B C).functor = CategoryTheory.prodFunctorToFunctorProd A B C
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>(CategoryTheory.functorProdFunctorEquiv A B C).unitIso = CategoryTheory.functorProdFunctorEquivUnitIso A B C
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>(CategoryTheory.functorProdFunctorEquiv A B C).counitIso = CategoryTheory.functorProdFunctorEquivCounitIso A B C
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>(CategoryTheory.functorProdFunctorEquiv A B C).inverse = CategoryTheory.functorProdToProdFunctor A B C
<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<GOAL>∀ (x : Cᵒᵖ × Dᵒᵖ), (CategoryTheory.prodOpEquiv C).inverse.obj x = match x with | (X, Y) => Opposite.op (Opposite.unop X, Opposite.unop Y)