ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>i : CategoryTheory.Limits.IsZero X<GOAL>CategoryTheory.Limits.IsZero Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>t : CategoryTheory.Limits.IsInitial X<GOAL>(CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial t).hom = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>t : CategoryTheory.Limits.IsInitial X<GOAL>(CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial t).inv = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>t : CategoryTheory.Limits.IsTerminal X<GOAL>(CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal t).hom = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>t : CategoryTheory.Limits.IsTerminal X<GOAL>(CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal t).inv = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasInitial C<GOAL>CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.hom = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasInitial C<GOAL>CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.inv = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.hom = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.inv = 0
<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>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>hF : CategoryTheory.Limits.IsZero F<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.map f = 0
<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>X : C<GOAL>CategoryTheory.Limits.IsZero ((CategoryTheory.Functor.toPrefunctor 0).obj X)
<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>CategoryTheory.Limits.HasZeroMorphisms D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Functor.toPrefunctor 0).map f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>𝟙 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>f : X ⟶ 0<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : Y ≅ 0<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>f : 0 ⟶ X<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : X ≅ 0<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : CategoryTheory.IsIsomorphic X 0<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : CategoryTheory.IsIsomorphic Y 0<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : X ≅ 0<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : Y ≅ 0<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>h : 𝟙 X = 0<GOAL>((CategoryTheory.Limits.idZeroEquivIsoZero X) h).hom = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>h : 𝟙 X = 0<GOAL>((CategoryTheory.Limits.idZeroEquivIsoZero X) h).inv = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>h : CategoryTheory.Mono 0<GOAL>(CategoryTheory.Limits.isoZeroOfMonoZero h).hom = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>h : CategoryTheory.Mono 0<GOAL>(CategoryTheory.Limits.isoZeroOfMonoZero h).inv = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>h : CategoryTheory.Epi 0<GOAL>(CategoryTheory.Limits.isoZeroOfEpiZero h).inv = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>h : CategoryTheory.Epi 0<GOAL>(CategoryTheory.Limits.isoZeroOfEpiZero h).hom = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>i : CategoryTheory.IsIso 0<GOAL>⋯ = ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>h : 𝟙 X = 0 ∧ 𝟙 Y = 0<GOAL>⋯ = ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : X ≅ 0<VAR>j : Y ≅ 0<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasInitial C<GOAL>CategoryTheory.Limits.HasZeroObject C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>CategoryTheory.Limits.HasZeroObject C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasImage f<VAR>CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)<VAR>h : f ≫ g = 0<GOAL>CategoryTheory.Limits.image.ι f ≫ g = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasImage g<VAR>h : f ≫ g = 0<GOAL>f ≫ CategoryTheory.Limits.factorThruImage g = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<GOAL>(CategoryTheory.Limits.monoFactorisationZero X Y).m = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<GOAL>(CategoryTheory.Limits.monoFactorisationZero X Y).e = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<GOAL>(CategoryTheory.Limits.monoFactorisationZero X Y).I = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasImage 0<GOAL>CategoryTheory.Limits.image.ι 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : f = 0<VAR>CategoryTheory.Limits.HasImage f<GOAL>CategoryTheory.Limits.image.ι f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>F : D ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>hF : CategoryTheory.Limits.IsZero F<GOAL>CategoryTheory.Limits.IsZero c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>F : D ⥤ C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hF : CategoryTheory.Limits.IsZero F<GOAL>CategoryTheory.Limits.IsZero c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>hX : CategoryTheory.Limits.IsTerminal X<GOAL>CategoryTheory.Limits.IsZero X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>hX : CategoryTheory.Limits.IsInitial X<GOAL>CategoryTheory.Limits.IsZero X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>self : CategoryTheory.Limits.HasCountableLimits C<VAR>J : Type<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.CountableCategory J<GOAL>CategoryTheory.Limits.HasLimitsOfShape J C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>self : CategoryTheory.Limits.HasCountableColimits C<VAR>J : Type<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.CountableCategory J<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C
<VAR>J : Type u_2<VAR>Countable J<VAR>Preorder J<VAR>CategoryTheory.IsCofiltered J<GOAL>Antitone (CategoryTheory.Limits.sequentialFunctor_obj J)
<VAR>J : Type u_2<VAR>Countable J<VAR>Preorder J<VAR>CategoryTheory.IsCofiltered J<VAR>j : J<GOAL>∃ n, CategoryTheory.Limits.sequentialFunctor_obj J n ≤ j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.RegularMono f<GOAL>CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.left = CategoryTheory.CategoryStruct.comp f CategoryTheory.RegularMono.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.RegularMono f<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.RegularEpi f<GOAL>CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.left f = CategoryTheory.CategoryStruct.comp CategoryTheory.RegularEpi.right f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.RegularEpi f<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.IsIso f
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>P : C<VAR>p : (b : β) → P ⟶ f b<VAR>X : CategoryTheory.Discrete β<GOAL>(CategoryTheory.Limits.Fan.mk P p).π.app X = p X.as
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>P : C<VAR>p : (b : β) → P ⟶ f b<GOAL>(CategoryTheory.Limits.Fan.mk P p).pt = P
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>P : C<VAR>p : (b : β) → f b ⟶ P<GOAL>(CategoryTheory.Limits.Cofan.mk P p).pt = P
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>P : C<VAR>p : (b : β) → f b ⟶ P<VAR>X : CategoryTheory.Discrete β<GOAL>(CategoryTheory.Limits.Cofan.mk P p).ι.app X = p X.as
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>P : C<VAR>p : (b : β) → P ⟶ f b<VAR>j : β<GOAL>(CategoryTheory.Limits.Fan.mk P p).proj j = p j
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>P : C<VAR>p : (b : β) → f b ⟶ P<VAR>j : β<GOAL>(CategoryTheory.Limits.Cofan.mk P p).inj j = p j
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>e : β ≃ α<VAR>iso : (j : β) → g j ≅ f (e j)<GOAL>CategoryTheory.Limits.HasCoproduct g
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>e : β ≃ α<VAR>iso : (j : β) → g j ≅ f (e j)<GOAL>CategoryTheory.Limits.HasProduct g
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>t : CategoryTheory.Limits.Fan f<VAR>lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt<VAR>fac : ∀ (s : CategoryTheory.Limits.Fan f) (j : β), lift s ≫ t.proj j = s.proj j := by aesop_cat<VAR>uniq : ∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), m ≫ t.proj j = s.proj j) → m = lift s := by aesop_cat<VAR>s : CategoryTheory.Limits.Fan f<GOAL>(CategoryTheory.Limits.mkFanLimit t lift fac uniq).lift s = lift s
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : β → C<VAR>c : CategoryTheory.Limits.Fan F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>A : C<VAR>f : (i : β) → A ⟶ F i<VAR>i : β<GOAL>CategoryTheory.Limits.Fan.IsLimit.desc hc f ≫ c.proj i = f i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type u_1<VAR>F : I → C<VAR>c : CategoryTheory.Limits.Fan F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>A : C<VAR>f g : A ⟶ c.pt<VAR>h : ∀ (i : I), f ≫ c.proj i = g ≫ c.proj i<GOAL>f = g
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>s : CategoryTheory.Limits.Cofan f<VAR>desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt<VAR>fac : ∀ (t : CategoryTheory.Limits.Cofan f) (j : β), s.inj j ≫ desc t = t.inj j := by aesop_cat<VAR>uniq : ∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), s.inj j ≫ m = t.inj j) → m = desc t := by aesop_cat<VAR>t : CategoryTheory.Limits.Cofan f<GOAL>(CategoryTheory.Limits.mkCofanColimit s desc fac uniq).desc t = desc t
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : β → C<VAR>c : CategoryTheory.Limits.Cofan F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>A : C<VAR>f : (i : β) → F i ⟶ A<VAR>i : β<GOAL>c.inj i ≫ CategoryTheory.Limits.Cofan.IsColimit.desc hc f = f i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type u_1<VAR>F : I → C<VAR>c : CategoryTheory.Limits.Cofan F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>A : C<VAR>f g : c.pt ⟶ A<VAR>h : ∀ (i : I), c.inj i ≫ f = c.inj i ≫ g<GOAL>f = g
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>X : C<VAR>g₁ g₂ : X ⟶ ∏ᶜ f<VAR>h : ∀ (b : β), g₁ ≫ CategoryTheory.Limits.Pi.π f b = g₂ ≫ CategoryTheory.Limits.Pi.π f b<GOAL>g₁ = g₂
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>X : C<VAR>g₁ g₂ : ∐ f ⟶ X<VAR>h : ∀ (b : β), CategoryTheory.Limits.Sigma.ι f b ≫ g₁ = CategoryTheory.Limits.Sigma.ι f b ≫ g₂<GOAL>g₁ = g₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u_1<VAR>f : J → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>j j' : J<VAR>w : j = j'<GOAL>CategoryTheory.Limits.Pi.π f j ≫ CategoryTheory.eqToHom ⋯ = CategoryTheory.Limits.Pi.π f j'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u_1<VAR>f : J → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>j j' : J<VAR>w : j = j'<GOAL>CategoryTheory.eqToHom ⋯ ≫ CategoryTheory.Limits.Sigma.ι f j' = CategoryTheory.Limits.Sigma.ι f j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type w<VAR>f : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>P : C<VAR>p : (b : β) → P ⟶ f b<VAR>b : β<GOAL>CategoryTheory.Limits.Pi.lift p ≫ CategoryTheory.Limits.Pi.π f b = p b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type w<VAR>f : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>P : C<VAR>p : (b : β) → f b ⟶ P<VAR>b : β<GOAL>CategoryTheory.Limits.Sigma.ι f b ≫ CategoryTheory.Limits.Sigma.desc p = p b
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>c₁ c₂ : CategoryTheory.Limits.Cofan f<VAR>e : c₁.pt ≅ c₂.pt<VAR>w : ∀ (b : β), c₁.inj b ≫ e.hom = c₂.inj b := by aesop_cat<GOAL>(CategoryTheory.Limits.Cofan.ext e w).inv.hom = e.inv
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>c₁ c₂ : CategoryTheory.Limits.Cofan f<VAR>e : c₁.pt ≅ c₂.pt<VAR>w : ∀ (b : β), c₁.inj b ≫ e.hom = c₂.inj b := by aesop_cat<GOAL>(CategoryTheory.Limits.Cofan.ext e w).hom.hom = e.hom
<VAR>β : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>c : CategoryTheory.Limits.Cofan f<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj) ↔ Nonempty (CategoryTheory.Limits.IsColimit c)
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>CategoryTheory.Limits.HasProduct f<GOAL>(CategoryTheory.Limits.Pi.map fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f)
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g h : α → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct g<VAR>CategoryTheory.Limits.HasProduct h<VAR>q : (a : α) → f a ⟶ g a<VAR>q' : (a : α) → g a ⟶ h a<GOAL>CategoryTheory.Limits.Pi.map q ≫ CategoryTheory.Limits.Pi.map q' = CategoryTheory.Limits.Pi.map fun a => q a ≫ q' a
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct g<VAR>p : β → α<VAR>q : (b : β) → f (p b) ⟶ g b<VAR>b : β<GOAL>CategoryTheory.Limits.Pi.map' p q ≫ CategoryTheory.Limits.Pi.π g b = CategoryTheory.Limits.Pi.π f (p b) ≫ q b
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>CategoryTheory.Limits.HasProduct f<GOAL>(CategoryTheory.Limits.Pi.map' id fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f)
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : α → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct g<VAR>p : (b : α) → f b ⟶ g b<GOAL>CategoryTheory.Limits.Pi.map' id p = CategoryTheory.Limits.Pi.map p
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g : β → C<VAR>h : γ → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct g<VAR>CategoryTheory.Limits.HasProduct h<VAR>p : β → α<VAR>p' : γ → β<VAR>q : (b : β) → f (p b) ⟶ g b<VAR>q' : (c : γ) → g (p' c) ⟶ h c<GOAL>CategoryTheory.Limits.Pi.map' p q ≫ CategoryTheory.Limits.Pi.map' p' q' = CategoryTheory.Limits.Pi.map' (p ∘ p') fun c => q (p' c) ≫ q' c
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g h : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct g<VAR>CategoryTheory.Limits.HasProduct h<VAR>p : β → α<VAR>q : (b : β) → f (p b) ⟶ g b<VAR>q' : (b : β) → g b ⟶ h b<GOAL>CategoryTheory.Limits.Pi.map' p q ≫ CategoryTheory.Limits.Pi.map q' = CategoryTheory.Limits.Pi.map' p fun b => q b ≫ q' b
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : α → C<VAR>h : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct g<VAR>CategoryTheory.Limits.HasProduct h<VAR>p : β → α<VAR>q : (a : α) → f a ⟶ g a<VAR>q' : (b : β) → g (p b) ⟶ h b<GOAL>CategoryTheory.Limits.Pi.map q ≫ CategoryTheory.Limits.Pi.map' p q' = CategoryTheory.Limits.Pi.map' p fun b => q (p b) ≫ q' b
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>CategoryTheory.Limits.HasProduct g<VAR>p p' : β → α<VAR>q : (b : β) → f (p b) ⟶ g b<VAR>q' : (b : β) → f (p' b) ⟶ g b<VAR>hp : p = p'<VAR>hq : ∀ (b : β), CategoryTheory.eqToHom ⋯ ≫ q b = q' b<GOAL>CategoryTheory.Limits.Pi.map' p q = CategoryTheory.Limits.Pi.map' p' q'
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Discrete α ⥤ C<VAR>CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }<GOAL>(CategoryTheory.Limits.Pi.cone X).pt = ∏ᶜ fun j => X.obj { as := j }
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Discrete α ⥤ C<VAR>CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }<GOAL>(CategoryTheory.Limits.Pi.cone X).π = CategoryTheory.Discrete.natTrans fun x => CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) x.as
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Discrete α ⥤ C<VAR>CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }<VAR>CategoryTheory.Limits.HasLimit X<VAR>j : α<GOAL>(CategoryTheory.Limits.Pi.isoLimit X).inv ≫ CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j = CategoryTheory.Limits.limit.π X { as := j }
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Discrete α ⥤ C<VAR>CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }<VAR>CategoryTheory.Limits.HasLimit X<VAR>j : α<GOAL>(CategoryTheory.Limits.Pi.isoLimit X).hom ≫ CategoryTheory.Limits.limit.π X { as := j } = CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>CategoryTheory.Limits.HasCoproduct f<GOAL>(CategoryTheory.Limits.Sigma.map fun a => 𝟙 (f a)) = 𝟙 (∐ f)
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g h : α → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct g<VAR>CategoryTheory.Limits.HasCoproduct h<VAR>q : (a : α) → f a ⟶ g a<VAR>q' : (a : α) → g a ⟶ h a<GOAL>CategoryTheory.Limits.Sigma.map q ≫ CategoryTheory.Limits.Sigma.map q' = CategoryTheory.Limits.Sigma.map fun a => q a ≫ q' a
<VAR>β : Type w<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct g<VAR>p : α → β<VAR>q : (a : α) → f a ⟶ g (p a)<VAR>a : α<GOAL>CategoryTheory.Limits.Sigma.ι f a ≫ CategoryTheory.Limits.Sigma.map' p q = q a ≫ CategoryTheory.Limits.Sigma.ι g (p a)
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>CategoryTheory.Limits.HasCoproduct f<GOAL>(CategoryTheory.Limits.Sigma.map' id fun a => 𝟙 (f a)) = 𝟙 (∐ f)
<VAR>α : Type w₂<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : α → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct g<VAR>p : (b : α) → f b ⟶ g b<GOAL>CategoryTheory.Limits.Sigma.map' id p = CategoryTheory.Limits.Sigma.map p
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : α → C<VAR>g : β → C<VAR>h : γ → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>CategoryTheory.Limits.HasCoproduct g<VAR>CategoryTheory.Limits.HasCoproduct h<VAR>p : α → β<VAR>p' : β → γ<VAR>q : (a : α) → f a ⟶ g (p a)<VAR>q' : (b : β) → g b ⟶ h (p' b)<GOAL>CategoryTheory.Limits.Sigma.map' p q ≫ CategoryTheory.Limits.Sigma.map' p' q' = CategoryTheory.Limits.Sigma.map' (p' ∘ p) fun a => q a ≫ q' (p a)