ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>j j' : J<VAR>h : j ≠ j'<GOAL>CategoryTheory.Limits.biproduct.ι f j ≫ CategoryTheory.Limits.biproduct.π f j' = 0
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>j j' : J<VAR>w : j = j'<GOAL>CategoryTheory.eqToHom ⋯ ≫ CategoryTheory.Limits.biproduct.ι f j' = CategoryTheory.Limits.biproduct.ι f j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>j j' : J<VAR>w : j = j'<GOAL>CategoryTheory.Limits.biproduct.π f j ≫ CategoryTheory.eqToHom ⋯ = CategoryTheory.Limits.biproduct.π f j'
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>P : C<VAR>p : (b : J) → P ⟶ f b<VAR>j : J<GOAL>CategoryTheory.Limits.biproduct.lift p ≫ CategoryTheory.Limits.biproduct.π f j = p j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>P : C<VAR>p : (b : J) → f b ⟶ P<VAR>j : J<GOAL>CategoryTheory.Limits.biproduct.ι f j ≫ CategoryTheory.Limits.biproduct.desc p = p j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>Z : C<VAR>g h : Z ⟶ ⨁ f<VAR>w : ∀ (j : J), g ≫ CategoryTheory.Limits.biproduct.π f j = h ≫ CategoryTheory.Limits.biproduct.π f j<GOAL>g = h
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>Z : C<VAR>g h : ⨁ f ⟶ Z<VAR>w : ∀ (j : J), CategoryTheory.Limits.biproduct.ι f j ≫ g = CategoryTheory.Limits.biproduct.ι f j ≫ h<GOAL>g = h
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<GOAL>(CategoryTheory.Limits.biproduct.isoProduct f).hom = CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π f)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<GOAL>(CategoryTheory.Limits.biproduct.isoProduct f).inv = CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.Pi.π f)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<GOAL>(CategoryTheory.Limits.biproduct.isoCoproduct f).inv = CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.biproduct.ι f)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<GOAL>(CategoryTheory.Limits.biproduct.isoCoproduct f).hom = CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.Sigma.ι f)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f g : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<VAR>p : (b : J) → f b ⟶ g b<GOAL>CategoryTheory.Limits.biproduct.map p = CategoryTheory.Limits.biproduct.map' p
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f g : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<VAR>p : (j : J) → f j ⟶ g j<VAR>j : J<GOAL>CategoryTheory.Limits.biproduct.map p ≫ CategoryTheory.Limits.biproduct.π g j = CategoryTheory.Limits.biproduct.π f j ≫ p j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f g : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<VAR>p : (j : J) → f j ⟶ g j<VAR>j : J<GOAL>CategoryTheory.Limits.biproduct.ι f j ≫ CategoryTheory.Limits.biproduct.map p = p j ≫ CategoryTheory.Limits.biproduct.ι g j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f g : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<VAR>p : (j : J) → f j ⟶ g j<VAR>P : C<VAR>k : (j : J) → g j ⟶ P<GOAL>CategoryTheory.Limits.biproduct.map p ≫ CategoryTheory.Limits.biproduct.desc k = CategoryTheory.Limits.biproduct.desc fun j => p j ≫ k j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f g : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<VAR>P : C<VAR>k : (j : J) → P ⟶ f j<VAR>p : (j : J) → f j ⟶ g j<GOAL>CategoryTheory.Limits.biproduct.lift k ≫ CategoryTheory.Limits.biproduct.map p = CategoryTheory.Limits.biproduct.lift fun j => k j ≫ p j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f g : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<VAR>p : (b : J) → f b ≅ g b<GOAL>(CategoryTheory.Limits.biproduct.mapIso p).inv = CategoryTheory.Limits.biproduct.map fun b => (p b).inv
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f g : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<VAR>p : (b : J) → f b ≅ g b<GOAL>(CategoryTheory.Limits.biproduct.mapIso p).hom = CategoryTheory.Limits.biproduct.map fun b => (p b).hom
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<GOAL>(CategoryTheory.Limits.biproduct.whiskerEquiv e w).hom = CategoryTheory.Limits.biproduct.desc fun j => (w j).inv ≫ CategoryTheory.Limits.biproduct.ι g (e j)
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<GOAL>(CategoryTheory.Limits.biproduct.whiskerEquiv e w).inv = CategoryTheory.Limits.biproduct.desc fun k => CategoryTheory.eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ CategoryTheory.Limits.biproduct.ι f (e.symm k)
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<GOAL>(CategoryTheory.Limits.biproduct.whiskerEquiv e w).hom = CategoryTheory.Limits.biproduct.lift fun k => CategoryTheory.Limits.biproduct.π f (e.symm k) ≫ (w (e.symm k)).inv ≫ CategoryTheory.eqToHom ⋯
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct g<GOAL>(CategoryTheory.Limits.biproduct.whiskerEquiv e w).inv = CategoryTheory.Limits.biproduct.lift fun j => CategoryTheory.Limits.biproduct.π g (e j) ≫ (w j).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_3<VAR>f : ι → Type u_2<VAR>g : (i : ι) → f i → C<VAR>∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)<VAR>CategoryTheory.Limits.HasBiproduct fun i => ⨁ g i<GOAL>(CategoryTheory.Limits.biproductBiproductIso f g).inv = CategoryTheory.Limits.biproduct.lift fun i => CategoryTheory.Limits.biproduct.lift fun x => CategoryTheory.Limits.biproduct.π (fun p => g p.fst p.snd) ⟨i, x⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>ι : Type u_3<VAR>f : ι → Type u_2<VAR>g : (i : ι) → f i → C<VAR>∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)<VAR>CategoryTheory.Limits.HasBiproduct fun i => ⨁ g i<GOAL>(CategoryTheory.Limits.biproductBiproductIso f g).hom = CategoryTheory.Limits.biproduct.lift fun x => match x with | ⟨i, x⟩ => CategoryTheory.Limits.biproduct.π (fun i => ⨁ g i) i ≫ CategoryTheory.Limits.biproduct.π (g i) x
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<VAR>DecidablePred p<VAR>j : J<GOAL>CategoryTheory.Limits.biproduct.fromSubtype f p ≫ CategoryTheory.Limits.biproduct.π f j = if h : p j then CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<VAR>DecidablePred p<GOAL>CategoryTheory.Limits.biproduct.fromSubtype f p = CategoryTheory.Limits.biproduct.lift fun j => if h : p j then CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<VAR>j : Subtype p<GOAL>CategoryTheory.Limits.biproduct.fromSubtype f p ≫ CategoryTheory.Limits.biproduct.π f ↑j = CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<VAR>j : Subtype p<GOAL>CategoryTheory.Limits.biproduct.toSubtype f p ≫ CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j = CategoryTheory.Limits.biproduct.π f ↑j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<VAR>DecidablePred p<VAR>j : J<GOAL>CategoryTheory.Limits.biproduct.ι f j ≫ CategoryTheory.Limits.biproduct.toSubtype f p = if h : p j then CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<VAR>DecidablePred p<GOAL>CategoryTheory.Limits.biproduct.toSubtype f p = CategoryTheory.Limits.biproduct.desc fun j => if h : p j then CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<VAR>j : Subtype p<GOAL>CategoryTheory.Limits.biproduct.ι f ↑j ≫ CategoryTheory.Limits.biproduct.toSubtype f p = CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<VAR>j : Subtype p<GOAL>CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j ≫ CategoryTheory.Limits.biproduct.fromSubtype f p = CategoryTheory.Limits.biproduct.ι f ↑j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<GOAL>CategoryTheory.Limits.biproduct.fromSubtype f p ≫ CategoryTheory.Limits.biproduct.toSubtype f p = 𝟙 (⨁ Subtype.restrict p f)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>p : J → Prop<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)<VAR>DecidablePred p<GOAL>CategoryTheory.Limits.biproduct.toSubtype f p ≫ CategoryTheory.Limits.biproduct.fromSubtype f p = CategoryTheory.Limits.biproduct.map fun j => if p j then 𝟙 (f j) else 0
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>i : J<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)<GOAL>(CategoryTheory.Limits.kernelBiproductπIso f i).hom = (CategoryTheory.Limits.biproduct.isLimitFromSubtype f i).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.π f i) 0))
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>i : J<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)<GOAL>(CategoryTheory.Limits.kernelBiproductπIso f i).inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.π f i) 0) (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f fun j => ¬j = i) ⋯)
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>i : J<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)<GOAL>(CategoryTheory.Limits.cokernelBiproductιIso f i).inv = (CategoryTheory.Limits.biproduct.isColimitToSubtype f i).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.ι f i) 0))
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>i : J<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)<GOAL>(CategoryTheory.Limits.cokernelBiproductιIso f i).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.ι f i) 0) (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f fun j => ¬j = i) ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type<VAR>Finite K<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<GOAL>(CategoryTheory.Limits.kernelForkBiproductToSubtype f p).isLimit = CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯ (fun {W} g x => g ≫ CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type<VAR>Finite K<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<GOAL>(CategoryTheory.Limits.kernelForkBiproductToSubtype f p).cone = CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type<VAR>Finite K<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<GOAL>(CategoryTheory.Limits.kernelBiproductToSubtypeIso f p).hom = (CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯ (fun {W} g x => g ≫ CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯ ⋯).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type<VAR>Finite K<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<GOAL>(CategoryTheory.Limits.kernelBiproductToSubtypeIso f p).inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0) (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type<VAR>Finite K<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<GOAL>(CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p).isColimit = CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯ (fun {W} g x => CategoryTheory.Limits.biproduct.fromSubtype f pᶜ ≫ g) ⋯ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type<VAR>Finite K<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<GOAL>(CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p).cocone = CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type<VAR>Finite K<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<GOAL>(CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p).inv = (CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯ (fun {W} g x => CategoryTheory.Limits.biproduct.fromSubtype f pᶜ ≫ g) ⋯ ⋯).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : Type<VAR>Finite K<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<GOAL>(CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0) (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯)
<VAR>J : Type<VAR>Finite J<VAR>K : Type<VAR>Finite K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : J → C<VAR>g : K → C<VAR>m : (j : J) → (k : K) → f j ⟶ g k<VAR>k : K<GOAL>CategoryTheory.Limits.biproduct.matrix m ≫ CategoryTheory.Limits.biproduct.π g k = CategoryTheory.Limits.biproduct.desc fun j => m j k
<VAR>J : Type<VAR>Finite J<VAR>K : Type<VAR>Finite K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : J → C<VAR>g : K → C<VAR>m : (j : J) → (k : K) → f j ⟶ g k<VAR>j : J<GOAL>CategoryTheory.Limits.biproduct.ι f j ≫ CategoryTheory.Limits.biproduct.matrix m = CategoryTheory.Limits.biproduct.lift fun k => m j k
<VAR>J : Type<VAR>Finite J<VAR>K : Type<VAR>Finite K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : J → C<VAR>g : K → C<VAR>m : (j : J) → (k : K) → f j ⟶ g k<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.biproduct.components (CategoryTheory.Limits.biproduct.matrix m) j k = m j k
<VAR>J : Type<VAR>Finite J<VAR>K : Type<VAR>Finite K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : J → C<VAR>g : K → C<VAR>m : ⨁ f ⟶ ⨁ g<GOAL>(CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.Limits.biproduct.components m j k) = m
<VAR>J : Type<VAR>Finite J<VAR>K : Type<VAR>Finite K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : J → C<VAR>g : K → C<VAR>m : (j : J) → (k : K) → f j ⟶ g k<GOAL>CategoryTheory.Limits.biproduct.matrixEquiv.symm m = CategoryTheory.Limits.biproduct.matrix m
<VAR>J : Type<VAR>Finite J<VAR>K : Type<VAR>Finite K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>f : J → C<VAR>g : K → C<VAR>m : ⨁ f ⟶ ⨁ g<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.biproduct.matrixEquiv m j k = CategoryTheory.Limits.biproduct.components m j k
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>b : CategoryTheory.Limits.Bicone f<VAR>hb : b.IsBilimit<GOAL>(hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).hom = CategoryTheory.Limits.biproduct.lift b.π
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>b : CategoryTheory.Limits.Bicone f<VAR>hb : b.IsBilimit<GOAL>(hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).inv = CategoryTheory.Limits.biproduct.desc b.ι
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>b : CategoryTheory.Limits.Bicone f<VAR>hb : b.IsBilimit<GOAL>(CategoryTheory.Limits.biproduct.uniqueUpToIso f hb).hom = CategoryTheory.Limits.biproduct.lift b.π
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>b : CategoryTheory.Limits.Bicone f<VAR>hb : b.IsBilimit<GOAL>(CategoryTheory.Limits.biproduct.uniqueUpToIso f hb).inv = CategoryTheory.Limits.biproduct.desc b.ι
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Unique J<VAR>f : J → C<VAR>j : J<GOAL>(CategoryTheory.Limits.limitBiconeOfUnique f).bicone.π j = CategoryTheory.eqToHom ⋯
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Unique J<VAR>f : J → C<GOAL>(CategoryTheory.Limits.limitBiconeOfUnique f).bicone.pt = f default
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Unique J<VAR>f : J → C<GOAL>(CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isLimit = (CategoryTheory.Limits.limitConeOfUnique f).isLimit
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Unique J<VAR>f : J → C<GOAL>(CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isColimit = (CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Unique J<VAR>f : J → C<VAR>j : J<GOAL>(CategoryTheory.Limits.limitBiconeOfUnique f).bicone.ι j = CategoryTheory.eqToHom ⋯
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Unique J<VAR>f : J → C<GOAL>(CategoryTheory.Limits.biproductUniqueIso f).hom = CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.ι
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Unique J<VAR>f : J → C<GOAL>(CategoryTheory.Limits.biproductUniqueIso f).inv = CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.π