ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.Fork f f<VAR>h : CategoryTheory.Limits.IsLimit c<GOAL>CategoryTheory.IsIso c.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.Fork f g<VAR>h : CategoryTheory.Limits.IsLimit c<VAR>CategoryTheory.Epi c.ι<GOAL>CategoryTheory.IsIso c.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Fork f g<VAR>CategoryTheory.Epi t.ι<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>CategoryTheory.Epi (CategoryTheory.Limits.equalizer.ι f g)<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Limits.equalizer.isoSourceOfSelf f).hom = CategoryTheory.Limits.equalizer.ι f f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Limits.equalizer.isoSourceOfSelf f).inv = CategoryTheory.Limits.equalizer.lift (CategoryTheory.CategoryStruct.id X) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<GOAL>(CategoryTheory.Limits.coequalizer.cofork f g).π = CategoryTheory.Limits.coequalizer.π f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<GOAL>(CategoryTheory.Limits.coequalizer.cofork f g).ι.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.Limits.coequalizer.π f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.coequalizer.π f g) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.coequalizer.π f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>W : C<VAR>k : Y ⟶ W<VAR>h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) (CategoryTheory.Limits.coequalizer.desc k h) = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>X' Y' Z : C<VAR>f' g' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasCoequalizer f' g'<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f'<VAR>wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g'<VAR>h : Y' ⟶ Z<VAR>wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom f g f' g' p q wf wg)) (CategoryTheory.Limits.coequalizer.desc h wh)) = CategoryTheory.CategoryStruct.comp q h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>W : C<VAR>k l : CategoryTheory.Limits.coequalizer f g ⟶ W<VAR>h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) l<GOAL>k = l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>W : C<VAR>k : Y ⟶ W<VAR>h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k<GOAL>∃! d, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) d = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.Cofork f g<VAR>i : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.Epi c.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h₀ : f = g<VAR>c : CategoryTheory.Limits.Cofork f g<VAR>h : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsIso c.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>h : f = g<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.coequalizer.π f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.Cofork f f<VAR>h : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsIso c.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.Cofork f g<VAR>h : CategoryTheory.Limits.IsColimit c<VAR>CategoryTheory.Mono c.π<GOAL>CategoryTheory.IsIso c.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : CategoryTheory.Limits.Cofork f g<VAR>CategoryTheory.Mono t.π<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>CategoryTheory.Mono (CategoryTheory.Limits.coequalizer.π f g)<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Limits.coequalizer.isoTargetOfSelf f).hom = CategoryTheory.Limits.coequalizer.desc (CategoryTheory.CategoryStruct.id Y) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Limits.coequalizer.isoTargetOfSelf f).inv = CategoryTheory.Limits.coequalizer.π f f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerComparison f g G) (CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)) = G.map (CategoryTheory.Limits.equalizer.ι f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)<VAR>Z : C<VAR>h : Z ⟶ X<VAR>w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g<GOAL>CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.equalizer.lift h w)) (CategoryTheory.Limits.equalizerComparison f g G) = CategoryTheory.Limits.equalizer.lift (G.map h) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g)) (CategoryTheory.Limits.coequalizerComparison f g G) = G.map (CategoryTheory.Limits.coequalizer.π f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizerComparison f g G) (G.map (CategoryTheory.Limits.coequalizer.desc h w)) = CategoryTheory.Limits.coequalizer.desc (G.map h) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)<GOAL>CategoryTheory.Limits.HasEqualizers C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f g)<GOAL>CategoryTheory.Limits.HasCoequalizers C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<GOAL>(CategoryTheory.Limits.coneOfIsSplitMono f).pt = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelPair), (CategoryTheory.Limits.coneOfIsSplitMono f).π.app X_1 = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t => X_1 = t → (X ⟶ (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f)).obj X_1)) (fun h => ⋯ ▸ f) (fun h => ⋯ ▸ f) X_1 ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<GOAL>(CategoryTheory.Limits.coneOfIsSplitMono f).ι = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>CategoryTheory.Mono h<GOAL>CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f : X ⟶ X<VAR>hf : CategoryTheory.CategoryStruct.comp f f = f<VAR>c : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id X) f<VAR>i : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C hf i).retraction = i.lift (CategoryTheory.Limits.Fork.ofι f ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitEpi f<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelPair), (CategoryTheory.Limits.coconeOfIsSplitEpi f).ι.app X_1 = CategoryTheory.Limits.WalkingParallelPair.rec f f X_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitEpi f<GOAL>(CategoryTheory.Limits.coconeOfIsSplitEpi f).pt = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitEpi f<GOAL>(CategoryTheory.Limits.coconeOfIsSplitEpi f).π = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<VAR>W : C<VAR>h : W ⟶ X<VAR>CategoryTheory.Epi h<GOAL>CategoryTheory.Limits.HasCoequalizer (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f : X ⟶ X<VAR>hf : CategoryTheory.CategoryStruct.comp f f = f<VAR>c : CategoryTheory.Limits.Cofork (CategoryTheory.CategoryStruct.id X) f<VAR>i : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C hf i).section_ = i.desc (CategoryTheory.Limits.Cofork.ofπ f ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<GOAL>G.map (CategoryTheory.Limits.Fork.ι c) ≫ G.map f = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<GOAL>CategoryTheory.Limits.Fork.ι (c.map G) = G.map (CategoryTheory.Limits.Fork.ι c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel (G.map f)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G<GOAL>(CategoryTheory.Limits.PreservesKernel.iso G f).hom = CategoryTheory.Limits.kernelComparison f G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel (G.map f)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G<VAR>X' Y' : C<VAR>g : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasKernel g<VAR>CategoryTheory.Limits.HasKernel (G.map g)<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair g 0) G<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>CategoryTheory.Limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ ≫ (CategoryTheory.Limits.PreservesKernel.iso G g).inv = (CategoryTheory.Limits.PreservesKernel.iso G f).inv ≫ G.map (CategoryTheory.Limits.kernel.map f g p q hpq)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<GOAL>G.map f ≫ G.map (CategoryTheory.Limits.Cofork.π c) = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<GOAL>CategoryTheory.Limits.Cofork.π (c.map G) = G.map (CategoryTheory.Limits.Cofork.π c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel (G.map f)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G<GOAL>(CategoryTheory.Limits.PreservesCokernel.iso G f).inv = CategoryTheory.Limits.cokernelComparison f G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel (G.map f)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G<VAR>X' Y' : C<VAR>g : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasCokernel g<VAR>CategoryTheory.Limits.HasCokernel (G.map g)<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair g 0) G<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>(CategoryTheory.Limits.PreservesCokernel.iso G f).hom ≫ CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ = G.map (CategoryTheory.Limits.cokernel.map f g p q hpq) ≫ (CategoryTheory.Limits.PreservesCokernel.iso G g).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : CategoryTheory.Limits.KernelFork f<GOAL>CategoryTheory.Limits.Fork.ι s ≫ f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : CategoryTheory.Limits.KernelFork f<GOAL>s.π.app CategoryTheory.Limits.WalkingParallelPair.one = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y P : C<VAR>f : X ⟶ Y<VAR>ι : P ⟶ X<VAR>w : ι ≫ f = 0<GOAL>CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι ι w) = ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>i : CategoryTheory.Limits.IsLimit c<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>hg : CategoryTheory.Mono g<VAR>h : X ⟶ Z<VAR>hh : h = f ≫ g<VAR>s : CategoryTheory.Limits.KernelFork h<GOAL>(CategoryTheory.Limits.isKernelCompMono i g hh).lift s = i.lift (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.Fork.ι s) ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>hf : f = 0<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.Fork.ι c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>kf : CategoryTheory.Limits.KernelFork f<VAR>kf' : CategoryTheory.Limits.KernelFork f'<VAR>hf' : CategoryTheory.Limits.IsLimit kf'<VAR>φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'<GOAL>kf.mapOfIsLimit hf' φ ≫ CategoryTheory.Limits.Fork.ι kf' = CategoryTheory.Limits.Fork.ι kf ≫ φ.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>kf : CategoryTheory.Limits.KernelFork f<VAR>kf' : CategoryTheory.Limits.KernelFork f'<VAR>hf : CategoryTheory.Limits.IsLimit kf<VAR>hf' : CategoryTheory.Limits.IsLimit kf'<VAR>φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'<GOAL>(CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit hf hf' φ).inv = kf'.mapOfIsLimit hf φ.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>kf : CategoryTheory.Limits.KernelFork f<VAR>kf' : CategoryTheory.Limits.KernelFork f'<VAR>hf : CategoryTheory.Limits.IsLimit kf<VAR>hf' : CategoryTheory.Limits.IsLimit kf'<VAR>φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'<GOAL>(CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit hf hf' φ).hom = kf.mapOfIsLimit hf' φ.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<GOAL>CategoryTheory.Limits.equalizer.ι f 0 = CategoryTheory.Limits.kernel.ι f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<GOAL>CategoryTheory.Limits.kernel.ι f ≫ f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>W : C<VAR>k : W ⟶ X<VAR>h : k ≫ f = 0<GOAL>CategoryTheory.Limits.kernel.lift f k h ≫ CategoryTheory.Limits.kernel.ι f = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>W : C<VAR>h : 0 ≫ f = 0<GOAL>CategoryTheory.Limits.kernel.lift f 0 h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z X' Y' Z' : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasKernel g<VAR>w : f ≫ g = 0<VAR>f' : X' ⟶ Y'<VAR>g' : Y' ⟶ Z'<VAR>CategoryTheory.Limits.HasKernel g'<VAR>w' : f' ≫ g' = 0<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>r : Z ⟶ Z'<VAR>h₁ : f ≫ q = p ≫ f'<VAR>h₂ : g ≫ r = q ≫ g'<GOAL>CategoryTheory.Limits.kernel.lift g f w ≫ CategoryTheory.Limits.kernel.map g g' q r h₂ = p ≫ CategoryTheory.Limits.kernel.lift g' f' w'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasKernel f'<VAR>p : X ≅ X'<VAR>q : Y ≅ Y'<VAR>w : f ≫ q.hom = p.hom ≫ f'<GOAL>(CategoryTheory.Limits.kernel.mapIso f f' p q w).inv = CategoryTheory.Limits.kernel.map f' f p.inv q.inv ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasKernel f'<VAR>p : X ≅ X'<VAR>q : Y ≅ Y'<VAR>w : f ≫ q.hom = p.hom ≫ f'<GOAL>(CategoryTheory.Limits.kernel.mapIso f f' p q w).hom = CategoryTheory.Limits.kernel.map f f' p.hom q.hom w
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Epi (CategoryTheory.Limits.kernel.ι f)<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<GOAL>CategoryTheory.Limits.kernelZeroIsoSource.hom = CategoryTheory.Limits.kernel.ι 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<GOAL>CategoryTheory.Limits.kernelZeroIsoSource.inv = CategoryTheory.Limits.kernel.lift 0 (𝟙 X) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>h : f = f<GOAL>CategoryTheory.Limits.kernelIsoOfEq h = CategoryTheory.Iso.refl (CategoryTheory.Limits.kernel f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel g<VAR>h : f = g<GOAL>(CategoryTheory.Limits.kernelIsoOfEq h).hom ≫ CategoryTheory.Limits.kernel.ι g = CategoryTheory.Limits.kernel.ι f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel g<VAR>h : f = g<GOAL>(CategoryTheory.Limits.kernelIsoOfEq h).inv ≫ CategoryTheory.Limits.kernel.ι f = CategoryTheory.Limits.kernel.ι g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel g<VAR>h : f = g<VAR>e : Z ⟶ X<VAR>he : e ≫ f = 0<GOAL>CategoryTheory.Limits.kernel.lift f e he ≫ (CategoryTheory.Limits.kernelIsoOfEq h).hom = CategoryTheory.Limits.kernel.lift g e ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel g<VAR>h : f = g<VAR>e : Z ⟶ X<VAR>he : e ≫ g = 0<GOAL>CategoryTheory.Limits.kernel.lift g e he ≫ (CategoryTheory.Limits.kernelIsoOfEq h).inv = CategoryTheory.Limits.kernel.lift f e ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f g h : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel g<VAR>CategoryTheory.Limits.HasKernel h<VAR>w₁ : f = g<VAR>w₂ : g = h<GOAL>CategoryTheory.Limits.kernelIsoOfEq w₁ ≪≫ CategoryTheory.Limits.kernelIsoOfEq w₂ = CategoryTheory.Limits.kernelIsoOfEq ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>w : f ≠ 0<GOAL>¬CategoryTheory.Epi (CategoryTheory.Limits.kernel.ι f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>w : f ≠ 0<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.kernel.ι f) → False
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Mono g<GOAL>(CategoryTheory.Limits.kernelCompMono f g).hom = CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.kernel.ι (f ≫ g)) ⋯