∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{z, w} D]
  [inst_2 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C),
  (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι (α.app X))
        ((CategoryTheory.Limits.kernel.ι α).app X)
        (CategoryTheory.Limits.PreservesKernel.iso ((CategoryTheory.evaluation C D).obj X) α).inv
        (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯)
      (CategoryTheory.Limits.cokernelComparison (CategoryTheory.Limits.kernel.ι α)
        ((CategoryTheory.evaluation C D).obj X))