ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.PreservesBinaryBiproduct X Y F<VAR>W : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<GOAL>F.map (CategoryTheory.Limits.biprod.lift f g) ≫ (F.mapBiprod X Y).hom = CategoryTheory.Limits.biprod.lift (F.map f) (F.map g)
<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.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.PreservesBinaryBiproduct X Y F<VAR>W : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<GOAL>CategoryTheory.Limits.biprod.lift (F.map f) (F.map g) ≫ (F.mapBiprod X Y).inv = F.map (CategoryTheory.Limits.biprod.lift 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.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.PreservesBinaryBiproduct X Y F<VAR>W : C<VAR>f : X ⟶ W<VAR>g : Y ⟶ W<GOAL>(F.mapBiprod X Y).inv ≫ F.map (CategoryTheory.Limits.biprod.desc f g) = CategoryTheory.Limits.biprod.desc (F.map f) (F.map g)
<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.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.PreservesBinaryBiproduct X Y F<VAR>W : C<VAR>f : X ⟶ W<VAR>g : Y ⟶ W<GOAL>(F.mapBiprod X Y).hom ≫ CategoryTheory.Limits.biprod.desc (F.map f) (F.map g) = F.map (CategoryTheory.Limits.biprod.desc f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>f g : CategoryTheory.Over X<VAR>h : f ⟶ g<VAR>CategoryTheory.Epi h<GOAL>CategoryTheory.Epi h.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>f g : CategoryTheory.Over X<VAR>h : f ⟶ g<GOAL>CategoryTheory.Epi h ↔ CategoryTheory.Epi h.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>f g : CategoryTheory.Under X<VAR>h : f ⟶ g<VAR>CategoryTheory.Mono h<GOAL>CategoryTheory.Mono h.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>f g : CategoryTheory.Under X<VAR>h : f ⟶ g<GOAL>CategoryTheory.Mono h ↔ CategoryTheory.Mono h.right
<GOAL>CategoryTheory.Limits.WalkingPair.swap CategoryTheory.Limits.WalkingPair.left = CategoryTheory.Limits.WalkingPair.right
<GOAL>CategoryTheory.Limits.WalkingPair.swap CategoryTheory.Limits.WalkingPair.right = CategoryTheory.Limits.WalkingPair.left
<GOAL>CategoryTheory.Limits.WalkingPair.swap.symm CategoryTheory.Limits.WalkingPair.left = CategoryTheory.Limits.WalkingPair.right
<GOAL>CategoryTheory.Limits.WalkingPair.swap.symm CategoryTheory.Limits.WalkingPair.right = CategoryTheory.Limits.WalkingPair.left
<GOAL>CategoryTheory.Limits.WalkingPair.equivBool CategoryTheory.Limits.WalkingPair.left = true
<GOAL>CategoryTheory.Limits.WalkingPair.equivBool CategoryTheory.Limits.WalkingPair.right = false
<GOAL>CategoryTheory.Limits.WalkingPair.equivBool.symm true = CategoryTheory.Limits.WalkingPair.left
<GOAL>CategoryTheory.Limits.WalkingPair.equivBool.symm false = CategoryTheory.Limits.WalkingPair.right
<VAR>C : Type u<VAR>X Y : C<GOAL>CategoryTheory.Limits.pairFunction X Y CategoryTheory.Limits.WalkingPair.left = X
<VAR>C : Type u<VAR>X Y : C<GOAL>CategoryTheory.Limits.pairFunction X Y CategoryTheory.Limits.WalkingPair.right = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<GOAL>(CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<GOAL>(CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair ⥤ C<VAR>f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left }<VAR>g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.right }<GOAL>(CategoryTheory.Limits.mapPair f g).app { as := CategoryTheory.Limits.WalkingPair.left } = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair ⥤ C<VAR>f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left }<VAR>g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.right }<GOAL>(CategoryTheory.Limits.mapPair f g).app { as := CategoryTheory.Limits.WalkingPair.right } = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair ⥤ C<VAR>f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.left }<VAR>g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.right }<VAR>X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair<GOAL>(CategoryTheory.Limits.mapPairIso f g).hom.app X = (CategoryTheory.Limits.WalkingPair.rec f g X.as).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair ⥤ C<VAR>f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.left }<VAR>g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.right }<VAR>X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair<GOAL>(CategoryTheory.Limits.mapPairIso f g).inv.app X = (CategoryTheory.Limits.WalkingPair.rec f g X.as).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair ⥤ C<VAR>X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair<GOAL>(CategoryTheory.Limits.diagramIsoPair F).hom.app X = (CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.right })) X.as).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair ⥤ C<VAR>X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair<GOAL>(CategoryTheory.Limits.diagramIsoPair F).inv.app X = (CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.right })) X.as).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>s : CategoryTheory.Limits.BinaryFan X Y<GOAL>s.π.app { as := CategoryTheory.Limits.WalkingPair.left } = s.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>s : CategoryTheory.Limits.BinaryFan X Y<GOAL>s.π.app { as := CategoryTheory.Limits.WalkingPair.right } = s.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>s : CategoryTheory.Limits.BinaryFan X Y<VAR>h : CategoryTheory.Limits.IsLimit s<VAR>f g : W ⟶ s.pt<VAR>h₁ : f ≫ s.fst = g ≫ s.fst<VAR>h₂ : f ≫ s.snd = g ≫ s.snd<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>s : CategoryTheory.Limits.BinaryCofan X Y<GOAL>s.ι.app { as := CategoryTheory.Limits.WalkingPair.left } = s.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>s : CategoryTheory.Limits.BinaryCofan X Y<GOAL>s.ι.app { as := CategoryTheory.Limits.WalkingPair.right } = s.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>s : CategoryTheory.Limits.BinaryCofan X Y<VAR>h : CategoryTheory.Limits.IsColimit s<VAR>f g : s.pt ⟶ W<VAR>h₁ : s.inl ≫ f = s.inl ≫ g<VAR>h₂ : s.inr ≫ f = s.inr ≫ g<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y P : C<VAR>π₁ : P ⟶ X<VAR>π₂ : P ⟶ Y<GOAL>(CategoryTheory.Limits.BinaryFan.mk π₁ π₂).pt = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y P : C<VAR>ι₁ : X ⟶ P<VAR>ι₂ : Y ⟶ P<GOAL>(CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).pt = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y P : C<VAR>π₁ : P ⟶ X<VAR>π₂ : P ⟶ Y<GOAL>(CategoryTheory.Limits.BinaryFan.mk π₁ π₂).fst = π₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y P : C<VAR>π₁ : P ⟶ X<VAR>π₂ : P ⟶ Y<GOAL>(CategoryTheory.Limits.BinaryFan.mk π₁ π₂).snd = π₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y P : C<VAR>ι₁ : X ⟶ P<VAR>ι₂ : Y ⟶ P<GOAL>(CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).inl = ι₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y P : C<VAR>ι₁ : X ⟶ P<VAR>ι₂ : Y ⟶ P<GOAL>(CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).inr = ι₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>s : CategoryTheory.Limits.BinaryFan X Y<VAR>h : CategoryTheory.Limits.IsLimit s<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<GOAL>↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' h f g) = h.lift (CategoryTheory.Limits.BinaryFan.mk f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>s : CategoryTheory.Limits.BinaryCofan X Y<VAR>h : CategoryTheory.Limits.IsColimit s<VAR>f : X ⟶ W<VAR>g : Y ⟶ W<GOAL>↑(CategoryTheory.Limits.BinaryCofan.IsColimit.desc' h f g) = h.desc (CategoryTheory.Limits.BinaryCofan.mk f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>h : CategoryTheory.Limits.IsTerminal Y<VAR>c : CategoryTheory.Limits.BinaryFan X Y<GOAL>Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>h : CategoryTheory.Limits.IsTerminal X<VAR>c : CategoryTheory.Limits.BinaryFan X Y<GOAL>Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>h : CategoryTheory.Limits.IsInitial Y<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<GOAL>Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>h : CategoryTheory.Limits.IsInitial X<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<GOAL>Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>f g : W ⟶ X ⨯ Y<VAR>h₁ : f ≫ CategoryTheory.Limits.prod.fst = g ≫ CategoryTheory.Limits.prod.fst<VAR>h₂ : f ≫ CategoryTheory.Limits.prod.snd = g ≫ CategoryTheory.Limits.prod.snd<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<VAR>f g : X ⨿ Y ⟶ W<VAR>h₁ : CategoryTheory.Limits.coprod.inl ≫ f = CategoryTheory.Limits.coprod.inl ≫ g<VAR>h₂ : CategoryTheory.Limits.coprod.inr ≫ f = CategoryTheory.Limits.coprod.inr ≫ g<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<GOAL>CategoryTheory.Limits.prod.lift f g ≫ CategoryTheory.Limits.prod.fst = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<GOAL>CategoryTheory.Limits.prod.lift f g ≫ CategoryTheory.Limits.prod.snd = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<VAR>f : X ⟶ W<VAR>g : Y ⟶ W<GOAL>CategoryTheory.Limits.coprod.inl ≫ CategoryTheory.Limits.coprod.desc f g = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<VAR>f : X ⟶ W<VAR>g : Y ⟶ W<GOAL>CategoryTheory.Limits.coprod.inr ≫ CategoryTheory.Limits.coprod.desc f g = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>V W X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>f : V ⟶ W<VAR>g : W ⟶ X<VAR>h : W ⟶ Y<GOAL>f ≫ CategoryTheory.Limits.prod.lift g h = CategoryTheory.Limits.prod.lift (f ≫ g) (f ≫ h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct Y Y<VAR>f : X ⟶ Y<GOAL>f ≫ CategoryTheory.Limits.diag Y = CategoryTheory.Limits.prod.lift f f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryProduct W X<VAR>CategoryTheory.Limits.HasBinaryProduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.prod.map f g ≫ CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.prod.fst ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryProduct W X<VAR>CategoryTheory.Limits.HasBinaryProduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.prod.map f g ≫ CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.prod.snd ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<GOAL>CategoryTheory.Limits.prod.map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨯ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<GOAL>CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd = 𝟙 (X ⨯ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>V W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryProduct W X<VAR>CategoryTheory.Limits.HasBinaryProduct Y Z<VAR>f : V ⟶ W<VAR>g : V ⟶ X<VAR>h : W ⟶ Y<VAR>k : X ⟶ Z<GOAL>CategoryTheory.Limits.prod.lift f g ≫ CategoryTheory.Limits.prod.map h k = CategoryTheory.Limits.prod.lift (f ≫ h) (g ≫ k)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryProduct W Y<VAR>CategoryTheory.Limits.HasBinaryProduct X Z<VAR>g : W ⟶ X<VAR>g' : Y ⟶ Z<GOAL>CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.fst ≫ g) (CategoryTheory.Limits.prod.snd ≫ g') = CategoryTheory.Limits.prod.map g g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A₁ A₂ A₃ B₁ B₂ B₃ : C<VAR>CategoryTheory.Limits.HasBinaryProduct A₁ B₁<VAR>CategoryTheory.Limits.HasBinaryProduct A₂ B₂<VAR>CategoryTheory.Limits.HasBinaryProduct A₃ B₃<VAR>f : A₁ ⟶ A₂<VAR>g : B₁ ⟶ B₂<VAR>h : A₂ ⟶ A₃<VAR>k : B₂ ⟶ B₃<GOAL>CategoryTheory.Limits.prod.map f g ≫ CategoryTheory.Limits.prod.map h k = CategoryTheory.Limits.prod.map (f ≫ h) (g ≫ k)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B X Y : C<VAR>f : A ⟶ B<VAR>g : X ⟶ Y<VAR>CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C<GOAL>CategoryTheory.Limits.prod.map (𝟙 X) f ≫ CategoryTheory.Limits.prod.map g (𝟙 B) = CategoryTheory.Limits.prod.map g (𝟙 A) ≫ CategoryTheory.Limits.prod.map (𝟙 Y) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z W : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasBinaryProduct X W<VAR>CategoryTheory.Limits.HasBinaryProduct Z W<VAR>CategoryTheory.Limits.HasBinaryProduct Y W<GOAL>CategoryTheory.Limits.prod.map (f ≫ g) (𝟙 W) = CategoryTheory.Limits.prod.map f (𝟙 W) ≫ CategoryTheory.Limits.prod.map g (𝟙 W)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z W : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasBinaryProduct W X<VAR>CategoryTheory.Limits.HasBinaryProduct W Y<VAR>CategoryTheory.Limits.HasBinaryProduct W Z<GOAL>CategoryTheory.Limits.prod.map (𝟙 W) (f ≫ g) = CategoryTheory.Limits.prod.map (𝟙 W) f ≫ CategoryTheory.Limits.prod.map (𝟙 W) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryProduct W X<VAR>CategoryTheory.Limits.HasBinaryProduct Y Z<VAR>f : W ≅ Y<VAR>g : X ≅ Z<GOAL>(CategoryTheory.Limits.prod.mapIso f g).inv = CategoryTheory.Limits.prod.map f.inv g.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryProduct W X<VAR>CategoryTheory.Limits.HasBinaryProduct Y Z<VAR>f : W ≅ Y<VAR>g : X ≅ Z<GOAL>(CategoryTheory.Limits.prod.mapIso f g).hom = CategoryTheory.Limits.prod.map f.hom g.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasBinaryProduct X X<VAR>CategoryTheory.Limits.HasBinaryProduct Y Y<GOAL>CategoryTheory.Limits.diag X ≫ CategoryTheory.Limits.prod.map f f = f ≫ CategoryTheory.Limits.diag Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>CategoryTheory.Limits.HasBinaryProduct (X ⨯ Y) (X ⨯ Y)<GOAL>CategoryTheory.Limits.diag (X ⨯ Y) ≫ CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd = 𝟙 (X ⨯ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C<VAR>X X' Y Y' : C<VAR>g : X ⟶ Y<VAR>g' : X' ⟶ Y'<GOAL>CategoryTheory.Limits.diag (X ⨯ X') ≫ CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.fst ≫ g) (CategoryTheory.Limits.prod.snd ≫ g') = CategoryTheory.Limits.prod.map g g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>V W X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<VAR>f : V ⟶ W<VAR>g : X ⟶ V<VAR>h : Y ⟶ V<GOAL>CategoryTheory.Limits.coprod.desc g h ≫ f = CategoryTheory.Limits.coprod.desc (g ≫ f) (h ≫ f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{u_1, u} C<VAR>V W X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<VAR>f : V ⟶ W<VAR>g : X ⟶ V<VAR>h : Y ⟶ V<VAR>Z : C<VAR>l : W ⟶ Z<GOAL>CategoryTheory.Limits.coprod.desc g h ≫ f ≫ l = CategoryTheory.Limits.coprod.desc (g ≫ f) (h ≫ f) ≫ l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X X<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.codiag X ≫ f = CategoryTheory.Limits.coprod.desc f f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct W X<VAR>CategoryTheory.Limits.HasBinaryCoproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.coprod.inl ≫ CategoryTheory.Limits.coprod.map f g = f ≫ CategoryTheory.Limits.coprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct W X<VAR>CategoryTheory.Limits.HasBinaryCoproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.coprod.inr ≫ CategoryTheory.Limits.coprod.map f g = g ≫ CategoryTheory.Limits.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<GOAL>CategoryTheory.Limits.coprod.map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨿ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<GOAL>CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr = 𝟙 (X ⨿ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>S T U V W : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct U W<VAR>CategoryTheory.Limits.HasBinaryCoproduct T V<VAR>f : U ⟶ S<VAR>g : W ⟶ S<VAR>h : T ⟶ U<VAR>k : V ⟶ W<GOAL>CategoryTheory.Limits.coprod.map h k ≫ CategoryTheory.Limits.coprod.desc f g = CategoryTheory.Limits.coprod.desc (h ≫ f) (k ≫ g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct W Y<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Z<VAR>g : W ⟶ X<VAR>g' : Y ⟶ Z<GOAL>CategoryTheory.Limits.coprod.desc (g ≫ CategoryTheory.Limits.coprod.inl) (g' ≫ CategoryTheory.Limits.coprod.inr) = CategoryTheory.Limits.coprod.map g g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A₁ A₂ A₃ B₁ B₂ B₃ : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct A₁ B₁<VAR>CategoryTheory.Limits.HasBinaryCoproduct A₂ B₂<VAR>CategoryTheory.Limits.HasBinaryCoproduct A₃ B₃<VAR>f : A₁ ⟶ A₂<VAR>g : B₁ ⟶ B₂<VAR>h : A₂ ⟶ A₃<VAR>k : B₂ ⟶ B₃<GOAL>CategoryTheory.Limits.coprod.map f g ≫ CategoryTheory.Limits.coprod.map h k = CategoryTheory.Limits.coprod.map (f ≫ h) (g ≫ k)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B X Y : C<VAR>f : A ⟶ B<VAR>g : X ⟶ Y<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C<GOAL>CategoryTheory.Limits.coprod.map (𝟙 X) f ≫ CategoryTheory.Limits.coprod.map g (𝟙 B) = CategoryTheory.Limits.coprod.map g (𝟙 A) ≫ CategoryTheory.Limits.coprod.map (𝟙 Y) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z W : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasBinaryCoproduct Z W<VAR>CategoryTheory.Limits.HasBinaryCoproduct Y W<VAR>CategoryTheory.Limits.HasBinaryCoproduct X W<GOAL>CategoryTheory.Limits.coprod.map (f ≫ g) (𝟙 W) = CategoryTheory.Limits.coprod.map f (𝟙 W) ≫ CategoryTheory.Limits.coprod.map g (𝟙 W)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z W : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasBinaryCoproduct W X<VAR>CategoryTheory.Limits.HasBinaryCoproduct W Y<VAR>CategoryTheory.Limits.HasBinaryCoproduct W Z<GOAL>CategoryTheory.Limits.coprod.map (𝟙 W) (f ≫ g) = CategoryTheory.Limits.coprod.map (𝟙 W) f ≫ CategoryTheory.Limits.coprod.map (𝟙 W) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct W X<VAR>CategoryTheory.Limits.HasBinaryCoproduct Y Z<VAR>f : W ≅ Y<VAR>g : X ≅ Z<GOAL>(CategoryTheory.Limits.coprod.mapIso f g).inv = CategoryTheory.Limits.coprod.map f.inv g.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct W X<VAR>CategoryTheory.Limits.HasBinaryCoproduct Y Z<VAR>f : W ≅ Y<VAR>g : X ≅ Z<GOAL>(CategoryTheory.Limits.coprod.mapIso f g).hom = CategoryTheory.Limits.coprod.map f.hom g.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasBinaryCoproduct X X<VAR>CategoryTheory.Limits.HasBinaryCoproduct Y Y<GOAL>CategoryTheory.Limits.coprod.map f f ≫ CategoryTheory.Limits.codiag Y = CategoryTheory.Limits.codiag X ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<VAR>CategoryTheory.Limits.HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)<GOAL>CategoryTheory.Limits.coprod.map CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr ≫ CategoryTheory.Limits.codiag (X ⨿ Y) = 𝟙 (X ⨿ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C<VAR>X X' Y Y' : C<VAR>g : X ⟶ Y<VAR>g' : X' ⟶ Y'<GOAL>CategoryTheory.Limits.coprod.map (g ≫ CategoryTheory.Limits.coprod.inl) (g' ≫ CategoryTheory.Limits.coprod.inr) ≫ CategoryTheory.Limits.codiag (Y ⨿ Y') = CategoryTheory.Limits.coprod.map g g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ {X Y : C}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)<GOAL>CategoryTheory.Limits.HasBinaryProducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ {X Y : C}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair X Y)<GOAL>CategoryTheory.Limits.HasBinaryCoproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>CategoryTheory.Limits.HasBinaryProduct P Q<VAR>CategoryTheory.Limits.HasBinaryProduct Q P<GOAL>(CategoryTheory.Limits.prod.braiding P Q).inv = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>CategoryTheory.Limits.HasBinaryProduct P Q<VAR>CategoryTheory.Limits.HasBinaryProduct Q P<GOAL>(CategoryTheory.Limits.prod.braiding P Q).hom = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst