-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (obj (functorExtension₂ C D ⋙ obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
              F).map
          f ≫
        Iso.hom
          ((fun (X : C) ↦
              {
                hom :=
                  {
                    f :=
                      𝟙
                        ((obj
                                (functorExtension₂ C D ⋙
                                  obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                                F).obj
                            X).X,
                    comm := ⋯ },
                inv :=
                  { f := 𝟙 ((obj (obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D)) F).obj X).X,
                    comm := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                (obj
                        (functorExtension₂ C D ⋙
                          obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                        F).obj
                    X ≅
                  (obj (obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D)) F).obj X })
            Y) =
      Iso.hom
          ((fun (X : C) ↦
              {
                hom :=
                  {
                    f :=
                      𝟙
                        ((obj
                                (functorExtension₂ C D ⋙
                                  obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                                F).obj
                            X).X,
                    comm := ⋯ :
                    ((obj
                              (functorExtension₂ C D ⋙
                                obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                              F).obj
                          X).Hom
                      ((obj (obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D)) F).obj X) },
                inv :=
                  { f := 𝟙 ((obj (obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D)) F).obj X).X,
                    comm := ⋯ :
                    ((obj (obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D)) F).obj X).Hom
                      ((obj
                            (functorExtension₂ C D ⋙
                              obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                            F).obj
                        X) },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                (obj
                        (functorExtension₂ C D ⋙
                          obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C))
                        F).obj
                    X ≅
                  (obj (obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D)) F).obj X })
            X) ≫
        (obj (obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D)) F).map f

Tactic:
simp