-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
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
⊢ 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)) φ)
have 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 := sorry },
                      naturality := sorry },
                  inv :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := sorry },
                      naturality := sorry },
                  hom_inv_id := sorry, inv_hom_id := sorry :
                  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 := sorry },
                      naturality := sorry },
                  inv :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := sorry },
                      naturality := sorry },
                  hom_inv_id := sorry, inv_hom_id := sorry :
                  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))
Tactic: ext P