ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iZ.hom<VAR>wg : iY.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingCospan.left = iX.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iZ.hom<VAR>wg : iY.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingCospan.right = iY.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iZ.hom<VAR>wg : iY.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingCospan.one = iZ.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iZ.hom<VAR>wg : iY.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingCospan.left = iX.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iZ.hom<VAR>wg : iY.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingCospan.right = iY.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iZ.hom<VAR>wg : iY.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingCospan.one = iZ.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iY.hom<VAR>wg : iX.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.left = iY
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iY.hom<VAR>wg : iX.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.right = iZ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iY.hom<VAR>wg : iX.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.zero = iX
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iY.hom<VAR>wg : iX.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.spanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingSpan.left = iY.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iY.hom<VAR>wg : iX.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.spanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingSpan.right = iZ.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iY.hom<VAR>wg : iX.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.spanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingSpan.zero = iX.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iY.hom<VAR>wg : iX.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.spanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingSpan.left = iY.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iY.hom<VAR>wg : iX.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.spanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingSpan.right = iZ.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iY.hom<VAR>wg : iX.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.spanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingSpan.zero = iX.inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)<VAR>h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), CategoryTheory.Zigzag (CategoryTheory.CostructuredArrow.mk i) (CategoryTheory.CostructuredArrow.mk j)<GOAL>(CategoryTheory.Limits.parallelPair f g).Initial
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)<VAR>h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = CategoryTheory.CategoryStruct.comp f a ∧ j = CategoryTheory.CategoryStruct.comp g a<GOAL>(CategoryTheory.Limits.parallelPair f g).Initial
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>self : CategoryTheory.Limits.IsZero X<VAR>Y : C<GOAL>Nonempty (Unique (Y ⟶ X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>self : CategoryTheory.Limits.IsZero X<VAR>Y : C<GOAL>Nonempty (Unique (X ⟶ Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>h : CategoryTheory.Limits.IsZero X<VAR>f : X ⟶ Y<GOAL>f = h.to_ Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>h : CategoryTheory.Limits.IsZero X<VAR>f : X ⟶ Y<GOAL>h.to_ Y = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>h : CategoryTheory.Limits.IsZero X<VAR>f : Y ⟶ X<GOAL>f = h.from_ Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>h : CategoryTheory.Limits.IsZero X<VAR>f : Y ⟶ X<GOAL>h.from_ Y = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>hX : CategoryTheory.Limits.IsZero X<VAR>f g : X ⟶ Y<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>hX : CategoryTheory.Limits.IsZero X<VAR>f g : Y ⟶ X<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>hY : CategoryTheory.Limits.IsZero Y<VAR>e : X ≅ Y<GOAL>CategoryTheory.Limits.IsZero X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>h : CategoryTheory.Limits.IsZero X<GOAL>CategoryTheory.Limits.IsZero (Opposite.op X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : Cᵒᵖ<VAR>h : CategoryTheory.Limits.IsZero X<GOAL>CategoryTheory.Limits.IsZero (Opposite.unop X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>e : X ≅ Y<GOAL>CategoryTheory.Limits.IsZero X ↔ CategoryTheory.Limits.IsZero Y
<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>hF : ∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)<GOAL>CategoryTheory.Limits.IsZero F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasZeroObject C<GOAL>∃ X, CategoryTheory.Limits.IsZero X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<GOAL>CategoryTheory.Limits.IsZero 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject Cᵒᵖ<GOAL>CategoryTheory.Limits.HasZeroObject C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>hX : CategoryTheory.Limits.IsZero X<GOAL>CategoryTheory.Limits.HasZeroObject C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>F : C ⥤ D<VAR>hF : CategoryTheory.Limits.IsZero F<VAR>X : C<GOAL>CategoryTheory.Limits.IsZero (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X : C<VAR>f g : X ⟶ 0<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X : C<VAR>f g : 0 ⟶ X<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>F : C ⥤ D<GOAL>CategoryTheory.Limits.IsZero F ↔ ∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor C (Type w)<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>Small.{w, u₁} I<VAR>F : CategoryTheory.Functor I A.Elements<VAR>i : I<GOAL>CategoryTheory.Limits.limit.π ((F.comp (CategoryTheory.CategoryOfElements.π A)).comp A) i (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement' F) = (F.obj i).snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor C (Type w)<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>Small.{w, u₁} I<VAR>F : CategoryTheory.Functor I A.Elements<VAR>CategoryTheory.Limits.HasLimitsOfShape I C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape I A<VAR>c : CategoryTheory.Limits.Cone F<GOAL>A.map (CategoryTheory.Limits.limit.lift (F.comp (CategoryTheory.CategoryOfElements.π A)) ((CategoryTheory.CategoryOfElements.π A).mapCone c)) c.pt.snd = CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor C (Type w)<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>Small.{w, u₁} I<VAR>F : CategoryTheory.Functor I A.Elements<VAR>CategoryTheory.Limits.HasLimitsOfShape I C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape I A<VAR>i : I<GOAL>A.map (CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.CategoryOfElements.π A)) i) (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F) = (F.obj i).snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor C (Type w)<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>Small.{w, u₁} I<VAR>F : CategoryTheory.Functor I A.Elements<VAR>CategoryTheory.Limits.HasLimitsOfShape I C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape I A<VAR>i : I<GOAL>↑((CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).π.app i) = CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.CategoryOfElements.π A)) i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor C (Type w)<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>Small.{w, u₁} I<VAR>F : CategoryTheory.Functor I A.Elements<VAR>CategoryTheory.Limits.HasLimitsOfShape I C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape I A<GOAL>(CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).pt.fst = CategoryTheory.Limits.limit (F.comp (CategoryTheory.CategoryOfElements.π A))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor C (Type w)<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>Small.{w, u₁} I<VAR>F : CategoryTheory.Functor I A.Elements<VAR>CategoryTheory.Limits.HasLimitsOfShape I C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape I A<GOAL>(CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).pt.snd = CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>s : CategoryTheory.CommSq f g h i<GOAL>s.cone.fst = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>s : CategoryTheory.CommSq f g h i<GOAL>s.cone.snd = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>s : CategoryTheory.CommSq f g h i<GOAL>s.cocone.inl = h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>s : CategoryTheory.CommSq f g h i<GOAL>s.cocone.inr = i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>self : CategoryTheory.IsPullback fst snd f g<GOAL>Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk fst snd ⋯))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>self : CategoryTheory.IsPushout f g inl inr<GOAL>Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr ⋯))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<GOAL>h.cone.fst = fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<GOAL>h.cone.snd = snd
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>hP : CategoryTheory.IsPullback fst snd f g<VAR>W : C<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>w : h ≫ f = k ≫ g<GOAL>hP.lift h k w ≫ fst = h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>hP : CategoryTheory.IsPullback fst snd f g<VAR>W : C<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>w : h ≫ f = k ≫ g<GOAL>hP.lift h k w ≫ snd = k
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>hP : CategoryTheory.IsPullback fst snd f g<VAR>W : C<VAR>k l : W ⟶ P<VAR>h₀ : k ≫ fst = l ≫ fst<VAR>h₁ : k ≫ snd = l ≫ snd<GOAL>k = l
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<VAR>h : CategoryTheory.Limits.IsLimit c<GOAL>CategoryTheory.IsPullback c.fst c.snd f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>w : CategoryTheory.CommSq fst snd f g<VAR>h : CategoryTheory.Limits.IsLimit w.cone<GOAL>CategoryTheory.IsPullback fst snd f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g) f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>c : CategoryTheory.Limits.BinaryFan X Y<VAR>h : CategoryTheory.Limits.IsLimit c<VAR>t : CategoryTheory.Limits.IsTerminal Z<GOAL>CategoryTheory.IsPullback c.fst c.snd (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd)<VAR>t : CategoryTheory.Limits.IsTerminal Z<GOAL>CategoryTheory.IsPullback fst snd (t.from X) (t.from Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd 0 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : C<VAR>X Y : C<VAR>Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>P' : C<VAR>fst' : P' ⟶ X<VAR>snd' : P' ⟶ Y<VAR>h : CategoryTheory.IsPullback fst snd f g<VAR>h' : CategoryTheory.IsPullback fst' snd' f g<GOAL>(CategoryTheory.IsPullback.isoIsPullback X Y h h').hom ≫ fst' = fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : C<VAR>X Y : C<VAR>Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>P' : C<VAR>fst' : P' ⟶ X<VAR>snd' : P' ⟶ Y<VAR>h : CategoryTheory.IsPullback fst snd f g<VAR>h' : CategoryTheory.IsPullback fst' snd' f g<GOAL>(CategoryTheory.IsPullback.isoIsPullback X Y h h').hom ≫ snd' = snd
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : C<VAR>X Y : C<VAR>Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>P' : C<VAR>fst' : P' ⟶ X<VAR>snd' : P' ⟶ Y<VAR>h : CategoryTheory.IsPullback fst snd f g<VAR>h' : CategoryTheory.IsPullback fst' snd' f g<GOAL>(CategoryTheory.IsPullback.isoIsPullback X Y h h').inv ≫ fst = fst'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : C<VAR>X Y : C<VAR>Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>P' : C<VAR>fst' : P' ⟶ X<VAR>snd' : P' ⟶ Y<VAR>h : CategoryTheory.IsPullback fst snd f g<VAR>h' : CategoryTheory.IsPullback fst' snd' f g<GOAL>(CategoryTheory.IsPullback.isoIsPullback X Y h h').inv ≫ snd = snd'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>h.isoPullback.hom ≫ CategoryTheory.Limits.pullback.fst f g = fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>h.isoPullback.hom ≫ CategoryTheory.Limits.pullback.snd f g = snd
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>h.isoPullback.inv ≫ fst = CategoryTheory.Limits.pullback.fst f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>h.isoPullback.inv ≫ snd = CategoryTheory.Limits.pullback.snd f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.CommSq fst snd f g<VAR>CategoryTheory.Limits.HasPullback f g<VAR>i : P ≅ CategoryTheory.Limits.pullback f g<VAR>w₁ : i.hom ≫ CategoryTheory.Limits.pullback.fst f g = fst<VAR>w₂ : i.hom ≫ CategoryTheory.Limits.pullback.snd f g = snd<GOAL>CategoryTheory.IsPullback fst snd f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso fst<VAR>CategoryTheory.IsIso g<VAR>sq : CategoryTheory.CommSq fst snd f g<GOAL>CategoryTheory.IsPullback fst snd f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : CategoryTheory.IsPullback fst snd f g<VAR>P' X' Y' Z' : C<VAR>fst' : P' ⟶ X'<VAR>snd' : P' ⟶ Y'<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>e₁ : P ≅ P'<VAR>e₂ : X ≅ X'<VAR>e₃ : Y ≅ Y'<VAR>e₄ : Z ≅ Z'<VAR>commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'<VAR>commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'<VAR>commf : f ≫ e₄.hom = e₂.hom ≫ f'<VAR>commg : g ≫ e₄.hom = e₃.hom ≫ g'<GOAL>CategoryTheory.IsPullback fst' snd' f' g'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<GOAL>h.cocone.inl = inl
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.IsPushout f g inl inr<GOAL>h.cocone.inr = inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>hP : CategoryTheory.IsPushout f g inl inr<VAR>W : C<VAR>h : X ⟶ W<VAR>k : Y ⟶ W<VAR>w : f ≫ h = g ≫ k<GOAL>inl ≫ hP.desc h k w = h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>hP : CategoryTheory.IsPushout f g inl inr<VAR>W : C<VAR>h : X ⟶ W<VAR>k : Y ⟶ W<VAR>w : f ≫ h = g ≫ k<GOAL>inr ≫ hP.desc h k w = k
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>hP : CategoryTheory.IsPushout f g inl inr<VAR>W : C<VAR>k l : P ⟶ W<VAR>h₀ : inl ≫ k = inl ≫ l<VAR>h₁ : inr ≫ k = inr ≫ l<GOAL>k = l
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>c : CategoryTheory.Limits.PushoutCocone f g<VAR>h : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsPushout f g c.inl c.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>w : CategoryTheory.CommSq f g inl inr<VAR>h : CategoryTheory.Limits.IsColimit w.cocone<GOAL>CategoryTheory.IsPushout f g inl inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.IsPushout f g (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.Limits.pushout.inr f g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y : C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<VAR>h : CategoryTheory.Limits.IsColimit c<VAR>t : CategoryTheory.Limits.IsInitial Z<GOAL>CategoryTheory.IsPushout (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr)<VAR>t : CategoryTheory.Limits.IsInitial Z<GOAL>CategoryTheory.IsPushout (t.to X) (t.to Y) inl inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<VAR>CategoryTheory.Limits.HasInitial C<GOAL>CategoryTheory.IsPushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>CategoryTheory.IsPushout 0 0 CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z : C<VAR>X Y : C<VAR>P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>P' : C<VAR>inl' : X ⟶ P'<VAR>inr' : Y ⟶ P'<VAR>h : CategoryTheory.IsPushout f g inl inr<VAR>h' : CategoryTheory.IsPushout f g inl' inr'<GOAL>inl ≫ (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom = inl'