ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y : CategoryTheory.Limits.WalkingParallelPair<VAR>g : CategoryTheory.Limits.WalkingParallelPairHom X Y<GOAL>(CategoryTheory.Limits.WalkingParallelPairHom.id X).comp g = g
<VAR>X Y : CategoryTheory.Limits.WalkingParallelPair<VAR>f : CategoryTheory.Limits.WalkingParallelPairHom X Y<GOAL>f.comp (CategoryTheory.Limits.WalkingParallelPairHom.id Y) = f
<VAR>X Y Z W : CategoryTheory.Limits.WalkingParallelPair<VAR>f : CategoryTheory.Limits.WalkingParallelPairHom X Y<VAR>g : CategoryTheory.Limits.WalkingParallelPairHom Y Z<VAR>h : CategoryTheory.Limits.WalkingParallelPairHom Z W<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>X : CategoryTheory.Limits.WalkingParallelPair<GOAL>CategoryTheory.Limits.WalkingParallelPairHom.id X = CategoryTheory.CategoryStruct.id X
<VAR>X : CategoryTheory.Limits.WalkingParallelPair<GOAL>sizeOf (CategoryTheory.CategoryStruct.id X) = 1 + sizeOf X
<GOAL>CategoryTheory.Limits.walkingParallelPairOp.obj CategoryTheory.Limits.WalkingParallelPair.zero = Opposite.op CategoryTheory.Limits.WalkingParallelPair.one
<GOAL>CategoryTheory.Limits.walkingParallelPairOp.obj CategoryTheory.Limits.WalkingParallelPair.one = Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero
<GOAL>CategoryTheory.Limits.walkingParallelPairOp.map CategoryTheory.Limits.WalkingParallelPairHom.left = Quiver.Hom.op CategoryTheory.Limits.WalkingParallelPairHom.left
<GOAL>CategoryTheory.Limits.walkingParallelPairOp.map CategoryTheory.Limits.WalkingParallelPairHom.right = Quiver.Hom.op CategoryTheory.Limits.WalkingParallelPairHom.right
<GOAL>CategoryTheory.Limits.walkingParallelPairOpEquiv.functor = CategoryTheory.Limits.walkingParallelPairOp
<GOAL>CategoryTheory.Limits.walkingParallelPairOpEquiv.inverse = CategoryTheory.Limits.walkingParallelPairOp.leftOp
<GOAL>CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.app CategoryTheory.Limits.WalkingParallelPair.zero = CategoryTheory.Iso.refl CategoryTheory.Limits.WalkingParallelPair.zero
<GOAL>CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.Iso.refl CategoryTheory.Limits.WalkingParallelPair.one
<GOAL>CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.app (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero) = CategoryTheory.Iso.refl (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero)
<GOAL>CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.app (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one) = CategoryTheory.Iso.refl (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>(CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.zero = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>(CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.one = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>(CategoryTheory.Limits.parallelPair f g).map CategoryTheory.Limits.WalkingParallelPairHom.left = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>(CategoryTheory.Limits.parallelPair f g).map CategoryTheory.Limits.WalkingParallelPairHom.right = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C<VAR>j : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Limits.parallelPair (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)).obj j = F.obj j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C<VAR>X : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Limits.diagramIsoParallelPair F).hom.app X = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C<VAR>X : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Limits.diagramIsoParallelPair F).inv.app X = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y X' Y' : C<VAR>f g : X ⟶ Y<VAR>f' g' : X' ⟶ Y'<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f'<VAR>wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g'<GOAL>(CategoryTheory.Limits.parallelPairHom f g f' g' p q wf wg).app CategoryTheory.Limits.WalkingParallelPair.zero = p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y X' Y' : C<VAR>f g : X ⟶ Y<VAR>f' g' : X' ⟶ Y'<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f'<VAR>wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g'<GOAL>(CategoryTheory.Limits.parallelPairHom f g f' g' p q wf wg).app CategoryTheory.Limits.WalkingParallelPair.one = q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C<VAR>zero : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero<VAR>one : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one<VAR>left : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left)<VAR>right : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right)<VAR>X : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Limits.parallelPair.ext zero one left right).hom.app X = (CategoryTheory.Limits.WalkingParallelPair.rec zero one X).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C<VAR>zero : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero<VAR>one : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one<VAR>left : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left)<VAR>right : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right)<VAR>X : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Limits.parallelPair.ext zero one left right).inv.app X = (CategoryTheory.Limits.WalkingParallelPair.rec zero one X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g f' g' : X ⟶ Y<VAR>hf : f = f'<VAR>hg : g = g'<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelPair), (CategoryTheory.Limits.parallelPair.eqOfHomEq hf hg).hom.app X_1 = (CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.Iso.refl X) (CategoryTheory.Iso.refl Y) X_1).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g f' g' : X ⟶ Y<VAR>hf : f = f'<VAR>hg : g = g'<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelPair), (CategoryTheory.Limits.parallelPair.eqOfHomEq hf hg).inv.app X_1 = (CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.Iso.refl X) (CategoryTheory.Iso.refl Y) X_1).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Fork f g<GOAL>t.π.app CategoryTheory.Limits.WalkingParallelPair.zero = t.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Cofork f g<GOAL>t.ι.app CategoryTheory.Limits.WalkingParallelPair.one = t.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Fork f g<GOAL>s.π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp s.ι f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Fork f g<GOAL>s.π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp s.ι g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Cofork f g<GOAL>s.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = CategoryTheory.CategoryStruct.comp f s.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Cofork f g<GOAL>s.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = CategoryTheory.CategoryStruct.comp g s.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>P : C<VAR>ι : P ⟶ X<VAR>w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelPair), (CategoryTheory.Limits.Fork.ofι ι w).π.app X_1 = CategoryTheory.Limits.WalkingParallelPair.casesOn (motive := fun t => X_1 = t → (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj P).obj X_1 ⟶ (CategoryTheory.Limits.parallelPair f g).obj X_1)) X_1 (fun h => ⋯ ▸ ι) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp ι f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>P : C<VAR>ι : P ⟶ X<VAR>w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g<GOAL>(CategoryTheory.Limits.Fork.ofι ι w).pt = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>P : C<VAR>π : Y ⟶ P<VAR>w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π<GOAL>(CategoryTheory.Limits.Cofork.ofπ π w).pt = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>P : C<VAR>π : Y ⟶ P<VAR>w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelPair), (CategoryTheory.Limits.Cofork.ofπ π w).ι.app X_1 = CategoryTheory.Limits.WalkingParallelPair.casesOn X_1 (CategoryTheory.CategoryStruct.comp f π) π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>P : C<VAR>ι : P ⟶ X<VAR>w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g<GOAL>(CategoryTheory.Limits.Fork.ofι ι w).ι = ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>P : C<VAR>π : Y ⟶ P<VAR>w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π<GOAL>(CategoryTheory.Limits.Cofork.ofπ π w).π = π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Fork f g<GOAL>CategoryTheory.CategoryStruct.comp t.ι f = CategoryTheory.CategoryStruct.comp t.ι g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Cofork f g<GOAL>CategoryTheory.CategoryStruct.comp f t.π = CategoryTheory.CategoryStruct.comp g t.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Fork f g<VAR>W : C<VAR>k l : W ⟶ s.pt<VAR>h : CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι<VAR>j : CategoryTheory.Limits.WalkingParallelPair<GOAL>CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp l (s.π.app j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Cofork f g<VAR>W : C<VAR>k l : s.pt ⟶ W<VAR>h : CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l<VAR>j : CategoryTheory.Limits.WalkingParallelPair<GOAL>CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (s.ι.app j) l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Fork f g<VAR>hs : CategoryTheory.Limits.IsLimit s<VAR>W : C<VAR>k l : W ⟶ s.pt<VAR>h : CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι<GOAL>k = l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Cofork f g<VAR>hs : CategoryTheory.Limits.IsColimit s<VAR>W : C<VAR>k l : s.pt ⟶ W<VAR>h : CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l<GOAL>k = l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Fork f g<VAR>hs : CategoryTheory.Limits.IsLimit s<GOAL>CategoryTheory.CategoryStruct.comp (hs.lift t) s.ι = t.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Cofork f g<VAR>hs : CategoryTheory.Limits.IsColimit s<GOAL>CategoryTheory.CategoryStruct.comp s.π (hs.desc t) = t.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Fork f g<VAR>hs : CategoryTheory.Limits.IsLimit s<VAR>W : C<VAR>k : W ⟶ X<VAR>h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.IsLimit.lift hs k h) s.ι = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Cofork f g<VAR>hs : CategoryTheory.Limits.IsColimit s<VAR>W : C<VAR>k : Y ⟶ W<VAR>h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k<GOAL>CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.Limits.Cofork.IsColimit.desc hs k h) = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Fork f g<VAR>hs : CategoryTheory.Limits.IsLimit s<VAR>W : C<VAR>k : W ⟶ X<VAR>h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g<GOAL>∃! l, CategoryTheory.CategoryStruct.comp l s.ι = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : CategoryTheory.Limits.Cofork f g<VAR>hs : CategoryTheory.Limits.IsColimit s<VAR>W : C<VAR>k : Y ⟶ W<VAR>h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k<GOAL>∃! d, CategoryTheory.CategoryStruct.comp s.π d = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Fork f g<VAR>lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt<VAR>fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι<VAR>uniq : ∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt ⟶ t.pt), CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = lift s<VAR>s : CategoryTheory.Limits.Fork f g<GOAL>(CategoryTheory.Limits.Fork.IsLimit.mk t lift fac uniq).lift s = lift s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Fork f g<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>Z : C<VAR>h : { h // CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g }<GOAL>(CategoryTheory.Limits.Fork.IsLimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Fork.IsLimit.lift' ht ↑h ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Fork f g<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>Z : C<VAR>k : Z ⟶ t.pt<GOAL>↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp k t.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Fork f g<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>Z Z' : C<VAR>q : Z' ⟶ Z<VAR>k : Z ⟶ t.pt<GOAL>↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp q k)) = CategoryTheory.CategoryStruct.comp q ↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z) k)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Cofork f g<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>Z : C<VAR>k : t.pt ⟶ Z<GOAL>↑((CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp t.π k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Cofork f g<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>Z : C<VAR>h : { h // CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h }<GOAL>(CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Cofork.IsColimit.desc' ht ↑h ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Cofork f g<VAR>Z Z' : C<VAR>q : Z ⟶ Z'<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>k : t.pt ⟶ Z<GOAL>↑((CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp k q)) = CategoryTheory.CategoryStruct.comp (↑((CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z) k)) q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C<VAR>t : CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)<VAR>j : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Limits.Cone.ofFork t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C<VAR>t : CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)<VAR>j : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Limits.Cocone.ofCofork t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C<VAR>t : CategoryTheory.Limits.Cone F<VAR>j : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Limits.Fork.ofCone t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C<VAR>t : CategoryTheory.Limits.Cocone F<VAR>j : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Limits.Cofork.ofCocone t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g f' g' : X ⟶ Y<VAR>α : CategoryTheory.Limits.parallelPair f g ⟶ CategoryTheory.Limits.parallelPair f' g'<VAR>c : CategoryTheory.Limits.Fork f g<GOAL>CategoryTheory.Limits.Fork.ι ((CategoryTheory.Limits.Cones.postcompose α).obj c) = CategoryTheory.CategoryStruct.comp c.ι (α.app CategoryTheory.Limits.WalkingParallelPair.zero)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g f' g' : X ⟶ Y<VAR>α : CategoryTheory.Limits.parallelPair f g ⟶ CategoryTheory.Limits.parallelPair f' g'<VAR>c : CategoryTheory.Limits.Cofork f' g'<GOAL>CategoryTheory.Limits.Cofork.π ((CategoryTheory.Limits.Cocones.precompose α).obj c) = CategoryTheory.CategoryStruct.comp (α.app CategoryTheory.Limits.WalkingParallelPair.one) c.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Fork f g<VAR>k : s.pt ⟶ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι<GOAL>(CategoryTheory.Limits.Fork.mkHom k w).hom = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Fork f g<VAR>i : s.pt ≅ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by aesop_cat<GOAL>(CategoryTheory.Limits.Fork.ext i w).inv = CategoryTheory.Limits.Fork.mkHom i.inv ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Fork f g<VAR>i : s.pt ≅ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by aesop_cat<GOAL>(CategoryTheory.Limits.Fork.ext i w).hom = CategoryTheory.Limits.Fork.mkHom i.hom w
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Cofork f g<VAR>k : s.pt ⟶ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp s.π k = t.π<GOAL>(CategoryTheory.Limits.Cofork.mkHom k w).hom = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Fork f g<GOAL>∀ (f_1 : s ⟶ t), CategoryTheory.CategoryStruct.comp f_1.hom t.ι = s.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Cofork f g<GOAL>∀ (f_1 : s ⟶ t), CategoryTheory.CategoryStruct.comp s.π f_1.hom = t.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Cofork f g<VAR>i : s.pt ≅ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp s.π i.hom = t.π := by aesop_cat<GOAL>(CategoryTheory.Limits.Cofork.ext i w).hom = CategoryTheory.Limits.Cofork.mkHom i.hom w
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : CategoryTheory.Limits.Cofork f g<VAR>i : s.pt ≅ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp s.π i.hom = t.π := by aesop_cat<GOAL>(CategoryTheory.Limits.Cofork.ext i w).inv = CategoryTheory.Limits.Cofork.mkHom i.inv ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<GOAL>(CategoryTheory.Limits.equalizer.fork f g).ι = CategoryTheory.Limits.equalizer.ι f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<GOAL>(CategoryTheory.Limits.equalizer.fork f g).π.app CategoryTheory.Limits.WalkingParallelPair.zero = CategoryTheory.Limits.equalizer.ι f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>W : C<VAR>k : W ⟶ X<VAR>h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift k h) (CategoryTheory.Limits.equalizer.ι f g) = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>W : C<VAR>k l : W ⟶ CategoryTheory.Limits.equalizer f g<VAR>h : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.equalizer.ι f g) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g)<GOAL>k = l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>W : C<VAR>k : W ⟶ X<VAR>h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g<GOAL>∃! l, CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.Fork f g<VAR>i : CategoryTheory.Limits.IsLimit c<GOAL>CategoryTheory.Mono c.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h₀ : f = g<VAR>c : CategoryTheory.Limits.Fork f g<VAR>h : CategoryTheory.Limits.IsLimit c<GOAL>CategoryTheory.IsIso c.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>h : f = g<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.equalizer.ι f g)