-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
j j' : J
f : j ⟶ j'
⊢ Eq (α := colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶ colimit ((obj curry F).obj j'))
    (𝟙 (colimit (obj curry (swap K J ⋙ F) ⋙ lim)) ≫
        colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
          { pt := colimit ((obj curry F).obj j'),
            ι :=
              ({
                  app := fun (k : K) ↦
                    limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k,
                  naturality := ⋯ } :
                NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j')))) } :
      colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶ colimit ((obj curry F).obj j'))
    (CategoryStruct.comp (Y := colimit ((obj curry F).obj j))
        (colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
            { pt := colimit ((obj curry F).obj j),
              ι :=
                ({
                    app := fun (k : K) ↦
                      limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                    naturality := ⋯ } :
                  NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) } :
          colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶
            Cocone.pt (F := obj curry (swap K J ⋙ F) ⋙ lim)
              { pt := colimit ((obj curry F).obj j),
                ι :=
                  ({
                      app := fun (k : K) ↦
                        limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                      naturality := ⋯ } :
                    NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) })
        (colimMap ((obj curry F).map f)) :
      colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶ colimit ((obj curry F).obj j'))
have w : ∀ (k : K),
  Eq (α := (obj curry (swap K J ⋙ F) ⋙ lim).obj k ⟶ colimit ((obj curry F).obj j'))
    (CategoryStruct.comp (Y := colimit (obj curry (swap K J ⋙ F) ⋙ lim)) (colimit.ι (obj curry (swap K J ⋙ F) ⋙ lim) k)
        (𝟙 (colimit (obj curry (swap K J ⋙ F) ⋙ lim)) ≫
          colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
            { pt := colimit ((obj curry F).obj j'),
              ι :=
                ({
                    app := fun (k : K) ↦
                      limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k,
                    naturality := sorry } :
                  NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j')))) }) :
      (obj curry (swap K J ⋙ F) ⋙ lim).obj k ⟶ colimit ((obj curry F).obj j'))
    (CategoryStruct.comp (Y := colimit (obj curry (swap K J ⋙ F) ⋙ lim)) (colimit.ι (obj curry (swap K J ⋙ F) ⋙ lim) k)
        (CategoryStruct.comp (Y := colimit ((obj curry F).obj j))
          (colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
              { pt := colimit ((obj curry F).obj j),
                ι :=
                  ({
                      app := fun (k : K) ↦
                        limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                      naturality := sorry } :
                    NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) } :
            colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶
              Cocone.pt (F := obj curry (swap K J ⋙ F) ⋙ lim)
                { pt := colimit ((obj curry F).obj j),
                  ι :=
                    ({
                        app := fun (k : K) ↦
                          limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                        naturality := sorry } :
                      NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) })
          (colimMap ((obj curry F).map f))) :
      (obj curry (swap K J ⋙ F) ⋙ lim).obj k ⟶ colimit ((obj curry F).obj j'))
Tactic: ext k