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>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<VAR>CategoryTheory.Limits.PreservesFiniteColimits F<GOAL>(CategoryTheory.ExactFunctor.forget C D).obj (CategoryTheory.ExactFunctor.of F) = F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>CategoryTheory.Limits.HasBinaryProducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasPushouts C<GOAL>CategoryTheory.Limits.HasBinaryCoproducts C
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : CategoryTheory.Functor J (CategoryTheory.Functor K TypeMax)<VAR>k : K<VAR>t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<VAR>x : t.pt.obj k<GOAL>∃ j y, x = (t.ι.app j).app k y
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : CategoryTheory.Functor J (CategoryTheory.Functor K TypeMax)<VAR>k : K<VAR>x : (CategoryTheory.Limits.colimit F).obj k<GOAL>∃ j y, x = (CategoryTheory.Limits.colimit.ι F j).app k y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>(CategoryTheory.forget C).Corepresentable<VAR>J : Type w<VAR>CategoryTheory.Category.{t, w} J<VAR>G : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit G<GOAL>Small.{v, max v w} ↑(G ⋙ CategoryTheory.forget C).sections
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{t, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)<VAR>D : CategoryTheory.Limits.Cone F<VAR>hD : CategoryTheory.Limits.IsLimit D<GOAL>Function.Injective fun x j => (D.π.app j) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{t, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)<VAR>D : CategoryTheory.Limits.Cone F<VAR>hD : CategoryTheory.Limits.IsLimit D<VAR>x y : (CategoryTheory.forget C).obj D.pt<GOAL>(∀ (j : J), (D.π.app j) x = (D.π.app j) y) → x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{t, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasLimit F<VAR>x y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.limit F)<GOAL>(∀ (j : J), (CategoryTheory.Limits.limit.π F j) x = (CategoryTheory.Limits.limit.π F j) y) → x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape ℕᵒᵖ (CategoryTheory.forget C)<VAR>F : ℕᵒᵖ ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>hF : ∀ (n : ℕ), Function.Surjective ⇑(F.map (CategoryTheory.homOfLE ⋯).op)<GOAL>Function.Surjective ⇑(c.π.app (Opposite.op 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{r, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)<VAR>D : CategoryTheory.Limits.Cocone F<VAR>hD : CategoryTheory.Limits.IsColimit D<GOAL>let ff := fun a => (D.ι.app a.fst) a.snd;
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{r, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)<VAR>D : CategoryTheory.Limits.Cocone F<VAR>hD : CategoryTheory.Limits.IsColimit D<VAR>x : (CategoryTheory.forget C).obj D.pt<GOAL>∃ j y, (D.ι.app j) y = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{r, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.HasColimit F<VAR>x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.colimit F)<GOAL>∃ j y, (CategoryTheory.Limits.colimit.ι F j) y = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{r, w} J<VAR>F : J ⥤ C<VAR>D : CategoryTheory.Limits.Cocone F<VAR>i j : J<VAR>x : (CategoryTheory.forget C).obj (F.obj i)<VAR>y : (CategoryTheory.forget C).obj (F.obj j)<VAR>h : ∃ k f g, (F.map f) x = (F.map g) y<GOAL>(D.ι.app i) x = (D.ι.app j) y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{r, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i j : J<VAR>x : (CategoryTheory.forget C).obj (F.obj i)<VAR>y : (CategoryTheory.forget C).obj (F.obj j)<VAR>h : ∃ k f g, (F.map f) x = (F.map g) y<GOAL>(CategoryTheory.Limits.colimit.ι F i) x = (CategoryTheory.Limits.colimit.ι F j) y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{r, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)<VAR>CategoryTheory.IsFiltered J<VAR>D : CategoryTheory.Limits.Cocone F<VAR>i j : J<VAR>hD : CategoryTheory.Limits.IsColimit D<VAR>x : (CategoryTheory.forget C).obj (F.obj i)<VAR>y : (CategoryTheory.forget C).obj (F.obj j)<VAR>h : (D.ι.app i) x = (D.ι.app j) y<GOAL>∃ k f g, (F.map f) x = (F.map g) y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{r, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)<VAR>CategoryTheory.IsFiltered J<VAR>D : CategoryTheory.Limits.Cocone F<VAR>i j : J<VAR>hD : CategoryTheory.Limits.IsColimit D<VAR>x : (CategoryTheory.forget C).obj (F.obj i)<VAR>y : (CategoryTheory.forget C).obj (F.obj j)<GOAL>(D.ι.app i) x = (D.ι.app j) y ↔ ∃ k f g, (F.map f) x = (F.map g) y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{r, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)<VAR>CategoryTheory.IsFiltered J<VAR>CategoryTheory.Limits.HasColimit F<VAR>i j : J<VAR>x : (CategoryTheory.forget C).obj (F.obj i)<VAR>y : (CategoryTheory.forget C).obj (F.obj j)<VAR>h : (CategoryTheory.Limits.colimit.ι F i) x = (CategoryTheory.Limits.colimit.ι F j) y<GOAL>∃ k f g, (F.map f) x = (F.map g) y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>CategoryTheory.Category.{r, w} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)<VAR>CategoryTheory.IsFiltered J<VAR>CategoryTheory.Limits.HasColimit F<VAR>i j : J<VAR>x : (CategoryTheory.forget C).obj (F.obj i)<VAR>y : (CategoryTheory.forget C).obj (F.obj j)<GOAL>(CategoryTheory.Limits.colimit.ι F i) x = (CategoryTheory.Limits.colimit.ι F j) y ↔ ∃ k f g, (F.map f) x = (F.map g) y
<VAR>I : Type v₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type v₁<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ ((i : I) → C i)<VAR>∀ (i : I), CategoryTheory.Limits.HasLimit (F ⋙ CategoryTheory.Pi.eval C i)<GOAL>CategoryTheory.Limits.HasLimit F
<VAR>I : Type v₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type v₁<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ ((i : I) → C i)<VAR>∀ (i : I), CategoryTheory.Limits.HasColimit (F ⋙ CategoryTheory.Pi.eval C i)<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>b : CategoryTheory.Limits.Bicone f<VAR>i : b.IsBilimit<GOAL>∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>b : CategoryTheory.Limits.Bicone f<VAR>total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt<GOAL>CategoryTheory.Limits.HasBiproduct f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Finite J<VAR>f : J → C<VAR>CategoryTheory.Limits.HasProduct f<GOAL>CategoryTheory.Limits.HasBiproduct f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Finite J<VAR>f : J → C<VAR>CategoryTheory.Limits.HasCoproduct f<GOAL>CategoryTheory.Limits.HasBiproduct f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteProducts C<GOAL>CategoryTheory.Limits.HasFiniteBiproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.Limits.HasFiniteBiproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<GOAL>∑ j : J, CategoryTheory.Limits.biproduct.π f j ≫ CategoryTheory.Limits.biproduct.ι f j = 𝟙 (⨁ f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>T : C<VAR>g : (j : J) → T ⟶ f j<GOAL>CategoryTheory.Limits.biproduct.lift g = ∑ j : J, g j ≫ CategoryTheory.Limits.biproduct.ι f j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>T : C<VAR>g : (j : J) → f j ⟶ T<GOAL>CategoryTheory.Limits.biproduct.desc g = ∑ j : J, CategoryTheory.Limits.biproduct.π f j ≫ g j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>T U : C<VAR>g : (j : J) → T ⟶ f j<VAR>h : (j : J) → f j ⟶ U<GOAL>CategoryTheory.Limits.biproduct.lift g ≫ CategoryTheory.Limits.biproduct.desc h = ∑ j : J, g j ≫ h j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Fintype J<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f g : J → C<VAR>h : (j : J) → f j ⟶ g j<GOAL>CategoryTheory.Limits.biproduct.map h = ∑ j : J, CategoryTheory.Limits.biproduct.π f j ≫ h j ≫ CategoryTheory.Limits.biproduct.ι g j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : Type<VAR>Fintype J<VAR>K : Type<VAR>Finite K<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : J → C<VAR>g : K → C<VAR>P : C<VAR>x : (j : J) → P ⟶ f j<VAR>m : (j : J) → (k : K) → f j ⟶ g k<GOAL>CategoryTheory.Limits.biproduct.lift x ≫ CategoryTheory.Limits.biproduct.matrix m = CategoryTheory.Limits.biproduct.lift fun k => ∑ j : J, x j ≫ m j k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J K : Type<VAR>Finite J<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>Fintype K<VAR>f : J → C<VAR>g : K → C<VAR>m : (j : J) → (k : K) → f j ⟶ g k<VAR>P : C<VAR>x : (k : K) → g k ⟶ P<GOAL>CategoryTheory.Limits.biproduct.matrix m ≫ CategoryTheory.Limits.biproduct.desc x = CategoryTheory.Limits.biproduct.desc fun j => ∑ k : K, m j k ≫ x k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J K : Type<VAR>Finite J<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>Finite K<VAR>f : J → C<VAR>g h : K → C<VAR>m : (j : J) → (k : K) → f j ⟶ g k<VAR>n : (k : K) → g k ⟶ h k<GOAL>CategoryTheory.Limits.biproduct.matrix m ≫ CategoryTheory.Limits.biproduct.map n = CategoryTheory.Limits.biproduct.matrix fun j k => m j k ≫ n k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J K : Type<VAR>Finite J<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>Finite K<VAR>f g : J → C<VAR>h : K → C<VAR>m : (k : J) → f k ⟶ g k<VAR>n : (j : J) → (k : K) → g j ⟶ h k<GOAL>CategoryTheory.Limits.biproduct.map m ≫ CategoryTheory.Limits.biproduct.matrix n = CategoryTheory.Limits.biproduct.matrix fun j k => m j ≫ n j k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>β γ : Type<VAR>Finite β<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (f ∘ ⇑ε)<GOAL>(CategoryTheory.Limits.biproduct.reindex ε f).hom = CategoryTheory.Limits.biproduct.desc fun b => CategoryTheory.Limits.biproduct.ι f (ε b)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>β γ : Type<VAR>Finite β<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (f ∘ ⇑ε)<GOAL>(CategoryTheory.Limits.biproduct.reindex ε f).inv = CategoryTheory.Limits.biproduct.lift fun b => CategoryTheory.Limits.biproduct.π f (ε b)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>i : b.IsBilimit<GOAL>b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>b : CategoryTheory.Limits.BinaryBicone X Y<VAR>total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt<GOAL>CategoryTheory.Limits.HasBinaryBiproduct X Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).inr = ht.lift (CategoryTheory.Limits.BinaryFan.mk 0 (𝟙 Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).fst = t.π.app { as := CategoryTheory.Limits.WalkingPair.left }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).pt = t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).inl = ht.lift (CategoryTheory.Limits.BinaryFan.mk (𝟙 X) 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).snd = t.π.app { as := CategoryTheory.Limits.WalkingPair.right }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.BinaryBicone X Y<VAR>ht : CategoryTheory.Limits.IsLimit t.toCone<GOAL>t.inl = ht.lift (CategoryTheory.Limits.BinaryFan.mk (𝟙 X) 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.BinaryBicone X Y<VAR>ht : CategoryTheory.Limits.IsLimit t.toCone<GOAL>t.inr = ht.lift (CategoryTheory.Limits.BinaryFan.mk 0 (𝟙 Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<GOAL>CategoryTheory.Limits.HasBinaryBiproduct X Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>CategoryTheory.Limits.HasBinaryBiproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsColimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).pt = t.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsColimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).snd = ht.desc (CategoryTheory.Limits.BinaryCofan.mk 0 (𝟙 Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsColimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).inr = t.ι.app { as := CategoryTheory.Limits.WalkingPair.right }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsColimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).fst = ht.desc (CategoryTheory.Limits.BinaryCofan.mk (𝟙 X) 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)<VAR>ht : CategoryTheory.Limits.IsColimit t<GOAL>(CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).inl = t.ι.app { as := CategoryTheory.Limits.WalkingPair.left }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.BinaryBicone X Y<VAR>ht : CategoryTheory.Limits.IsColimit t.toCocone<GOAL>t.fst = ht.desc (CategoryTheory.Limits.BinaryCofan.mk (𝟙 X) 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.BinaryBicone X Y<VAR>ht : CategoryTheory.Limits.IsColimit t.toCocone<GOAL>t.snd = ht.desc (CategoryTheory.Limits.BinaryCofan.mk 0 (𝟙 Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<GOAL>CategoryTheory.Limits.HasBinaryBiproduct X Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<GOAL>CategoryTheory.Limits.HasBinaryBiproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.biprod.fst ≫ CategoryTheory.Limits.biprod.inl + CategoryTheory.Limits.biprod.snd ≫ CategoryTheory.Limits.biprod.inr = 𝟙 (X ⊞ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>T : C<VAR>f : T ⟶ X<VAR>g : T ⟶ Y<GOAL>CategoryTheory.Limits.biprod.lift f g = f ≫ CategoryTheory.Limits.biprod.inl + g ≫ CategoryTheory.Limits.biprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<GOAL>CategoryTheory.Limits.biprod.desc f g = CategoryTheory.Limits.biprod.fst ≫ f + CategoryTheory.Limits.biprod.snd ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>T U : C<VAR>f : T ⟶ X<VAR>g : T ⟶ Y<VAR>h : X ⟶ U<VAR>i : Y ⟶ U<GOAL>CategoryTheory.Limits.biprod.lift f g ≫ CategoryTheory.Limits.biprod.desc h i = f ≫ h + g ≫ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>CategoryTheory.Limits.biprod.map f g = CategoryTheory.Limits.biprod.fst ≫ f ≫ CategoryTheory.Limits.biprod.inl + CategoryTheory.Limits.biprod.snd ≫ g ≫ CategoryTheory.Limits.biprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>i : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).pt = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>i : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).fst = CategoryTheory.retraction f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>i : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).inr = let c' := CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c) ⋯; let i' := CategoryTheory.Limits.isCokernelEpiComp i (CategoryTheory.retraction f) ⋯; let i'' := CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork i'; (CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>i : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).snd = CategoryTheory.Limits.Cofork.π c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>i : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).inl = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitEpi f<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>i : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).pt = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitEpi f<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>i : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).inr = CategoryTheory.section_ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitEpi f<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>i : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).snd = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitEpi f<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>i : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).inl = CategoryTheory.Limits.Fork.ι c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitEpi f<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>i : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).fst = let c' := CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.Fork.ι c) ⋯; let i' := CategoryTheory.Limits.isKernelCompMono i (CategoryTheory.section_ f) ⋯; let i'' := CategoryTheory.Preadditive.isLimitForkOfKernelFork i'; (CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasBinaryBiproduct X X<GOAL>f + g = CategoryTheory.Limits.biprod.lift (𝟙 X) (𝟙 X) ≫ CategoryTheory.Limits.biprod.desc f g