∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u_4}
  [inst_2 : CategoryTheory.Category.{u_3, u_4} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {X Y : D}
  (i : X ⟶ Y) [inst_4 : CategoryTheory.Limits.HasCokernel i] (F : CategoryTheory.Functor D C)
  [inst_5 : F.PreservesZeroMorphisms]
  [inst_6 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair i 0) F],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.Limits.KernelFork.ofι (F.map i) ⋯).pt).hom
      (CategoryTheory.Limits.Fork.ι
        ((CategoryTheory.Limits.Cones.postcompose
              (CategoryTheory.Limits.parallelPair.ext
                  (CategoryTheory.Iso.refl
                    ((CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π (F.map i)) 0).obj
                      CategoryTheory.Limits.WalkingParallelPair.zero))
                  (CategoryTheory.asIso (CategoryTheory.Limits.cokernelComparison i F)) ⋯ ⋯).inv).obj
          (F.mapCone (CategoryTheory.Limits.KernelFork.ofι i ⋯)))) =
    CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι (F.map i) ⋯)