-- 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'
k : K
w :
  Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j'))
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k)
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ F.map (f ×ₘ 𝟙 k) ≫ colimit.ι ((obj curry F).obj j') 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'))

Tactic:
simp only [Functor.comp_obj, lim_obj, Category.id_comp, colimit.ι_desc,
              colimit.ι_desc_assoc, Category.assoc, ι_colimMap,
              curry_obj_obj_obj, curry_obj_map_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.curry_obj_obj_obj, CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.lim_obj, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.ι_desc_assoc, CategoryTheory.Functor.curry_obj_map_app, CategoryTheory.Category.id_comp