-- Module: Mathlib.CategoryTheory.Limits.ColimitLimit
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'
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 := ⋯ } :
                    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 := ⋯ } :
                      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))) :
        (obj curry (swap K J ⋙ F) ⋙ lim).obj k ⟶ colimit ((obj curry F).obj 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'))

Tactic:
ext k