ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j : D.J<GOAL>D.diagram.snd (i, j) = CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<GOAL>D.diagram.left = D.V
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<GOAL>D.diagram.right = D.U
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>CategoryTheory.Limits.HasMulticoequalizer D.diagram<VAR>i j : D.J<GOAL>CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (D.ι j)) = CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)
<VAR>D : CategoryTheory.GlueData (Type u_1)<GOAL>Function.Surjective D.π
<VAR>D : CategoryTheory.GlueData (Type v)<VAR>x : D.glued<GOAL>∃ i y, D.ι i y = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i j : D.J<GOAL>(D.mapGlueData F).f i j = F.map (D.f i j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i : D.J × D.J<GOAL>(D.mapGlueData F).V i = F.obj (D.V i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i j k : D.J<GOAL>(D.mapGlueData F).t' i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso F (D.f i j) (D.f i k)).inv (CategoryTheory.CategoryStruct.comp (F.map (D.t' i j k)) (CategoryTheory.Limits.PreservesPullback.iso F (D.f j k) (D.f j i)).hom)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<GOAL>(D.mapGlueData F).J = D.J
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i : D.J<GOAL>(D.mapGlueData F).U i = F.obj (D.U i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i j : D.J<GOAL>(D.mapGlueData F).t i j = F.map (D.t i j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i : D.J × D.J<GOAL>(D.diagramIso F).app (CategoryTheory.Limits.WalkingMultispan.left i) = CategoryTheory.Iso.refl ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.left i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i : D.J<GOAL>(D.diagramIso F).app (CategoryTheory.Limits.WalkingMultispan.right i) = CategoryTheory.Iso.refl ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.right i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i : D.J × D.J<GOAL>(D.diagramIso F).hom.app (CategoryTheory.Limits.WalkingMultispan.left i) = CategoryTheory.CategoryStruct.id ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.left i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i : D.J<GOAL>(D.diagramIso F).hom.app (CategoryTheory.Limits.WalkingMultispan.right i) = CategoryTheory.CategoryStruct.id ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.right i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i : D.J × D.J<GOAL>(D.diagramIso F).inv.app (CategoryTheory.Limits.WalkingMultispan.left i) = CategoryTheory.CategoryStruct.id ((D.mapGlueData F).diagram.multispan.obj (CategoryTheory.Limits.WalkingMultispan.left i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>i : D.J<GOAL>(D.diagramIso F).inv.app (CategoryTheory.Limits.WalkingMultispan.right i) = CategoryTheory.CategoryStruct.id ((D.mapGlueData F).diagram.multispan.obj (CategoryTheory.Limits.WalkingMultispan.right i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>CategoryTheory.Limits.HasMulticoequalizer D.diagram<VAR>CategoryTheory.Limits.PreservesColimit D.diagram.multispan F<GOAL>CategoryTheory.Limits.HasColimit (D.diagram.multispan.comp F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>CategoryTheory.Limits.HasMulticoequalizer D.diagram<VAR>CategoryTheory.Limits.PreservesColimit D.diagram.multispan F<GOAL>CategoryTheory.Limits.HasMulticoequalizer (D.mapGlueData F).diagram
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>CategoryTheory.Limits.HasMulticoequalizer D.diagram<VAR>CategoryTheory.Limits.PreservesColimit D.diagram.multispan F<VAR>i : D.J<GOAL>CategoryTheory.CategoryStruct.comp (F.map (D.ι i)) (D.gluedIso F).hom = (D.mapGlueData F).ι i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>C' : Type u₂<VAR>CategoryTheory.Category.{v, u₂} C'<VAR>D : CategoryTheory.GlueData C<VAR>F : CategoryTheory.Functor C C'<VAR>H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>CategoryTheory.Limits.HasMulticoequalizer D.diagram<VAR>CategoryTheory.Limits.PreservesColimit D.diagram.multispan F<VAR>i : D.J<GOAL>CategoryTheory.CategoryStruct.comp ((D.mapGlueData F).ι i) (D.gluedIso F).inv = F.map (D.ι i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>CategoryTheory.Limits.HasMulticoequalizer D.diagram<VAR>F : CategoryTheory.Functor C (Type v)<VAR>CategoryTheory.Limits.PreservesColimit D.diagram.multispan F<VAR>(i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F<VAR>x : F.obj D.glued<GOAL>∃ i y, F.map (D.ι i) y = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData' C<VAR>i j : self.J<VAR>hij : i ≠ j<GOAL>CategoryTheory.CategoryStruct.comp (self.t i j hij) (self.t j i ⋯) = CategoryTheory.CategoryStruct.id (self.V i j hij)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData' C<VAR>i j k : self.J<VAR>hij : i ≠ j<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>CategoryTheory.CategoryStruct.comp (self.t' i j k hij hik hjk) (CategoryTheory.CategoryStruct.comp (self.t' j k i hjk ⋯ ⋯) (self.t' k i j ⋯ ⋯ hij)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j hij) (self.f i k hik))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData' C<VAR>i j k : self.J<VAR>hij : i ≠ j<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>CategoryTheory.CategoryStruct.comp (self.t' i j k hij hik hjk) (CategoryTheory.Limits.pullback.snd (self.f j k hjk) (self.f j i ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (self.f i j hij) (self.f i k hik)) (self.t i j hij)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData' C<VAR>i j k : self.J<VAR>hij : i ≠ j<VAR>hik : i ≠ k<GOAL>CategoryTheory.Limits.HasPullback (self.f i j hij) (self.f i k hik)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData' C<VAR>i j : self.J<VAR>h : i ≠ j<GOAL>CategoryTheory.Mono (self.f i j h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasFiniteLimits C<VAR>J : Type<VAR>𝒥 : CategoryTheory.SmallCategory J<VAR>CategoryTheory.FinCategory J<GOAL>CategoryTheory.Limits.HasLimitsOfShape J C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfSize.{v', u', v, u} C<GOAL>CategoryTheory.Limits.HasFiniteLimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>h : ∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J}, CategoryTheory.FinCategory J → CategoryTheory.Limits.HasLimitsOfShape J C<GOAL>CategoryTheory.Limits.HasFiniteLimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasFiniteColimits C<VAR>J : Type<VAR>𝒥 : CategoryTheory.SmallCategory J<VAR>CategoryTheory.FinCategory J<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfSize.{v', u', v, u} C<GOAL>CategoryTheory.Limits.HasFiniteColimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>h : ∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J}, CategoryTheory.FinCategory J → CategoryTheory.Limits.HasColimitsOfShape J C<GOAL>CategoryTheory.Limits.HasFiniteColimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasFiniteWidePullbacks C<VAR>J : Type<VAR>Finite J<GOAL>CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasFiniteWidePushouts C<VAR>J : Type<VAR>Finite J<GOAL>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteLimits C<GOAL>CategoryTheory.Limits.HasFiniteWidePullbacks C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteColimits C<GOAL>CategoryTheory.Limits.HasFiniteWidePushouts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>self : CategoryTheory.IsReflexivePair f g<GOAL>∃ s, CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B ∧ CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsReflexivePair f g<GOAL>∃ s, CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B ∧ CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>self : CategoryTheory.IsCoreflexivePair f g<GOAL>∃ s, CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A ∧ CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsCoreflexivePair f g<GOAL>∃ s, CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A ∧ CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>s : B ⟶ A<VAR>sf : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B<VAR>sg : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B<GOAL>CategoryTheory.IsReflexivePair f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>s : B ⟶ A<VAR>fs : CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A<VAR>gs : CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A<GOAL>CategoryTheory.IsCoreflexivePair f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsReflexivePair f g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.commonSection f g) f = CategoryTheory.CategoryStruct.id B
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsReflexivePair f g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.commonSection f g) g = CategoryTheory.CategoryStruct.id B
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsCoreflexivePair f g<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.commonRetraction f g) = CategoryTheory.CategoryStruct.id A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsCoreflexivePair f g<GOAL>CategoryTheory.CategoryStruct.comp g (CategoryTheory.commonRetraction f g) = CategoryTheory.CategoryStruct.id A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B R : C<VAR>f g : R ⟶ A<VAR>q : A ⟶ B<VAR>h : CategoryTheory.IsKernelPair q f g<GOAL>CategoryTheory.IsReflexivePair f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsReflexivePair f g<GOAL>CategoryTheory.IsReflexivePair g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsCoreflexivePair f g<GOAL>CategoryTheory.IsCoreflexivePair g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasReflexiveCoequalizers C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsReflexivePair f g<GOAL>CategoryTheory.Limits.HasCoequalizer f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasCoreflexiveEqualizers C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>CategoryTheory.IsCoreflexivePair f g<GOAL>CategoryTheory.Limits.HasEqualizer f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasReflexiveCoequalizers C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>r : B ⟶ A<VAR>rf : CategoryTheory.CategoryStruct.comp r f = CategoryTheory.CategoryStruct.id B<VAR>rg : CategoryTheory.CategoryStruct.comp r g = CategoryTheory.CategoryStruct.id B<GOAL>CategoryTheory.Limits.HasCoequalizer f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasCoreflexiveEqualizers C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>r : B ⟶ A<VAR>fr : CategoryTheory.CategoryStruct.comp f r = CategoryTheory.CategoryStruct.id A<VAR>gr : CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.id A<GOAL>CategoryTheory.Limits.HasEqualizer f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ C<VAR>c₁ : CategoryTheory.Limits.Fan F.obj<VAR>c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2<VAR>s t : c₁.pt ⟶ c₂.pt<VAR>hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd<VAR>ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }<VAR>i : CategoryTheory.Limits.Fork s t<GOAL>(CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).pt = i.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ C<VAR>c₁ : CategoryTheory.Limits.Fan F.obj<VAR>c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2<VAR>s t : c₁.pt ⟶ c₂.pt<VAR>hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd<VAR>ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }<VAR>i : CategoryTheory.Limits.Fork s t<VAR>j : J<GOAL>(CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).π.app j = i.ι ≫ c₁.π.app { as := j }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F.obj)<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.2)<VAR>CategoryTheory.Limits.HasEqualizers C<GOAL>CategoryTheory.Limits.HasLimit F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>CategoryTheory.Limits.HasEqualizers C<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasEqualizers C<GOAL>CategoryTheory.Limits.HasFiniteLimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>CategoryTheory.Limits.HasFiniteLimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ C<VAR>c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1<VAR>c₂ : CategoryTheory.Limits.Cofan F.obj<VAR>s t : c₁.pt ⟶ c₂.pt<VAR>hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }<VAR>ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }<VAR>i : CategoryTheory.Limits.Cofork s t<GOAL>(CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i).pt = i.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ C<VAR>c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1<VAR>c₂ : CategoryTheory.Limits.Cofan F.obj<VAR>s t : c₁.pt ⟶ c₂.pt<VAR>hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }<VAR>ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }<VAR>i : CategoryTheory.Limits.Cofork s t<VAR>j : J<GOAL>(CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i).ι.app j = c₂.ι.app { as := j } ≫ i.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor F.obj)<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.1)<VAR>CategoryTheory.Limits.HasCoequalizers C<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasCoproducts C<VAR>CategoryTheory.Limits.HasCoequalizers C<GOAL>CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.Limits.HasCoequalizers C<GOAL>CategoryTheory.Limits.HasFiniteColimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasPushouts C<GOAL>CategoryTheory.Limits.HasFiniteColimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasStrictInitialObjects C<VAR>I A : C<VAR>f : A ⟶ I<GOAL>CategoryTheory.Limits.IsInitial I → CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>I : C<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>A : C<VAR>f : A ⟶ I<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>I : C<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>A : C<VAR>f g : A ⟶ I<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>I : C<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>A : C<GOAL>Subsingleton (A ⟶ I)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>I : C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProduct X I<VAR>hI : CategoryTheory.Limits.IsInitial I<GOAL>(CategoryTheory.Limits.mulIsInitial X hI).hom = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>I : C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProduct X I<VAR>hI : CategoryTheory.Limits.IsInitial I<GOAL>(CategoryTheory.Limits.mulIsInitial X hI).inv = hI.to (X ⨯ I)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>I : C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProduct I X<VAR>hI : CategoryTheory.Limits.IsInitial I<GOAL>(CategoryTheory.Limits.isInitialMul X hI).hom = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>I : C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProduct I X<VAR>hI : CategoryTheory.Limits.IsInitial I<GOAL>(CategoryTheory.Limits.isInitialMul X hI).inv = hI.to (I ⨯ X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>CategoryTheory.Limits.HasInitial C<VAR>A : C<VAR>f g : A ⟶ ⊥_ C<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>CategoryTheory.Limits.HasInitial C<VAR>A : C<GOAL>Subsingleton (A ⟶ ⊥_ C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>CategoryTheory.Limits.HasInitial C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)<GOAL>(CategoryTheory.Limits.mulInitial X).hom = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>CategoryTheory.Limits.HasInitial C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)<GOAL>(CategoryTheory.Limits.mulInitial X).inv = CategoryTheory.Limits.initial.to (X ⨯ ⊥_ C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>CategoryTheory.Limits.HasInitial C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X<GOAL>(CategoryTheory.Limits.initialMul X).hom = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictInitialObjects C<VAR>CategoryTheory.Limits.HasInitial C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X<GOAL>(CategoryTheory.Limits.initialMul X).inv = CategoryTheory.Limits.initial.to ((⊥_ C) ⨯ X)