∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C],
  CategoryTheory.CategoryStruct.comp { app := fun P => { f := { f := P.p.f, comm := ⋯ }, comm := ⋯ }, naturality := ⋯ }
      { app := fun P => { f := { f := P.p.f, comm := ⋯ }, comm := ⋯ }, naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).comp
        (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Idempotents.Karoubi C)))