[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
⊢ ∀ ⦃X Y : K⦄ (f : X ⟶ Y),
    (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).map f ≫
        (fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) Y =
      (fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) X ≫
        ((Functor.const K).obj (colimit.cocone ((curry.obj F).obj j)).1).map f
[PROOFSTEP]
intro k k' f
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k k' : K
f : k ⟶ k'
⊢ (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).map f ≫
      (fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) k' =
    (fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) k ≫
      ((Functor.const K).obj (colimit.cocone ((curry.obj F).obj j)).1).map f
[PROOFSTEP]
simp only [Functor.comp_obj, lim_obj, colimit.cocone_x, Functor.const_obj_obj, Functor.comp_map, lim_map,
  curry_obj_obj_obj, Prod.swap_obj, limMap_π_assoc, curry_obj_map_app, Prod.swap_map, Functor.const_obj_map,
  Category.comp_id]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k k' : K
f : k ⟶ k'
⊢ limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ F.map (𝟙 j, f) ≫ colimit.ι ((curry.obj F).obj j) k' =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k
[PROOFSTEP]
rw [map_id_left_eq_curry_map, colimit.w]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj (colimit.cocone (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)).1).map f ≫
        (fun j =>
            colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
              { pt := (colimit.cocone ((curry.obj F).obj j)).1,
                ι :=
                  NatTrans.mk fun k =>
                    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k })
          Y =
      (fun j =>
            colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
              { pt := (colimit.cocone ((curry.obj F).obj j)).1,
                ι :=
                  NatTrans.mk fun k =>
                    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k })
          X ≫
        (curry.obj F ⋙ colim).map f
[PROOFSTEP]
intro j j' f
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (colimit.cocone (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)).1).map f ≫
      (fun j =>
          colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
            { pt := (colimit.cocone ((curry.obj F).obj j)).1,
              ι :=
                NatTrans.mk fun k =>
                  limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k })
        j' =
    (fun j =>
          colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
            { pt := (colimit.cocone ((curry.obj F).obj j)).1,
              ι :=
                NatTrans.mk fun k =>
                  limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k })
        j ≫
      (curry.obj F ⋙ colim).map f
[PROOFSTEP]
dsimp
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
⊢ 𝟙 (colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)) ≫
      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.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 } ≫
      colimMap ((curry.obj F).map f)
[PROOFSTEP]
ext k
[GOAL]
case w
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫
      𝟙 (colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)) ≫
        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 ≫
      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 } ≫
        colimMap ((curry.obj F).map f)
[PROOFSTEP]
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]
[GOAL]
case w
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
k : K
⊢ limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((curry.obj F).obj j') k =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ F.map (f, 𝟙 k) ≫ colimit.ι ((curry.obj F).obj j') k
[PROOFSTEP]
rw [map_id_right_eq_curry_swap_map, limit.w_assoc]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} 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
[PROOFSTEP]
dsimp [colimitLimitToLimitColimit]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} 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
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} 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)
[PROOFSTEP]
dsimp [colimitLimitToLimitColimit]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} 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)
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
⊢ (colim.map (limitIsoSwapCompLim G).hom ≫
        colimitLimitToLimitColimit (uncurry.obj G) ≫ lim.map (whiskerRight (currying.unitIso.app G).inv colim)) ≫
      NatTrans.app (limit.cone (G ⋙ colim)).π j =
    NatTrans.app (colim.mapCone (limit.cone G)).π j
[PROOFSTEP]
dsimp
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
⊢ (colimMap (limitIsoSwapCompLim G).hom ≫
        colimitLimitToLimitColimit (uncurry.obj G) ≫
          limMap (whiskerRight (NatTrans.app currying.unitIso.inv G) colim)) ≫
      limit.π (G ⋙ colim) j =
    colimMap (limit.π G j)
[PROOFSTEP]
ext1 k
[GOAL]
case w
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
k : K
⊢ colimit.ι (limit G) k ≫
      (colimMap (limitIsoSwapCompLim G).hom ≫
          colimitLimitToLimitColimit (uncurry.obj G) ≫
            limMap (whiskerRight (NatTrans.app currying.unitIso.inv G) colim)) ≫
        limit.π (G ⋙ colim) j =
    colimit.ι (limit G) k ≫ colimMap (limit.π G j)
[PROOFSTEP]
simp only [Category.assoc, limMap_π, Functor.comp_obj, colim_obj, whiskerRight_app, colim_map, ι_colimMap_assoc,
  lim_obj, limitIsoSwapCompLim_hom_app, ι_colimitLimitToLimitColimit_π_assoc, curry_obj_obj_obj, Prod.swap_obj,
  uncurry_obj_obj, ι_colimMap, currying_unitIso_inv_app_app_app, Category.id_comp, limMap_π_assoc, Functor.flip_obj_obj,
  flipIsoCurrySwapUncurry_hom_app_app]
[GOAL]
case w
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
k : K
⊢ (limitObjIsoLimitCompEvaluation G k).hom ≫ limit.π ((Functor.flip G).obj k) j ≫ colimit.ι (G.obj j) k =
    NatTrans.app (limit.π G j) k ≫ colimit.ι (G.obj j) k
[PROOFSTEP]
erw [limitObjIsoLimitCompEvaluation_hom_π_assoc]
