∀ (C : Type u_1) (D : Type u_4) [inst : CategoryTheory.Category.{u_2, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D]
  (G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)),
  CategoryTheory.CategoryStruct.comp { app := fun P => { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ }
      { app := fun P => { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id
      ((((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C)
                    (CategoryTheory.Idempotents.Karoubi D)).obj
                (CategoryTheory.Idempotents.toKaroubi C)).comp
            (CategoryTheory.Idempotents.functorExtension₁ C D)).obj
        G)