-- 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
X Y : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
φ : X ⟶ Y
w :
  ∀ (P : Karoubi.{v_1, u_1} C),
    Eq (α :=
      ((obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
                X).obj
            P).X ⟶
        ((obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) Y).obj P).X)
      (Hom.f
        (NatTrans.app
          (map
              (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                functorExtension₁ C D)
              φ ≫
            Iso.hom
              ((fun (G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D) ↦
                  {
                    hom :=
                      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ },
                        naturality := ⋯ },
                    inv :=
                      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ },
                        naturality := ⋯ },
                    hom_inv_id := ⋯, inv_hom_id := ⋯ :
                    obj
                        (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                          functorExtension₁ C D)
                        G ≅
                      obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G })
                Y))
          P))
      (Hom.f
        (NatTrans.app
          (Iso.hom
              ((fun (G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D) ↦
                  {
                    hom :=
                      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ },
                        naturality := ⋯ },
                    inv :=
                      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ },
                        naturality := ⋯ },
                    hom_inv_id := ⋯, inv_hom_id := ⋯ :
                    obj
                        (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                          functorExtension₁ C D)
                        G ≅
                      obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G })
                X) ≫
            map (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) φ)
          P))
⊢ Eq (α :=
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D) X ⟶
      obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) Y)
    (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
        φ ≫
      Iso.hom
        ((fun (G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D) ↦
            {
              hom :=
                { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ },
              inv :=
                { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ },
              hom_inv_id := ⋯, inv_hom_id := ⋯ :
              obj
                  (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                    functorExtension₁ C D)
                  G ≅
                obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G })
          Y))
    (Iso.hom
        ((fun (G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D) ↦
            {
              hom :=
                { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ },
              inv :=
                { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ },
              hom_inv_id := ⋯, inv_hom_id := ⋯ :
              obj
                  (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                    functorExtension₁ C D)
                  G ≅
                obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G })
          X) ≫
      map (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) φ)

Tactic:
ext P