ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁) (CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂) = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk (z₁.comp₀ z₂ z₃)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>z₁ z₂ : W.LeftFraction X Y<VAR>h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂<GOAL>CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁ = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>z₁ z₂ : W.LeftFraction X Y<GOAL>CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁ = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂ ↔ CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Y' : C<VAR>f : X ⟶ Y'<VAR>s : Y ⟶ Y'<VAR>hs : W s<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map f) (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk (CategoryTheory.MorphismProperty.LeftFraction.mk f s hs)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso s hs).hom = (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso s hs).inv = CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s) (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>X Y : C<VAR>f : W.LeftFraction X Y<VAR>F : CategoryTheory.Functor C E<VAR>hF : W.IsInvertedBy F<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk f).map F hF = f.map F hF
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<GOAL>W.IsInvertedBy (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>F : CategoryTheory.Functor C E<VAR>hF : W.IsInvertedBy F<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.lift F hF) = F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>F₁ F₂ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.LeftFraction.Localization W) E<VAR>h : (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).comp F₁ = (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).comp F₂<GOAL>F₁ = F₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : W.LeftFraction X Y<GOAL>CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk f = f.map (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f g : W.LeftFraction X Y<GOAL>f.map (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) ⋯ = g.map (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) ⋯ ↔ CategoryTheory.MorphismProperty.LeftFractionRel f g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<GOAL>φ.map L ⋯ = CategoryTheory.CategoryStruct.comp (L.map φ.f) (CategoryTheory.Localization.isoOfHom L W φ.s ⋯).inv
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>L₁ : CategoryTheory.Functor C D<VAR>L₂ : CategoryTheory.Functor C E<VAR>L₁.IsLocalization W<VAR>L₂.IsLocalization W<GOAL>(CategoryTheory.Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.compUniqFunctor L₁ L₂ W).hom.app X) (CategoryTheory.CategoryStruct.comp (φ.map L₂ ⋯) ((CategoryTheory.Localization.compUniqFunctor L₁ L₂ W).inv.app Y))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ₁ φ₂ : W.LeftFraction X Y<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>L₁ : CategoryTheory.Functor C D<VAR>L₂ : CategoryTheory.Functor C E<VAR>L₁.IsLocalization W<VAR>L₂.IsLocalization W<VAR>h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯<GOAL>φ₁.map L₂ ⋯ = φ₂.map L₂ ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<GOAL>CategoryTheory.CategoryStruct.comp (z₁.map L ⋯) (z₂.map L ⋯) = (z₁.comp₀ z₂ z₃).map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>∃ φ, f = φ.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ ψ : W.LeftFraction X Y<GOAL>φ.map L ⋯ = ψ.map L ⋯ ↔ CategoryTheory.MorphismProperty.LeftFractionRel φ ψ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f₁ f₂ : X ⟶ Y<GOAL>L.map f₁ = L.map f₂ ↔ ∃ Z s, ∃ (_ : W s), CategoryTheory.CategoryStruct.comp f₁ s = CategoryTheory.CategoryStruct.comp f₂ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<GOAL>L.mapArrow.EssSurj
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<GOAL>φ.op.f = φ.f.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<GOAL>φ.op.X' = Opposite.op φ.Y'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<GOAL>φ.op.s = φ.s.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.RightFraction X Y<GOAL>φ.op.s = φ.s.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.RightFraction X Y<GOAL>φ.op.Y' = Opposite.op φ.X'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.RightFraction X Y<GOAL>φ.op.f = φ.f.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>X Y : Cᵒᵖ<VAR>φ : W.LeftFraction X Y<GOAL>φ.unop.f = φ.f.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>X Y : Cᵒᵖ<VAR>φ : W.LeftFraction X Y<GOAL>φ.unop.s = φ.s.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>X Y : Cᵒᵖ<VAR>φ : W.LeftFraction X Y<GOAL>φ.unop.X' = Opposite.unop φ.Y'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>X Y : Cᵒᵖ<VAR>φ : W.RightFraction X Y<GOAL>φ.unop.f = φ.f.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>X Y : Cᵒᵖ<VAR>φ : W.RightFraction X Y<GOAL>φ.unop.s = φ.s.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>X Y : Cᵒᵖ<VAR>φ : W.RightFraction X Y<GOAL>φ.unop.Y' = Opposite.unop φ.X'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.RightFraction X Y<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<GOAL>(φ.map L hL).op = φ.op.map L.op ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<GOAL>(φ.map L hL).op = φ.op.map L.op ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ : W.RightFraction X Y<VAR>h : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂<GOAL>CategoryTheory.MorphismProperty.LeftFractionRel z₁.op z₂.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>X Y : Cᵒᵖ<VAR>z₁ z₂ : W.RightFraction X Y<VAR>h : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂<GOAL>CategoryTheory.MorphismProperty.LeftFractionRel z₁.unop z₂.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ : W.LeftFraction X Y<VAR>h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂<GOAL>CategoryTheory.MorphismProperty.RightFractionRel z₁.op z₂.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>X Y : Cᵒᵖ<VAR>z₁ z₂ : W.LeftFraction X Y<VAR>h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂<GOAL>CategoryTheory.MorphismProperty.RightFractionRel z₁.unop z₂.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ : W.RightFraction X Y<GOAL>CategoryTheory.MorphismProperty.LeftFractionRel z₁.op z₂.op ↔ CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ : W.LeftFraction X Y<GOAL>CategoryTheory.MorphismProperty.RightFractionRel z₁.op z₂.op ↔ CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z : W.RightFraction X Y<GOAL>CategoryTheory.MorphismProperty.RightFractionRel z z
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ : W.RightFraction X Y<VAR>h : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂<GOAL>CategoryTheory.MorphismProperty.RightFractionRel z₂ z₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ z₃ : W.RightFraction X Y<VAR>W.HasRightCalculusOfFractions<VAR>h₁₂ : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂<VAR>h₂₃ : CategoryTheory.MorphismProperty.RightFractionRel z₂ z₃<GOAL>CategoryTheory.MorphismProperty.RightFractionRel z₁ z₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>W.HasRightCalculusOfFractions<GOAL>Equivalence CategoryTheory.MorphismProperty.RightFractionRel
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>∃ φ, f = φ.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>φ ψ : W.RightFraction X Y<GOAL>φ.map L ⋯ = ψ.map L ⋯ ↔ CategoryTheory.MorphismProperty.RightFractionRel φ ψ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasRightCalculusOfFractions<VAR>Y Z : C<VAR>f₁ f₂ : Y ⟶ Z<GOAL>L.map f₁ = L.map f₂ ↔ ∃ X s, ∃ (_ : W s), CategoryTheory.CategoryStruct.comp s f₁ = CategoryTheory.CategoryStruct.comp s f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasRightCalculusOfFractions<GOAL>L.mapArrow.EssSurj
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ : C<VAR>self : CategoryTheory.Limits.CoproductDisjoint X₁ X₂<VAR>X : C<GOAL>∀ (X₁_1 : X₁ ⟶ X) (X₂_1 : X₂ ⟶ X), CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk X₁_1 X₂_1) → CategoryTheory.Mono X₂_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ : C<VAR>self : CategoryTheory.Limits.CoproductDisjoint X₁ X₂<VAR>X : C<GOAL>∀ (X₁_1 : X₁ ⟶ X) (X₂_1 : X₂ ⟶ X), CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk X₁_1 X₂_1) → CategoryTheory.Mono X₁_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.CoproductsDisjoint C<GOAL>CategoryTheory.Limits.InitialMonoClass C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>K : J ⥤ C<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasLimit (K ⋙ F)<VAR>CategoryTheory.CreatesLimit K F<GOAL>CategoryTheory.Limits.HasLimit K
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasLimitsOfShape J D<VAR>CategoryTheory.CreatesLimitsOfShape J F<GOAL>CategoryTheory.Limits.HasLimitsOfShape J C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} D<VAR>CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, u₁} C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>K : J ⥤ C<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasColimit (K ⋙ F)<VAR>CategoryTheory.CreatesColimit K F<GOAL>CategoryTheory.Limits.HasColimit K
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasColimitsOfShape J D<VAR>CategoryTheory.CreatesColimitsOfShape J F<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} D<VAR>CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F<GOAL>CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, u₁} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>self : CategoryTheory.IsSplitEqualizer f g ι<GOAL>CategoryTheory.CategoryStruct.comp g self.rightRetraction = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>self : CategoryTheory.IsSplitEqualizer f g ι<GOAL>CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>self : CategoryTheory.IsSplitEqualizer f g ι<GOAL>CategoryTheory.CategoryStruct.comp ι self.leftRetraction = CategoryTheory.CategoryStruct.id W
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>self : CategoryTheory.IsSplitEqualizer f g ι<GOAL>CategoryTheory.CategoryStruct.comp f self.rightRetraction = CategoryTheory.CategoryStruct.comp self.leftRetraction ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>q : CategoryTheory.IsSplitEqualizer f g ι<VAR>F : CategoryTheory.Functor C D<GOAL>(q.map F).leftRetraction = F.map q.leftRetraction
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>q : CategoryTheory.IsSplitEqualizer f g ι<VAR>F : CategoryTheory.Functor C D<GOAL>(q.map F).rightRetraction = F.map q.rightRetraction
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>h : W ⟶ X<VAR>t : CategoryTheory.IsSplitEqualizer f g h<GOAL>t.asFork.pt = W
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>h : W ⟶ X<VAR>t : CategoryTheory.IsSplitEqualizer f g h<GOAL>t.asFork.ι = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>self : CategoryTheory.HasSplitEqualizer f g<GOAL>∃ W h, Nonempty (CategoryTheory.IsSplitEqualizer f g h)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData C<VAR>i j k : self.J<GOAL>CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j) (self.f i k))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData C<VAR>i j : self.J<GOAL>CategoryTheory.Mono (self.f i j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData C<VAR>i j k : self.J<GOAL>CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.Limits.pullback.snd (self.f j k) (self.f j i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (self.f i j) (self.f i k)) (self.t i j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData C<VAR>i j k : self.J<GOAL>CategoryTheory.Limits.HasPullback (self.f i j) (self.f i k)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData C<VAR>i : self.J<GOAL>CategoryTheory.IsIso (self.f i i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>self : CategoryTheory.GlueData C<VAR>i : self.J<GOAL>self.t i i = CategoryTheory.CategoryStruct.id (self.V (i, i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j : D.J<GOAL>D.t' i i j = (CategoryTheory.Limits.pullbackSymmetry (D.f i i) (D.f i j)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j : D.J<GOAL>D.t' j i i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j i)) (CategoryTheory.CategoryStruct.comp (D.t j i) (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd (D.f i i) (D.f i j))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j : D.J<GOAL>D.t' i j i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i i)) (CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j i))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j : D.J<GOAL>CategoryTheory.CategoryStruct.comp (D.t i j) (D.t j i) = CategoryTheory.CategoryStruct.id (D.V (i, j))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j k : D.J<GOAL>CategoryTheory.CategoryStruct.comp (D.t' i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (D.f j k) (D.f j i)).hom (CategoryTheory.CategoryStruct.comp (D.t' j i k) (CategoryTheory.Limits.pullbackSymmetry (D.f i k) (D.f i j)).hom)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (D.f i j) (D.f i k))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j k : D.J<GOAL>CategoryTheory.CategoryStruct.comp (D.t' j k i) (D.t' k i j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (D.f j k) (D.f j i)).hom (CategoryTheory.CategoryStruct.comp (D.t' j i k) (CategoryTheory.Limits.pullbackSymmetry (D.f i k) (D.f i j)).hom)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<GOAL>D.diagram.L = (D.J × D.J)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<GOAL>D.diagram.R = D.J
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j : D.J<GOAL>D.diagram.fstFrom (i, j) = i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j : D.J<GOAL>D.diagram.sndFrom (i, j) = j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : CategoryTheory.GlueData C<VAR>i j : D.J<GOAL>D.diagram.fst (i, j) = D.f i j