ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>CategoryTheory.Limits.HasImageMap sq<GOAL>CategoryTheory.Limits.image.map sq ≫ CategoryTheory.Limits.image.ι g.hom = CategoryTheory.Limits.image.ι f.hom ≫ sq.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y P Q : C<VAR>k : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage k<VAR>l : P ⟶ Q<VAR>CategoryTheory.Limits.HasImage l<VAR>m : X ⟶ P<VAR>n : Y ⟶ Q<VAR>w : m ≫ l = k ≫ n<VAR>CategoryTheory.Limits.HasImageMap (CategoryTheory.Arrow.homMk' w)<GOAL>CategoryTheory.Limits.image.map (CategoryTheory.Arrow.homMk' w) ≫ CategoryTheory.Limits.image.ι l = CategoryTheory.Limits.image.ι k ≫ n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImage g.hom<VAR>sq : f ⟶ g<VAR>CategoryTheory.Limits.HasImageMap sq<VAR>h : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage h.hom<VAR>sq' : g ⟶ h<VAR>CategoryTheory.Limits.HasImageMap sq'<VAR>CategoryTheory.Limits.HasImageMap (sq ≫ sq')<GOAL>CategoryTheory.Limits.image.map (sq ≫ sq') = CategoryTheory.Limits.image.map sq ≫ CategoryTheory.Limits.image.map sq'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>CategoryTheory.Limits.HasImage f.hom<VAR>CategoryTheory.Limits.HasImageMap (𝟙 f)<GOAL>CategoryTheory.Limits.image.map (𝟙 f) = 𝟙 (CategoryTheory.Limits.image f.hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasImages C<VAR>self : CategoryTheory.Limits.HasImageMaps C<VAR>f g : CategoryTheory.Arrow C<VAR>st : f ⟶ g<GOAL>CategoryTheory.Limits.HasImageMap st
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasImages C<VAR>CategoryTheory.Limits.HasImageMaps C<GOAL>∀ {X Y : CategoryTheory.Arrow C} (st : X ⟶ Y), CategoryTheory.Limits.im.map st = CategoryTheory.Limits.image.map st
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasImages C<VAR>CategoryTheory.Limits.HasImageMaps C<VAR>f : CategoryTheory.Arrow C<GOAL>CategoryTheory.Limits.im.obj f = CategoryTheory.Limits.image f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.Limits.StrongEpiMonoFactorisation f<GOAL>CategoryTheory.StrongEpi self.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Nonempty (CategoryTheory.Limits.StrongEpiMonoFactorisation f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>d : {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.StrongEpiMonoFactorisation f<GOAL>CategoryTheory.Limits.HasStrongEpiMonoFactorisations C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasImages C<VAR>self : CategoryTheory.Limits.HasStrongEpiImages C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Limits.StrongEpiMonoFactorisation f<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<VAR>hF' : CategoryTheory.Limits.IsImage F'<GOAL>CategoryTheory.StrongEpi F'.e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>F : CategoryTheory.Limits.StrongEpiMonoFactorisation f<GOAL>CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrongEpiMonoFactorisations C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I' : C<VAR>e : X ⟶ I'<VAR>m : I' ⟶ Y<VAR>comm : e ≫ m = f<VAR>CategoryTheory.StrongEpi e<VAR>CategoryTheory.Mono m<GOAL>(CategoryTheory.Limits.image.isoStrongEpiMono e m comm).hom ≫ CategoryTheory.Limits.image.ι f = m
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrongEpiMonoFactorisations C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I' : C<VAR>e : X ⟶ I'<VAR>m : I' ⟶ Y<VAR>comm : e ≫ m = f<VAR>CategoryTheory.StrongEpi e<VAR>CategoryTheory.Mono m<GOAL>(CategoryTheory.Limits.image.isoStrongEpiMono e m comm).inv ≫ m = CategoryTheory.Limits.image.ι f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>F.IsEquivalence<VAR>h : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C<GOAL>CategoryTheory.Limits.HasStrongEpiMonoFactorisations D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G<GOAL>(CategoryTheory.Limits.PreservesLimitPair.iso G X Y).hom = CategoryTheory.Limits.prodComparison G X Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G<GOAL>(CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv ≫ G.map CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.prod.fst
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryProduct X Y<VAR>CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G<GOAL>(CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv ≫ G.map CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.prod.snd
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct X Y<VAR>CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G<GOAL>(CategoryTheory.Limits.PreservesColimitPair.iso G X Y).hom = CategoryTheory.Limits.coprodComparison G X Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G<GOAL>CategoryTheory.Limits.HasTerminal D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasTerminal D<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G<GOAL>(CategoryTheory.Limits.PreservesTerminal.iso G).hom = CategoryTheory.Limits.terminalComparison G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G<GOAL>CategoryTheory.Limits.HasInitial D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasInitial D<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G<GOAL>(CategoryTheory.Limits.PreservesInitial.iso G).inv = CategoryTheory.Limits.initialComparison G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G<GOAL>(CategoryTheory.Limits.PreservesEqualizer.iso G f g).hom = CategoryTheory.Limits.equalizerComparison f g G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G<GOAL>(CategoryTheory.Limits.PreservesEqualizer.iso G f g).inv ≫ G.map (CategoryTheory.Limits.equalizer.ι f g) = CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G<GOAL>(CategoryTheory.Limits.PreservesCoequalizer.iso G f g).hom = CategoryTheory.Limits.coequalizerComparison f g G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G<GOAL>G.map (CategoryTheory.Limits.coequalizer.π f g) ≫ (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv = CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G<VAR>W : D<VAR>k : G.obj Y ⟶ W<VAR>wk : G.map f ≫ k = G.map g ≫ k<GOAL>G.map (CategoryTheory.Limits.coequalizer.π f g) ≫ (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv ≫ CategoryTheory.Limits.coequalizer.desc k wk = k
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G<VAR>X' Y' : D<VAR>f' g' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasCoequalizer f' g'<VAR>p : G.obj X ⟶ X'<VAR>q : G.obj Y ⟶ Y'<VAR>wf : G.map f ≫ q = p ≫ f'<VAR>wg : G.map g ≫ q = p ≫ g'<GOAL>G.map (CategoryTheory.Limits.coequalizer.π f g) ≫ (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv ≫ CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) = q ≫ CategoryTheory.Limits.coequalizer.π f' g'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G<VAR>X' Y' : D<VAR>f' g' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasCoequalizer f' g'<VAR>p : G.obj X ⟶ X'<VAR>q : G.obj Y ⟶ Y'<VAR>wf : G.map f ≫ q = p ≫ f'<VAR>wg : G.map g ≫ q = p ≫ g'<VAR>Z' : D<VAR>h : Y' ⟶ Z'<VAR>wh : f' ≫ h = g' ≫ h<GOAL>G.map (CategoryTheory.Limits.coequalizer.π f g) ≫ (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv ≫ CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) ≫ CategoryTheory.Limits.coequalizer.desc h wh = q ≫ h
<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>J : Type w₁<VAR>f : J → C<VAR>b : CategoryTheory.Limits.Bicone f<VAR>j : J<GOAL>(F.mapBicone b).π j = F.map (b.π j)
<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>J : Type w₁<VAR>f : J → C<VAR>b : CategoryTheory.Limits.Bicone f<VAR>j : J<GOAL>(F.mapBicone b).ι j = F.map (b.ι j)
<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>J : Type w₁<VAR>f : J → C<VAR>b : CategoryTheory.Limits.Bicone f<GOAL>(F.mapBicone b).pt = F.obj b.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>K : Type w₂<VAR>g : K ≃ J<VAR>f : J → C<VAR>c : CategoryTheory.Limits.Bicone f<GOAL>F.mapBicone (c.whisker g) = (F.mapBicone c).whisker 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>b : CategoryTheory.Limits.BinaryBicone X Y<GOAL>(F.mapBinaryBicone b).inl = F.map b.inl
<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>b : CategoryTheory.Limits.BinaryBicone X Y<GOAL>(F.mapBinaryBicone b).snd = F.map b.snd
<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>b : CategoryTheory.Limits.BinaryBicone X Y<GOAL>(F.mapBinaryBicone b).fst = F.map b.fst
<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>b : CategoryTheory.Limits.BinaryBicone X Y<GOAL>(F.mapBinaryBicone b).inr = F.map b.inr
<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>b : CategoryTheory.Limits.BinaryBicone X Y<GOAL>(F.mapBinaryBicone b).pt = F.obj b.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>J : Type w₁<VAR>F : C ⥤ D<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)<VAR>j : J<GOAL>F.biproductComparison f ≫ CategoryTheory.Limits.biproduct.π (F.obj ∘ f) j = F.map (CategoryTheory.Limits.biproduct.π f j)
<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>J : Type w₁<VAR>F : C ⥤ D<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)<VAR>j : J<GOAL>CategoryTheory.Limits.biproduct.ι (F.obj ∘ f) j ≫ F.biproductComparison' f = F.map (CategoryTheory.Limits.biproduct.ι f j)
<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>J : Type w₁<VAR>F : C ⥤ D<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)<VAR>F.PreservesZeroMorphisms<GOAL>F.biproductComparison' f ≫ F.biproductComparison f = 𝟙 (⨁ F.obj ∘ f)
<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>J : Type w₁<VAR>F : C ⥤ D<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)<VAR>F.PreservesZeroMorphisms<GOAL>(F.splitEpiBiproductComparison f).section_ = F.biproductComparison' f
<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>J : Type w₁<VAR>F : C ⥤ D<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)<VAR>F.PreservesZeroMorphisms<GOAL>(F.splitMonoBiproductComparison' f).retraction = F.biproductComparison f
<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>J : Type w₁<VAR>F : C ⥤ D<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>F.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.PreservesBiproduct f F<GOAL>(F.mapBiproduct f).hom = CategoryTheory.Limits.biproduct.lift fun j => F.map (CategoryTheory.Limits.biproduct.π f j)
<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>J : Type w₁<VAR>F : C ⥤ D<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>F.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.PreservesBiproduct f F<GOAL>(F.mapBiproduct f).inv = CategoryTheory.Limits.biproduct.desc fun j => F.map (CategoryTheory.Limits.biproduct.ι f j)
<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>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)<GOAL>F.biprodComparison X Y ≫ CategoryTheory.Limits.biprod.fst = F.map CategoryTheory.Limits.biprod.fst
<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>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)<GOAL>F.biprodComparison X Y ≫ CategoryTheory.Limits.biprod.snd = F.map CategoryTheory.Limits.biprod.snd
<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>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)<GOAL>CategoryTheory.Limits.biprod.inl ≫ F.biprodComparison' X Y = F.map CategoryTheory.Limits.biprod.inl
<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>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)<GOAL>CategoryTheory.Limits.biprod.inr ≫ F.biprodComparison' X Y = F.map CategoryTheory.Limits.biprod.inr
<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>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)<VAR>F.PreservesZeroMorphisms<GOAL>F.biprodComparison' X Y ≫ F.biprodComparison X Y = 𝟙 (F.obj X ⊞ F.obj Y)
<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>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)<VAR>F.PreservesZeroMorphisms<GOAL>(F.splitEpiBiprodComparison X Y).section_ = F.biprodComparison' X Y
<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>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)<VAR>F.PreservesZeroMorphisms<GOAL>(F.splitMonoBiprodComparison' X Y).retraction = F.biprodComparison X Y
<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>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>F.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.PreservesBinaryBiproduct X Y F<GOAL>(F.mapBiprod X Y).hom = CategoryTheory.Limits.biprod.lift (F.map CategoryTheory.Limits.biprod.fst) (F.map CategoryTheory.Limits.biprod.snd)
<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>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>F.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.PreservesBinaryBiproduct X Y F<GOAL>(F.mapBiprod X Y).inv = CategoryTheory.Limits.biprod.desc (F.map CategoryTheory.Limits.biprod.inl) (F.map CategoryTheory.Limits.biprod.inr)
<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>J : Type w₁<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → W ⟶ f j<GOAL>F.map (CategoryTheory.Limits.biproduct.lift g) ≫ (F.mapBiproduct f).hom = CategoryTheory.Limits.biproduct.lift fun j => F.map (g j)
<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>J : Type w₁<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → f j ⟶ W<GOAL>(F.mapBiproduct f).inv ≫ F.map (CategoryTheory.Limits.biproduct.desc g) = CategoryTheory.Limits.biproduct.desc fun j => F.map (g j)
<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>J : Type w₁<VAR>f : J → C<VAR>CategoryTheory.Limits.HasBiproduct f<VAR>CategoryTheory.Limits.PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → f j ⟶ W<GOAL>((F.mapBiproduct f).hom ≫ CategoryTheory.Limits.biproduct.desc fun j => F.map (g j)) = F.map (CategoryTheory.Limits.biproduct.desc g)