ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : CategoryTheory.Limits.PullbackCone f g<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Mono t.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : CategoryTheory.Limits.PullbackCone f g<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>CategoryTheory.Mono g<GOAL>CategoryTheory.Mono t.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (𝟙 X) (𝟙 X) ⋯)<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Limits.pullback.fst f f = CategoryTheory.Limits.pullback.snd f f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.Limits.pullbackSymmetry f f).hom = 𝟙 (CategoryTheory.Limits.pullback f f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.Epi t.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : CategoryTheory.Limits.PushoutCocone f g<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>CategoryTheory.Epi g<GOAL>CategoryTheory.Epi t.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>t : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (𝟙 Y) (𝟙 Y) ⋯)<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.Limits.pushout.inl f f = CategoryTheory.Limits.pushout.inr f f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>(CategoryTheory.Limits.pushoutSymmetry f f).hom = 𝟙 (CategoryTheory.Limits.pushout f f)
<VAR>J : Type w<VAR>X : CategoryTheory.Limits.WalkingParallelFamily J<GOAL>CategoryTheory.Limits.WalkingParallelFamily.Hom.id X = CategoryTheory.CategoryStruct.id X
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<GOAL>(CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.zero = X
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<GOAL>(CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.one = Y
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>j : J<GOAL>(CategoryTheory.Limits.parallelFamily f).map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j) = f j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C<VAR>X : CategoryTheory.Limits.WalkingParallelFamily J<GOAL>(CategoryTheory.Limits.diagramIsoParallelFamily F).inv.app X = CategoryTheory.eqToHom ⋯
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C<VAR>X : CategoryTheory.Limits.WalkingParallelFamily J<GOAL>(CategoryTheory.Limits.diagramIsoParallelFamily F).hom.app X = CategoryTheory.eqToHom ⋯
<VAR>X : CategoryTheory.Limits.WalkingParallelPair<GOAL>CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.counitIso.hom.app X = CategoryTheory.eqToHom ⋯
<VAR>x y : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)<VAR>h : x ⟶ y<GOAL>CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.functor.map h = match x, y, h with | x, .(x), CategoryTheory.Limits.WalkingParallelFamily.Hom.id .(x) => CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.WalkingParallelFamily.rec CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one x) | .(CategoryTheory.Limits.WalkingParallelFamily.zero), .(CategoryTheory.Limits.WalkingParallelFamily.one), CategoryTheory.Limits.WalkingParallelFamily.Hom.line j => bif j.down then CategoryTheory.Limits.WalkingParallelPairHom.left else CategoryTheory.Limits.WalkingParallelPairHom.right
<VAR>X : CategoryTheory.Limits.WalkingParallelPair<GOAL>CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.counitIso.inv.app X = CategoryTheory.eqToHom ⋯
<VAR>X : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)<GOAL>CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.unitIso.inv.app X = CategoryTheory.eqToHom ⋯
<VAR>x : CategoryTheory.Limits.WalkingParallelPair<GOAL>CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.inverse.obj x = match x with | CategoryTheory.Limits.WalkingParallelPair.zero => CategoryTheory.Limits.WalkingParallelFamily.zero | CategoryTheory.Limits.WalkingParallelPair.one => CategoryTheory.Limits.WalkingParallelFamily.one
<VAR>X : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)<GOAL>CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.unitIso.hom.app X = CategoryTheory.eqToHom ⋯
<VAR>x : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)<GOAL>CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.functor.obj x = CategoryTheory.Limits.WalkingParallelFamily.rec CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one x
<GOAL>∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y), CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.inverse.map h = match X, Y, h with | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => CategoryTheory.CategoryStruct.id (match x with | CategoryTheory.Limits.WalkingParallelPair.zero => CategoryTheory.Limits.WalkingParallelFamily.zero | CategoryTheory.Limits.WalkingParallelPair.one => CategoryTheory.Limits.WalkingParallelFamily.one) | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.left => CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := true } | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.right => CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := false }
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>t : CategoryTheory.Limits.Trident f<GOAL>t.ι = t.π.app CategoryTheory.Limits.WalkingParallelFamily.zero
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>t : CategoryTheory.Limits.Cotrident f<GOAL>t.π = t.ι.app CategoryTheory.Limits.WalkingParallelFamily.one
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>s : CategoryTheory.Limits.Trident f<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero) (f j) = s.π.app CategoryTheory.Limits.WalkingParallelFamily.one
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>s : CategoryTheory.Limits.Cotrident f<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (f j) (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.one) = s.ι.app CategoryTheory.Limits.WalkingParallelFamily.zero
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>P : C<VAR>ι : P ⟶ X<VAR>w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelFamily J), (CategoryTheory.Limits.Trident.ofι ι w).π.app X_1 = CategoryTheory.Limits.WalkingParallelFamily.casesOn X_1 ι (CategoryTheory.CategoryStruct.comp ι (f (Classical.arbitrary J)))
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>P : C<VAR>ι : P ⟶ X<VAR>w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)<GOAL>(CategoryTheory.Limits.Trident.ofι ι w).pt = P
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>P : C<VAR>π : Y ⟶ P<VAR>w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π<GOAL>(CategoryTheory.Limits.Cotrident.ofπ π w).pt = P
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>P : C<VAR>π : Y ⟶ P<VAR>w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelFamily J), (CategoryTheory.Limits.Cotrident.ofπ π w).ι.app X_1 = CategoryTheory.Limits.WalkingParallelFamily.casesOn X_1 (CategoryTheory.CategoryStruct.comp (f (Classical.arbitrary J)) π) π
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>P : C<VAR>ι : P ⟶ X<VAR>w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)<GOAL>(CategoryTheory.Limits.Trident.ofι ι w).ι = ι
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>P : C<VAR>π : Y ⟶ P<VAR>w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π<GOAL>(CategoryTheory.Limits.Cotrident.ofπ π w).π = π
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>j₁ j₂ : J<VAR>t : CategoryTheory.Limits.Trident f<GOAL>CategoryTheory.CategoryStruct.comp t.ι (f j₁) = CategoryTheory.CategoryStruct.comp t.ι (f j₂)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>j₁ j₂ : J<VAR>t : CategoryTheory.Limits.Cotrident f<GOAL>CategoryTheory.CategoryStruct.comp (f j₁) t.π = CategoryTheory.CategoryStruct.comp (f j₂) t.π
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>s : CategoryTheory.Limits.Trident f<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.WalkingParallelFamily J<GOAL>CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp l (s.π.app j)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>s : CategoryTheory.Limits.Cotrident f<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.WalkingParallelFamily J<GOAL>CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (s.ι.app j) l
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>s : CategoryTheory.Limits.Trident f<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>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>s : CategoryTheory.Limits.Cotrident f<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>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>t : CategoryTheory.Limits.Trident f<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>Z : C<VAR>h : { h // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp h (f j₁) = CategoryTheory.CategoryStruct.comp h (f j₂) }<GOAL>(CategoryTheory.Limits.Trident.IsLimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Trident.IsLimit.lift' ht ↑h ⋯)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>t : CategoryTheory.Limits.Trident f<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>Z : C<VAR>k : Z ⟶ t.pt<GOAL>↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp k t.ι
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>t : CategoryTheory.Limits.Trident f<VAR>ht : CategoryTheory.Limits.IsLimit t<VAR>Z Z' : C<VAR>q : Z' ⟶ Z<VAR>k : Z ⟶ t.pt<GOAL>↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp q k)) = CategoryTheory.CategoryStruct.comp q ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z) k)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>t : CategoryTheory.Limits.Cotrident f<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>Z : C<VAR>k : t.pt ⟶ Z<GOAL>↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp t.π k
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>t : CategoryTheory.Limits.Cotrident f<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>Z : C<VAR>h : { h // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) h = CategoryTheory.CategoryStruct.comp (f j₂) h }<GOAL>(CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Cotrident.IsColimit.desc' ht ↑h ⋯)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>t : CategoryTheory.Limits.Cotrident f<VAR>Z Z' : C<VAR>q : Z ⟶ Z'<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>k : t.pt ⟶ Z<GOAL>↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp k q)) = CategoryTheory.CategoryStruct.comp (↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z) k)) q
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C<VAR>t : CategoryTheory.Limits.Trident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)<VAR>j : CategoryTheory.Limits.WalkingParallelFamily J<GOAL>(CategoryTheory.Limits.Cone.ofTrident t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C<VAR>t : CategoryTheory.Limits.Cotrident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)<VAR>j : CategoryTheory.Limits.WalkingParallelFamily J<GOAL>(CategoryTheory.Limits.Cocone.ofCotrident t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C<VAR>t : CategoryTheory.Limits.Cone F<VAR>j : CategoryTheory.Limits.WalkingParallelFamily J<GOAL>(CategoryTheory.Limits.Trident.ofCone t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C<VAR>t : CategoryTheory.Limits.Cocone F<VAR>j : CategoryTheory.Limits.WalkingParallelFamily J<GOAL>(CategoryTheory.Limits.Cotrident.ofCocone t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>s t : CategoryTheory.Limits.Trident f<VAR>k : s.pt ⟶ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι := by aesop_cat<GOAL>(CategoryTheory.Limits.Trident.mkHom k w).hom = k
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>s t : CategoryTheory.Limits.Trident f<VAR>i : s.pt ≅ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by aesop_cat<GOAL>(CategoryTheory.Limits.Trident.ext i w).hom = CategoryTheory.Limits.Trident.mkHom i.hom w
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>s t : CategoryTheory.Limits.Trident f<VAR>i : s.pt ≅ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by aesop_cat<GOAL>(CategoryTheory.Limits.Trident.ext i w).inv = CategoryTheory.Limits.Trident.mkHom i.inv ⋯
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>s t : CategoryTheory.Limits.Cotrident f<VAR>k : s.pt ⟶ t.pt<VAR>w : CategoryTheory.CategoryStruct.comp s.π k = t.π := by aesop_cat<GOAL>(CategoryTheory.Limits.Cotrident.mkHom k w).hom = k
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideEqualizer f<GOAL>(CategoryTheory.Limits.wideEqualizer.trident f).ι = CategoryTheory.Limits.wideEqualizer.ι f
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideEqualizer f<GOAL>(CategoryTheory.Limits.wideEqualizer.trident f).π.app CategoryTheory.Limits.WalkingParallelFamily.zero = CategoryTheory.Limits.wideEqualizer.ι f
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideEqualizer f<VAR>j₁ j₂ : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (f j₁) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (f j₂)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideEqualizer f<VAR>Nonempty J<VAR>W : C<VAR>k : W ⟶ X<VAR>h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.lift k h) (CategoryTheory.Limits.wideEqualizer.ι f) = k
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideEqualizer f<VAR>Nonempty J<VAR>W : C<VAR>k l : W ⟶ CategoryTheory.Limits.wideEqualizer f<VAR>h : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.wideEqualizer.ι f) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.wideEqualizer.ι f)<GOAL>k = l
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>c : CategoryTheory.Limits.Cone (CategoryTheory.Limits.parallelFamily f)<VAR>i : CategoryTheory.Limits.IsLimit c<GOAL>CategoryTheory.Mono (CategoryTheory.Limits.Trident.ι c)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideCoequalizer f<GOAL>(CategoryTheory.Limits.wideCoequalizer.cotrident f).π = CategoryTheory.Limits.wideCoequalizer.π f
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideCoequalizer f<GOAL>(CategoryTheory.Limits.wideCoequalizer.cotrident f).ι.app CategoryTheory.Limits.WalkingParallelFamily.one = CategoryTheory.Limits.wideCoequalizer.π f
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideCoequalizer f<VAR>j₁ j₂ : J<GOAL>CategoryTheory.CategoryStruct.comp (f j₁) (CategoryTheory.Limits.wideCoequalizer.π f) = CategoryTheory.CategoryStruct.comp (f j₂) (CategoryTheory.Limits.wideCoequalizer.π f)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideCoequalizer f<VAR>Nonempty J<VAR>W : C<VAR>k : Y ⟶ W<VAR>h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) (CategoryTheory.Limits.wideCoequalizer.desc k h) = k
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>CategoryTheory.Limits.HasWideCoequalizer f<VAR>Nonempty J<VAR>W : C<VAR>k l : CategoryTheory.Limits.wideCoequalizer f ⟶ W<VAR>h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) l<GOAL>k = l
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>Nonempty J<VAR>c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.parallelFamily f)<VAR>i : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.Epi (c.ι.app CategoryTheory.Limits.WalkingParallelFamily.one)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelFamily f)<GOAL>CategoryTheory.Limits.HasWideEqualizers C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelFamily f)<GOAL>CategoryTheory.Limits.HasWideCoequalizers C
<VAR>β : Type v<VAR>Small.{u, v} β<VAR>f : β → Type u<VAR>P : Type u<VAR>s : (b : β) → P ⟶ f b<VAR>b : β<VAR>x : P<GOAL>CategoryTheory.Limits.Pi.π f b (CategoryTheory.Limits.Pi.lift s x) = s b x
<VAR>β : Type v<VAR>f : β → Type v<VAR>P : Type v<VAR>s : (b : β) → P ⟶ f b<VAR>b : β<VAR>x : P<GOAL>CategoryTheory.Limits.Pi.π f b (CategoryTheory.Limits.Pi.lift s x) = s b x
<VAR>β : Type v<VAR>Small.{u, v} β<VAR>f g : β → Type u<VAR>α : (j : β) → f j ⟶ g j<VAR>b : β<VAR>x : ∏ᶜ f<GOAL>CategoryTheory.Limits.Pi.π g b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π f b x)
<VAR>β : Type v<VAR>f g : β → Type v<VAR>α : (j : β) → f j ⟶ g j<VAR>b : β<VAR>x : ∏ᶜ f<GOAL>CategoryTheory.Limits.Pi.π g b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π f b x)
<VAR>X : Type u<GOAL>Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty X
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductCone X Y).pt = (X × Y)
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductCone X Y).fst = Prod.fst
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductCone X Y).snd = Prod.snd
<VAR>X Y : Type u<VAR>s : CategoryTheory.Limits.BinaryFan X Y<VAR>x : s.pt<GOAL>(CategoryTheory.Limits.Types.binaryProductLimit X Y).lift s x = (s.fst x, s.snd x)
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone = CategoryTheory.Limits.Types.binaryProductCone X Y
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductLimitCone X Y).isLimit = CategoryTheory.Limits.Types.binaryProductLimit X Y
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductIso X Y).hom ≫ Prod.fst = CategoryTheory.Limits.prod.fst
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductIso X Y).hom ≫ Prod.snd = CategoryTheory.Limits.prod.snd
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductIso X Y).inv ≫ CategoryTheory.Limits.prod.fst = Prod.fst
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductIso X Y).inv ≫ CategoryTheory.Limits.prod.snd = Prod.snd
<VAR>X : Type u<VAR>Y₁ Y₂ : Type u<VAR>f : Y₁ ⟶ Y₂<GOAL>∀ (a : (CategoryTheory.Limits.BinaryFan.mk Prod.fst (Prod.snd ≫ f)).pt), (CategoryTheory.Limits.Types.binaryProductFunctor.obj X).map f a = (CategoryTheory.Limits.Types.binaryProductLimit X Y₂).lift (CategoryTheory.Limits.BinaryFan.mk Prod.fst (Prod.snd ≫ f)) a
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryProductFunctor.obj X).obj Y = (X × Y)