ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>self : CategoryTheory.Limits.BinaryBicone P Q<GOAL>self.inr ≫ self.snd = 𝟙 Q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>self : CategoryTheory.Limits.BinaryBicone P Q<GOAL>self.inr ≫ self.fst = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>self : CategoryTheory.Limits.BinaryBicone P Q<GOAL>self.inl ≫ self.fst = 𝟙 P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>self : CategoryTheory.Limits.BinaryBicone P Q<GOAL>self.inl ≫ self.snd = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>A B : CategoryTheory.Limits.BinaryBicone P Q<VAR>self : CategoryTheory.Limits.BinaryBiconeMorphism A B<GOAL>self.hom ≫ B.fst = A.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>A B : CategoryTheory.Limits.BinaryBicone P Q<VAR>self : CategoryTheory.Limits.BinaryBiconeMorphism A B<GOAL>self.hom ≫ B.snd = A.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>A B : CategoryTheory.Limits.BinaryBicone P Q<VAR>self : CategoryTheory.Limits.BinaryBiconeMorphism A B<GOAL>A.inr ≫ self.hom = B.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>A B : CategoryTheory.Limits.BinaryBicone P Q<VAR>self : CategoryTheory.Limits.BinaryBiconeMorphism A B<GOAL>A.inl ≫ self.hom = B.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<GOAL>∀ {X Y Z : CategoryTheory.Limits.BinaryBicone P Q} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g).hom = f.hom ≫ g.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>B : CategoryTheory.Limits.BinaryBicone P Q<GOAL>(𝟙 B).hom = 𝟙 B.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c c' : CategoryTheory.Limits.BinaryBicone P Q<VAR>f g : c ⟶ c'<VAR>w : f.hom = g.hom<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c c' : CategoryTheory.Limits.BinaryBicone P Q<VAR>φ : c.pt ≅ c'.pt<VAR>winl : c.inl ≫ φ.hom = c'.inl := by aesop_cat<VAR>winr : c.inr ≫ φ.hom = c'.inr := by aesop_cat<VAR>wfst : φ.hom ≫ c'.fst = c.fst := by aesop_cat<VAR>wsnd : φ.hom ≫ c'.snd = c.snd := by aesop_cat<GOAL>(CategoryTheory.Limits.BinaryBicones.ext φ winl winr wfst wsnd).hom.hom = φ.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c c' : CategoryTheory.Limits.BinaryBicone P Q<VAR>φ : c.pt ≅ c'.pt<VAR>winl : c.inl ≫ φ.hom = c'.inl := by aesop_cat<VAR>winr : c.inr ≫ φ.hom = c'.inr := by aesop_cat<VAR>wfst : φ.hom ≫ c'.fst = c.fst := by aesop_cat<VAR>wsnd : φ.hom ≫ c'.snd = c.snd := by aesop_cat<GOAL>(CategoryTheory.Limits.BinaryBicones.ext φ winl winr wfst wsnd).inv.hom = φ.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>A : CategoryTheory.Limits.BinaryBicone P Q<GOAL>((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).fst = F.map A.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>A : CategoryTheory.Limits.BinaryBicone P Q<GOAL>((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).snd = F.map A.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<GOAL>∀ {X Y : CategoryTheory.Limits.BinaryBicone P Q} (f : X ⟶ Y), ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).map f).hom = F.map f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>A : CategoryTheory.Limits.BinaryBicone P Q<GOAL>((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).inr = F.map A.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>A : CategoryTheory.Limits.BinaryBicone P Q<GOAL>((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).inl = F.map A.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>A : CategoryTheory.Limits.BinaryBicone P Q<GOAL>((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).pt = F.obj A.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>c.toCone.pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>c.toCone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = c.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>c.toCone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = c.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>CategoryTheory.Limits.BinaryFan.fst c.toCone = c.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>CategoryTheory.Limits.BinaryFan.snd c.toCone = c.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>c.toCocone.pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>c.toCocone.ι.app { as := CategoryTheory.Limits.WalkingPair.left } = c.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>c.toCocone.ι.app { as := CategoryTheory.Limits.WalkingPair.right } = c.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>CategoryTheory.Limits.BinaryCofan.inl c.toCocone = c.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>c : CategoryTheory.Limits.BinaryBicone P Q<GOAL>CategoryTheory.Limits.BinaryCofan.inr c.toCocone = c.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<GOAL>∀ {X_1 Y_1 : CategoryTheory.Limits.BinaryBicone X Y} (f : X_1 ⟶ Y_1), (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.map f).hom = f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>j : CategoryTheory.Limits.WalkingPair<GOAL>(CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).ι j = CategoryTheory.Limits.WalkingPair.casesOn j b.inl b.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>j : CategoryTheory.Limits.WalkingPair<GOAL>(CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).π j = CategoryTheory.Limits.WalkingPair.casesOn j b.fst b.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<GOAL>(CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).pt = b.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)<GOAL>(CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).pt = b.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)<GOAL>(CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).inr = b.ι CategoryTheory.Limits.WalkingPair.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)<GOAL>(CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).inl = b.ι CategoryTheory.Limits.WalkingPair.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<GOAL>∀ {X_1 Y_1 : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)} (f : X_1 ⟶ Y_1), (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.map f).hom = f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)<GOAL>(CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).snd = b.π CategoryTheory.Limits.WalkingPair.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)<GOAL>(CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).fst = b.π CategoryTheory.Limits.WalkingPair.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>self : CategoryTheory.Limits.HasBinaryBiproduct P Q<GOAL>Nonempty (CategoryTheory.Limits.BinaryBiproductData P Q)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>P Q : C<VAR>d : CategoryTheory.Limits.BinaryBiproductData P Q<GOAL>CategoryTheory.Limits.HasBinaryBiproduct P Q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>self : CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q : C<GOAL>CategoryTheory.Limits.HasBinaryBiproduct P Q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<GOAL>CategoryTheory.Limits.HasBinaryBiproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>(CategoryTheory.Limits.BinaryBiproduct.bicone X Y).fst = CategoryTheory.Limits.biprod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>(CategoryTheory.Limits.BinaryBiproduct.bicone X Y).snd = CategoryTheory.Limits.biprod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>(CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inl = CategoryTheory.Limits.biprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>(CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inr = CategoryTheory.Limits.biprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.biprod.inl ≫ CategoryTheory.Limits.biprod.fst = 𝟙 X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.biprod.inl ≫ CategoryTheory.Limits.biprod.snd = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.biprod.inr ≫ CategoryTheory.Limits.biprod.fst = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.biprod.inr ≫ CategoryTheory.Limits.biprod.snd = 𝟙 Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<GOAL>CategoryTheory.Limits.biprod.lift f g ≫ CategoryTheory.Limits.biprod.fst = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<GOAL>CategoryTheory.Limits.biprod.lift f g ≫ CategoryTheory.Limits.biprod.snd = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>f : X ⟶ W<VAR>g : Y ⟶ W<GOAL>CategoryTheory.Limits.biprod.inl ≫ CategoryTheory.Limits.biprod.desc f g = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>f : X ⟶ W<VAR>g : Y ⟶ W<GOAL>CategoryTheory.Limits.biprod.inr ≫ CategoryTheory.Limits.biprod.desc f g = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>f g : Z ⟶ X ⊞ Y<VAR>h₀ : f ≫ CategoryTheory.Limits.biprod.fst = g ≫ CategoryTheory.Limits.biprod.fst<VAR>h₁ : f ≫ CategoryTheory.Limits.biprod.snd = g ≫ CategoryTheory.Limits.biprod.snd<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>f g : X ⊞ Y ⟶ Z<VAR>h₀ : CategoryTheory.Limits.biprod.inl ≫ f = CategoryTheory.Limits.biprod.inl ≫ g<VAR>h₁ : CategoryTheory.Limits.biprod.inr ≫ f = CategoryTheory.Limits.biprod.inr ≫ g<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>(CategoryTheory.Limits.biprod.isoProd X Y).hom = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>(CategoryTheory.Limits.biprod.isoProd X Y).inv = CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>(CategoryTheory.Limits.biprod.isoCoprod X Y).inv = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>(CategoryTheory.Limits.biprod.isoCoprod X Y).hom = CategoryTheory.Limits.biprod.desc CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct W X<VAR>CategoryTheory.Limits.HasBinaryBiproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.biprod.map f g = CategoryTheory.Limits.biprod.map' f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct W X<VAR>CategoryTheory.Limits.HasBinaryBiproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.biprod.map f g ≫ CategoryTheory.Limits.biprod.fst = CategoryTheory.Limits.biprod.fst ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct W X<VAR>CategoryTheory.Limits.HasBinaryBiproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.biprod.map f g ≫ CategoryTheory.Limits.biprod.snd = CategoryTheory.Limits.biprod.snd ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct W X<VAR>CategoryTheory.Limits.HasBinaryBiproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.biprod.inl ≫ CategoryTheory.Limits.biprod.map f g = f ≫ CategoryTheory.Limits.biprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct W X<VAR>CategoryTheory.Limits.HasBinaryBiproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.biprod.inr ≫ CategoryTheory.Limits.biprod.map f g = g ≫ CategoryTheory.Limits.biprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct W X<VAR>CategoryTheory.Limits.HasBinaryBiproduct Y Z<VAR>f : W ≅ Y<VAR>g : X ≅ Z<GOAL>(CategoryTheory.Limits.biprod.mapIso f g).inv = CategoryTheory.Limits.biprod.map f.inv g.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>W X Y Z : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct W X<VAR>CategoryTheory.Limits.HasBinaryBiproduct Y Z<VAR>f : W ≅ Y<VAR>g : X ≅ Z<GOAL>(CategoryTheory.Limits.biprod.mapIso f g).hom = CategoryTheory.Limits.biprod.map f.hom g.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>(hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)).hom = CategoryTheory.Limits.biprod.lift b.fst b.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>(hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)).inv = CategoryTheory.Limits.biprod.desc b.inl b.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>(CategoryTheory.Limits.biprod.uniqueUpToIso X Y hb).hom = CategoryTheory.Limits.biprod.lift b.fst b.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>(CategoryTheory.Limits.biprod.uniqueUpToIso X Y hb).inv = CategoryTheory.Limits.biprod.desc b.inl b.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.IsIso CategoryTheory.Limits.biprod.inl ↔ 𝟙 (X ⊞ Y) = CategoryTheory.Limits.biprod.fst ≫ CategoryTheory.Limits.biprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>c : CategoryTheory.Limits.BinaryBicone X Y<GOAL>CategoryTheory.Limits.Fork.ι c.fstKernelFork = c.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>c : CategoryTheory.Limits.BinaryBicone X Y<GOAL>CategoryTheory.Limits.Fork.ι c.sndKernelFork = c.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>c : CategoryTheory.Limits.BinaryBicone X Y<GOAL>CategoryTheory.Limits.Cofork.π c.inlCokernelCofork = c.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>c : CategoryTheory.Limits.BinaryBicone X Y<GOAL>CategoryTheory.Limits.Cofork.π c.inrCokernelCofork = c.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.biprod.fstKernelFork X Y) = CategoryTheory.Limits.biprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.biprod.sndKernelFork X Y) = CategoryTheory.Limits.biprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.biprod.inlCokernelCofork X Y) = CategoryTheory.Limits.biprod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.biprod.inrCokernelCofork X Y) = CategoryTheory.Limits.biprod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.kernelBiprodFstIso.inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.fst 0) (CategoryTheory.Limits.biprod.fstKernelFork X Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.kernelBiprodFstIso.hom = (CategoryTheory.Limits.biprod.isKernelFstKernelFork X Y).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.fst 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.kernelBiprodSndIso.hom = (CategoryTheory.Limits.biprod.isKernelSndKernelFork X Y).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.snd 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.kernelBiprodSndIso.inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.snd 0) (CategoryTheory.Limits.biprod.sndKernelFork X Y)