J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫
      limit.lift (curry.obj F ⋙ colim)
          { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
            π :=
              NatTrans.mk fun j =>
                colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                  { pt := colimit ((curry.obj F).obj j),
                    ι :=
                      NatTrans.mk fun k =>
                        limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k } } ≫
        limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫ colimitLimitToLimitColimit F ≫ limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k
dsimp [colimitLimitToLimitColimit]
no goals
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫
      limit.lift (curry.obj F ⋙ colim)
          { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
            π :=
              NatTrans.mk fun j =>
                colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                  { pt := colimit ((curry.obj F).obj j),
                    ι :=
                      NatTrans.mk fun k =>
                        limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k } } ≫
        limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k
simp