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
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ limit.π (curry.obj F ⋙ colim) j
      (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 } }
        (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)
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
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ limit.π (curry.obj F ⋙ colim) j (colimitLimitToLimitColimit F (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)
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
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ limit.π (curry.obj F ⋙ colim) j
      (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 } }
        (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)
simp