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>S : D<VAR>T : CategoryTheory.Functor C D<GOAL>∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T} (f : X ⟶ Y), (CategoryTheory.StructuredArrow.proj S T).map f = f.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T<GOAL>(CategoryTheory.StructuredArrow.proj S T).obj X = X.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.StructuredArrow S T<VAR>f g : X ⟶ Y<VAR>h : f.right = g.right<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.StructuredArrow S T<VAR>f g : X ⟶ Y<GOAL>f = g ↔ f.right = g.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ T.obj Y<GOAL>(CategoryTheory.StructuredArrow.mk f).left = { as := PUnit.unit }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ T.obj Y<GOAL>(CategoryTheory.StructuredArrow.mk f).right = Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ T.obj Y<GOAL>(CategoryTheory.StructuredArrow.mk f).hom = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>A B : CategoryTheory.StructuredArrow S T<VAR>f : A ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp A.hom (T.map f.right) = B.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>X Y Z : CategoryTheory.StructuredArrow S T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>X : CategoryTheory.StructuredArrow S T<GOAL>(CategoryTheory.CategoryStruct.id X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.StructuredArrow S T<VAR>h : X = Y<GOAL>(CategoryTheory.eqToHom h).right = CategoryTheory.eqToHom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.StructuredArrow S T<VAR>f : X ⟶ Y<GOAL>f.left = CategoryTheory.CategoryStruct.id X.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f f' : CategoryTheory.StructuredArrow S T<VAR>g : f.right ⟶ f'.right<VAR>w : CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom := by aesop_cat<GOAL>(CategoryTheory.StructuredArrow.homMk g w).left = CategoryTheory.CategoryStruct.id f.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f f' : CategoryTheory.StructuredArrow S T<VAR>g : f.right ⟶ f'.right<VAR>w : CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom := by aesop_cat<GOAL>(CategoryTheory.StructuredArrow.homMk g w).right = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f f' : CategoryTheory.StructuredArrow S T<VAR>φ : f ⟶ f'<GOAL>∃ ψ, ∃ (hψ : CategoryTheory.CategoryStruct.comp f.hom (T.map ψ) = f'.hom), φ = CategoryTheory.StructuredArrow.homMk ψ hψ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y' : C<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<VAR>g : f.right ⟶ Y'<GOAL>(f.homMk' g).right = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y' : C<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<VAR>g : f.right ⟶ Y'<GOAL>(f.homMk' g).left = CategoryTheory.CategoryStruct.id f.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<GOAL>f.homMk' (CategoryTheory.CategoryStruct.id f.right) = CategoryTheory.eqToHom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ T.obj Y<GOAL>(CategoryTheory.StructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y' Y'' : C<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<VAR>g : f.right ⟶ Y'<VAR>g' : Y' ⟶ Y''<GOAL>f.homMk' (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (f.homMk' g) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map g))).homMk' g') (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y Y' Y'' : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ T.obj Y<VAR>g : Y ⟶ Y'<VAR>g' : Y' ⟶ Y''<GOAL>(CategoryTheory.StructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk f).homMk' g) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f (T.map g))).homMk' g') (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y Y' : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ T.obj Y<VAR>g : Y ⟶ Y'<GOAL>(CategoryTheory.StructuredArrow.mkPostcomp f g).left = CategoryTheory.CategoryStruct.id (CategoryTheory.StructuredArrow.mk f).left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y Y' : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ T.obj Y<VAR>g : Y ⟶ Y'<GOAL>(CategoryTheory.StructuredArrow.mkPostcomp f g).right = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ T.obj Y<GOAL>CategoryTheory.StructuredArrow.mkPostcomp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>Y Y' Y'' : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ T.obj Y<VAR>g : Y ⟶ Y'<VAR>g' : Y' ⟶ Y''<GOAL>CategoryTheory.StructuredArrow.mkPostcomp f (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.mkPostcomp f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.mkPostcomp (CategoryTheory.CategoryStruct.comp f (T.map g)) g') (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f f' : CategoryTheory.StructuredArrow S T<VAR>g : f.right ≅ f'.right<VAR>w : CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat<GOAL>⋯ = ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f f' : CategoryTheory.StructuredArrow S T<VAR>g : f.right ≅ f'.right<VAR>w : CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat<GOAL>(CategoryTheory.StructuredArrow.isoMk g w).inv.right = g.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f f' : CategoryTheory.StructuredArrow S T<VAR>g : f.right ≅ f'.right<VAR>w : CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom := by aesop_cat<GOAL>(CategoryTheory.StructuredArrow.isoMk g w).hom.right = g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>A B : CategoryTheory.StructuredArrow S T<VAR>f g : A ⟶ B<GOAL>f.right = g.right → f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>A B : CategoryTheory.StructuredArrow S T<VAR>f g : A ⟶ B<GOAL>f = g ↔ f.right = g.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>A B : CategoryTheory.StructuredArrow S T<VAR>f : A ⟶ B<VAR>h : CategoryTheory.Mono f.right<GOAL>CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>A B : CategoryTheory.StructuredArrow S T<VAR>f : A ⟶ B<VAR>h : CategoryTheory.Epi f.right<GOAL>CategoryTheory.Epi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<GOAL>f = CategoryTheory.StructuredArrow.mk f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<GOAL>f.eta.hom.right = CategoryTheory.CategoryStruct.id f.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<GOAL>⋯ = ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<GOAL>f.eta.inv.right = CategoryTheory.CategoryStruct.id f.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<GOAL>∃ Y g, f = CategoryTheory.StructuredArrow.mk g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S S' : D<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ S'<GOAL>∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f_1 : X ⟶ Y), ((CategoryTheory.StructuredArrow.map f).map f_1).right = f_1.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S S' : D<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ S'<GOAL>∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f_1 : X ⟶ Y), ((CategoryTheory.StructuredArrow.map f).map f_1).left = CategoryTheory.CategoryStruct.id X.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S S' : D<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ S'<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T<GOAL>((CategoryTheory.StructuredArrow.map f).obj X).hom = CategoryTheory.CategoryStruct.comp f X.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S S' : D<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ S'<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T<GOAL>((CategoryTheory.StructuredArrow.map f).obj X).left = X.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S S' : D<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ S'<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T<GOAL>((CategoryTheory.StructuredArrow.map f).obj X).right = X.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S S' : D<VAR>Y : C<VAR>T : CategoryTheory.Functor C D<VAR>f : S' ⟶ T.obj Y<VAR>g : S ⟶ S'<GOAL>(CategoryTheory.StructuredArrow.map g).obj (CategoryTheory.StructuredArrow.mk f) = CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp g f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<GOAL>(CategoryTheory.StructuredArrow.map (CategoryTheory.CategoryStruct.id S)).obj f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>T : CategoryTheory.Functor C D<VAR>f : S ⟶ S'<VAR>f' : S' ⟶ S''<VAR>h : CategoryTheory.StructuredArrow S'' T<GOAL>(CategoryTheory.StructuredArrow.map (CategoryTheory.CategoryStruct.comp f f')).obj h = (CategoryTheory.StructuredArrow.map f).obj ((CategoryTheory.StructuredArrow.map f').obj h)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>S : D<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)<GOAL>((CategoryTheory.StructuredArrow.pre S F G).obj X).hom = X.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>S : D<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)<GOAL>((CategoryTheory.StructuredArrow.pre S F G).obj X).right = F.obj X.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>S : D<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)<GOAL>((CategoryTheory.StructuredArrow.pre S F G).obj X).left = X.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>S : D<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<GOAL>∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)} (f : X ⟶ Y), ((CategoryTheory.StructuredArrow.pre S F G).map f).right = F.map f.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>S : D<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<GOAL>∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)} (f : X ⟶ Y), ((CategoryTheory.StructuredArrow.pre S F G).map f).left = CategoryTheory.CategoryStruct.id X.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>S : C<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<GOAL>∀ {X Y : CategoryTheory.StructuredArrow S F} (f : X ⟶ Y), (CategoryTheory.StructuredArrow.post S F G).map f = CategoryTheory.StructuredArrow.homMk f.right ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>S : C<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>X : CategoryTheory.StructuredArrow S F<GOAL>(CategoryTheory.StructuredArrow.post S F G).obj X = CategoryTheory.StructuredArrow.mk (G.map X.hom)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>L : D<VAR>R : CategoryTheory.Functor C D<VAR>L' : B<VAR>R' : CategoryTheory.Functor A B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : L' ⟶ G.obj L<VAR>β : R.comp G ⟶ F.comp R'<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R<GOAL>((CategoryTheory.StructuredArrow.map₂ α β).obj X).left = X.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>L : D<VAR>R : CategoryTheory.Functor C D<VAR>L' : B<VAR>R' : CategoryTheory.Functor A B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : L' ⟶ G.obj L<VAR>β : R.comp G ⟶ F.comp R'<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R<GOAL>((CategoryTheory.StructuredArrow.map₂ α β).obj X).right = F.obj X.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>L : D<VAR>R : CategoryTheory.Functor C D<VAR>L' : B<VAR>R' : CategoryTheory.Functor A B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : L' ⟶ G.obj L<VAR>β : R.comp G ⟶ F.comp R'<VAR>X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.StructuredArrow.map₂ α β).map φ).right = F.map φ.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>L : D<VAR>R : CategoryTheory.Functor C D<VAR>L' : B<VAR>R' : CategoryTheory.Functor A B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : L' ⟶ G.obj L<VAR>β : R.comp G ⟶ F.comp R'<VAR>X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.StructuredArrow.map₂ α β).map φ).left = CategoryTheory.CategoryStruct.id X.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>L : D<VAR>R : CategoryTheory.Functor C D<VAR>L' : B<VAR>R' : CategoryTheory.Functor A B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : L' ⟶ G.obj L<VAR>β : R.comp G ⟶ F.comp R'<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R<GOAL>((CategoryTheory.StructuredArrow.map₂ α β).obj X).hom = CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (G.map X.hom) (β.app X.right))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f g : CategoryTheory.StructuredArrow S T<VAR>h : f.IsUniversal<VAR>η : f ⟶ g<GOAL>η = CategoryTheory.Limits.IsInitial.to h g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<VAR>h : f.IsUniversal<VAR>g : CategoryTheory.StructuredArrow S T<GOAL>CategoryTheory.CategoryStruct.comp f.hom (T.map (h.desc g)) = g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<VAR>h : f.IsUniversal<VAR>c : C<VAR>η : f.right ⟶ c<GOAL>η = h.desc (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map η)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<VAR>h : f.IsUniversal<VAR>c : C<VAR>η η' : f.right ⟶ c<VAR>w : CategoryTheory.CategoryStruct.comp f.hom (T.map η) = CategoryTheory.CategoryStruct.comp f.hom (T.map η')<GOAL>η = η'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>f : CategoryTheory.StructuredArrow S T<VAR>h : f.IsUniversal<VAR>g : CategoryTheory.StructuredArrow S T<GOAL>∃! η, CategoryTheory.CategoryStruct.comp f.hom (T.map η) = g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : CategoryTheory.Functor C D<VAR>T : D<VAR>X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)<GOAL>(CategoryTheory.CostructuredArrow.proj S T).obj X = X.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : CategoryTheory.Functor C D<VAR>T : D<GOAL>∀ {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f : X ⟶ Y), (CategoryTheory.CostructuredArrow.proj S T).map f = f.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T : D<VAR>S : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.CostructuredArrow S T<VAR>f g : X ⟶ Y<VAR>h : f.left = g.left<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T : D<VAR>S : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.CostructuredArrow S T<VAR>f g : X ⟶ Y<GOAL>f = g ↔ f.left = g.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T : D<VAR>Y : C<VAR>S : CategoryTheory.Functor C D<VAR>f : S.obj Y ⟶ T<GOAL>(CategoryTheory.CostructuredArrow.mk f).left = Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T : D<VAR>Y : C<VAR>S : CategoryTheory.Functor C D<VAR>f : S.obj Y ⟶ T<GOAL>(CategoryTheory.CostructuredArrow.mk f).right = { as := PUnit.unit }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T : D<VAR>Y : C<VAR>S : CategoryTheory.Functor C D<VAR>f : S.obj Y ⟶ T<GOAL>(CategoryTheory.CostructuredArrow.mk f).hom = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T : D<VAR>S : CategoryTheory.Functor C D<VAR>A B : CategoryTheory.CostructuredArrow S T<VAR>f : A ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp (S.map f.left) B.hom = A.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T : D<VAR>S : CategoryTheory.Functor C D<VAR>X Y Z : CategoryTheory.CostructuredArrow S T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left