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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>X : CategoryTheory.CostructuredArrow S T<GOAL>(CategoryTheory.CategoryStruct.id X).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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.CostructuredArrow S T<VAR>h : X = Y<GOAL>(CategoryTheory.eqToHom h).left = CategoryTheory.eqToHom ⋯
<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 : X ⟶ Y<GOAL>f.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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>f f' : CategoryTheory.CostructuredArrow S T<VAR>g : f.left ⟶ f'.left<VAR>w : CategoryTheory.CategoryStruct.comp (S.map g) f'.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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>f f' : CategoryTheory.CostructuredArrow S T<VAR>g : f.left ⟶ f'.left<VAR>w : CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom := by aesop_cat<GOAL>(CategoryTheory.CostructuredArrow.homMk g w).left = 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>f f' : CategoryTheory.CostructuredArrow S T<VAR>φ : f ⟶ f'<GOAL>∃ ψ, ∃ (hψ : CategoryTheory.CategoryStruct.comp (S.map ψ) f'.hom = f.hom), φ = CategoryTheory.CostructuredArrow.homMk ψ hψ
<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 : CategoryTheory.CostructuredArrow S T<VAR>g : Y' ⟶ f.left<GOAL>(f.homMk' g).left = 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>Y' : C<VAR>S : CategoryTheory.Functor C D<VAR>f : CategoryTheory.CostructuredArrow S T<VAR>g : Y' ⟶ f.left<GOAL>(f.homMk' g).right = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).right
<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>f : CategoryTheory.CostructuredArrow S T<GOAL>f.homMk' (CategoryTheory.CategoryStruct.id f.left) = CategoryTheory.eqToHom ⋯
<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).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>T : D<VAR>Y' Y'' : C<VAR>S : CategoryTheory.Functor C D<VAR>f : CategoryTheory.CostructuredArrow S T<VAR>g : Y' ⟶ f.left<VAR>g' : Y'' ⟶ Y'<GOAL>f.homMk' (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).homMk' g') (f.homMk' 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>Y Y' Y'' : C<VAR>S : CategoryTheory.Functor C D<VAR>f : S.obj Y ⟶ T<VAR>g : Y' ⟶ Y<VAR>g' : Y'' ⟶ Y'<GOAL>(CategoryTheory.CostructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f)).homMk' g') ((CategoryTheory.CostructuredArrow.mk f).homMk' 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>Y Y' : C<VAR>S : CategoryTheory.Functor C D<VAR>f : S.obj Y ⟶ T<VAR>g : Y' ⟶ Y<GOAL>(CategoryTheory.CostructuredArrow.mkPrecomp f g).right = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f)).right
<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 Y' : C<VAR>S : CategoryTheory.Functor C D<VAR>f : S.obj Y ⟶ T<VAR>g : Y' ⟶ Y<GOAL>(CategoryTheory.CostructuredArrow.mkPrecomp f g).left = 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>Y : C<VAR>S : CategoryTheory.Functor C D<VAR>f : S.obj Y ⟶ T<GOAL>CategoryTheory.CostructuredArrow.mkPrecomp 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>T : D<VAR>Y Y' Y'' : C<VAR>S : CategoryTheory.Functor C D<VAR>f : S.obj Y ⟶ T<VAR>g : Y' ⟶ Y<VAR>g' : Y'' ⟶ Y'<GOAL>CategoryTheory.CostructuredArrow.mkPrecomp f (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CostructuredArrow.mkPrecomp (CategoryTheory.CategoryStruct.comp (S.map g) f) g') (CategoryTheory.CostructuredArrow.mkPrecomp 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>f f' : CategoryTheory.CostructuredArrow S T<VAR>g : f.left ≅ f'.left<VAR>w : CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>f f' : CategoryTheory.CostructuredArrow S T<VAR>g : f.left ≅ f'.left<VAR>w : CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat<GOAL>(CategoryTheory.CostructuredArrow.isoMk g w).hom.left = g.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>f f' : CategoryTheory.CostructuredArrow S T<VAR>g : f.left ≅ f'.left<VAR>w : CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom := by aesop_cat<GOAL>(CategoryTheory.CostructuredArrow.isoMk g w).inv.left = g.inv
<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 g : A ⟶ B<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>A B : CategoryTheory.CostructuredArrow S T<VAR>f g : A ⟶ B<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>S : CategoryTheory.Functor C D<VAR>A B : CategoryTheory.CostructuredArrow S T<VAR>f : A ⟶ B<VAR>h : CategoryTheory.Mono f.left<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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>A B : CategoryTheory.CostructuredArrow S T<VAR>f : A ⟶ B<VAR>h : CategoryTheory.Epi f.left<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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>f : CategoryTheory.CostructuredArrow S T<GOAL>f = CategoryTheory.CostructuredArrow.mk f.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>f : CategoryTheory.CostructuredArrow S T<GOAL>f.eta.hom.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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>f : CategoryTheory.CostructuredArrow S T<GOAL>⋯ = ⋯
<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>f : CategoryTheory.CostructuredArrow S T<GOAL>f.eta.inv.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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>f : CategoryTheory.CostructuredArrow S T<GOAL>∃ Y g, f = CategoryTheory.CostructuredArrow.mk g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T T' : D<VAR>S : CategoryTheory.Functor C D<VAR>f : T ⟶ T'<VAR>X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)<GOAL>((CategoryTheory.CostructuredArrow.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>T T' : D<VAR>S : CategoryTheory.Functor C D<VAR>f : T ⟶ T'<VAR>X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)<GOAL>((CategoryTheory.CostructuredArrow.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>T T' : D<VAR>S : CategoryTheory.Functor C D<VAR>f : T ⟶ T'<GOAL>∀ {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f_1 : X ⟶ Y), ((CategoryTheory.CostructuredArrow.map f).map f_1).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>T T' : D<VAR>S : CategoryTheory.Functor C D<VAR>f : T ⟶ T'<GOAL>∀ {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f_1 : X ⟶ Y), ((CategoryTheory.CostructuredArrow.map f).map f_1).left = f_1.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T T' : D<VAR>S : CategoryTheory.Functor C D<VAR>f : T ⟶ T'<VAR>X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)<GOAL>((CategoryTheory.CostructuredArrow.map f).obj X).hom = CategoryTheory.CategoryStruct.comp X.hom f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T T' : D<VAR>Y : C<VAR>S : CategoryTheory.Functor C D<VAR>f : S.obj Y ⟶ T<VAR>g : T ⟶ T'<GOAL>(CategoryTheory.CostructuredArrow.map g).obj (CategoryTheory.CostructuredArrow.mk f) = CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp 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>f : CategoryTheory.CostructuredArrow S T<GOAL>(CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.id T)).obj f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>S : CategoryTheory.Functor C D<VAR>f : T ⟶ T'<VAR>f' : T' ⟶ T''<VAR>h : CategoryTheory.CostructuredArrow S T<GOAL>(CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.comp f f')).obj h = (CategoryTheory.CostructuredArrow.map f').obj ((CategoryTheory.CostructuredArrow.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>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>S : D<GOAL>∀ {X Y : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)} (f : X ⟶ Y), ((CategoryTheory.CostructuredArrow.pre F G S).map f).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>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>S : D<VAR>X : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)<GOAL>((CategoryTheory.CostructuredArrow.pre F G S).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>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>S : D<VAR>X : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)<GOAL>((CategoryTheory.CostructuredArrow.pre F G S).obj X).left = F.obj 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>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>S : D<GOAL>∀ {X Y : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)} (f : X ⟶ Y), ((CategoryTheory.CostructuredArrow.pre F G S).map f).left = F.map f.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>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>S : D<VAR>X : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)<GOAL>((CategoryTheory.CostructuredArrow.pre F G S).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>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>S : C<VAR>X : CategoryTheory.CostructuredArrow F S<GOAL>(CategoryTheory.CostructuredArrow.post F G S).obj X = CategoryTheory.CostructuredArrow.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>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>S : C<GOAL>∀ {X Y : CategoryTheory.CostructuredArrow F S} (f : X ⟶ Y), (CategoryTheory.CostructuredArrow.post F G S).map f = CategoryTheory.CostructuredArrow.homMk 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>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>U : CategoryTheory.Functor A B<VAR>V : B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : F.comp U ⟶ S.comp G<VAR>β : G.obj T ⟶ V<VAR>X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)<GOAL>((CategoryTheory.CostructuredArrow.map₂ α β).obj X).left = F.obj X.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>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>U : CategoryTheory.Functor A B<VAR>V : B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : F.comp U ⟶ S.comp G<VAR>β : G.obj T ⟶ V<VAR>X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)<GOAL>((CategoryTheory.CostructuredArrow.map₂ α β).obj X).hom = CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>U : CategoryTheory.Functor A B<VAR>V : B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : F.comp U ⟶ S.comp G<VAR>β : G.obj T ⟶ V<VAR>X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)<GOAL>((CategoryTheory.CostructuredArrow.map₂ α β).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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>U : CategoryTheory.Functor A B<VAR>V : B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : F.comp U ⟶ S.comp G<VAR>β : G.obj T ⟶ V<VAR>X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.CostructuredArrow.map₂ α β).map φ).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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>U : CategoryTheory.Functor A B<VAR>V : B<VAR>F : CategoryTheory.Functor C A<VAR>G : CategoryTheory.Functor D B<VAR>α : F.comp U ⟶ S.comp G<VAR>β : G.obj T ⟶ V<VAR>X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.CostructuredArrow.map₂ α β).map φ).left = F.map φ.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>f g : CategoryTheory.CostructuredArrow S T<VAR>h : f.IsUniversal<VAR>η : g ⟶ f<GOAL>η = CategoryTheory.Limits.IsTerminal.from h 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>f : CategoryTheory.CostructuredArrow S T<VAR>h : f.IsUniversal<VAR>g : CategoryTheory.CostructuredArrow S T<GOAL>CategoryTheory.CategoryStruct.comp (S.map (h.lift g)) 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>T : D<VAR>S : CategoryTheory.Functor C D<VAR>f : CategoryTheory.CostructuredArrow S T<VAR>h : f.IsUniversal<VAR>c : C<VAR>η : c ⟶ f.left<GOAL>η = h.lift (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map η) f.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>f : CategoryTheory.CostructuredArrow S T<VAR>h : f.IsUniversal<VAR>c : C<VAR>η η' : c ⟶ f.left<VAR>w : CategoryTheory.CategoryStruct.comp (S.map η) f.hom = CategoryTheory.CategoryStruct.comp (S.map η') f.hom<GOAL>η = η'
<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>f : CategoryTheory.CostructuredArrow S T<VAR>h : f.IsUniversal<VAR>g : CategoryTheory.CostructuredArrow S T<GOAL>∃! η, CategoryTheory.CategoryStruct.comp (S.map η) 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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor E C<VAR>X : D<VAR>F : CategoryTheory.Functor C D<VAR>f : (Y : E) → X ⟶ F.obj (G.obj Y)<VAR>h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z<GOAL>∀ {X_1 Y : E} (g : X_1 ⟶ Y), (G.toStructuredArrow X F f h).map g = CategoryTheory.StructuredArrow.homMk (G.map g) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor E C<VAR>X : D<VAR>F : CategoryTheory.Functor C D<VAR>f : (Y : E) → X ⟶ F.obj (G.obj Y)<VAR>h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z<VAR>Y : E<GOAL>(G.toStructuredArrow X F f h).obj Y = CategoryTheory.StructuredArrow.mk (f Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor E C<VAR>X : D<VAR>F : CategoryTheory.Functor C D<VAR>f : (Y : E) → X ⟶ F.obj (G.obj Y)<VAR>h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z<GOAL>(G.toStructuredArrow X F f ⋯).comp (CategoryTheory.StructuredArrow.proj X F) = G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor E C<VAR>F : CategoryTheory.Functor C D<VAR>X : D<VAR>f : (Y : E) → F.obj (G.obj Y) ⟶ X<VAR>h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y<VAR>Y : E<GOAL>(G.toCostructuredArrow F X f h).obj Y = CategoryTheory.CostructuredArrow.mk (f Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor E C<VAR>F : CategoryTheory.Functor C D<VAR>X : D<VAR>f : (Y : E) → F.obj (G.obj Y) ⟶ X<VAR>h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y<GOAL>∀ {X_1 Y : E} (g : X_1 ⟶ Y), (G.toCostructuredArrow F X f h).map g = CategoryTheory.CostructuredArrow.homMk (G.map g) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor E C<VAR>F : CategoryTheory.Functor C D<VAR>X : D<VAR>f : (Y : E) → F.obj (G.obj Y) ⟶ X<VAR>h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y<GOAL>(G.toCostructuredArrow F X f ⋯).comp (CategoryTheory.CostructuredArrow.proj F X) = 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>d : D<VAR>X : (CategoryTheory.StructuredArrow d F)ᵒᵖ<GOAL>(CategoryTheory.StructuredArrow.toCostructuredArrow F d).obj X = CategoryTheory.CostructuredArrow.mk (Opposite.unop X).hom.op
<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>d : D<GOAL>∀ {X Y : (CategoryTheory.StructuredArrow d F)ᵒᵖ} (f : X ⟶ Y), (CategoryTheory.StructuredArrow.toCostructuredArrow F d).map f = CategoryTheory.CostructuredArrow.homMk f.unop.right.op ⋯
<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>d : D<GOAL>∀ {X Y : (CategoryTheory.StructuredArrow (Opposite.op d) F.op)ᵒᵖ} (f : X ⟶ Y), (CategoryTheory.StructuredArrow.toCostructuredArrow' F d).map f = CategoryTheory.CostructuredArrow.homMk f.unop.right.unop ⋯
<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>d : D<VAR>X : (CategoryTheory.StructuredArrow (Opposite.op d) F.op)ᵒᵖ<GOAL>(CategoryTheory.StructuredArrow.toCostructuredArrow' F d).obj X = CategoryTheory.CostructuredArrow.mk (Opposite.unop X).hom.unop
<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>d : D<VAR>X : (CategoryTheory.CostructuredArrow F d)ᵒᵖ<GOAL>(CategoryTheory.CostructuredArrow.toStructuredArrow F d).obj X = CategoryTheory.StructuredArrow.mk (Opposite.unop X).hom.op