J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ ((limitIsoLimitCurryCompLim G).inv ≫
        (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ G))).inv ≫
          (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).hom) ≫
      limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ (limitCurrySwapCompLimIsoLimitCurryCompLim G).inv ≫
      limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).inv ≫
      limit.π G ((Prod.braiding K J).functor.obj (k, j)) ≫ (𝟙 ((Prod.braiding K J).functor ⋙ G)).app (k, j) =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ ((limitIsoLimitCurryCompLim G).inv ≫
        (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ G))).inv ≫
          (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).hom) ≫
      limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
simp only [Iso.refl_hom, Prod.braiding_counitIso_hom_app, Limits.HasLimit.isoOfEquivalence_inv_π,
  Iso.refl_inv, limitIsoLimitCurryCompLim_hom_π_π, eqToIso_refl, Category.assoc]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).inv ≫
      limit.π G ((Prod.braiding K J).functor.obj (k, j)) ≫ 𝟙 (((Prod.braiding K J).functor ⋙ G).obj (k, j)) =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).inv ≫
      limit.π G ((Prod.braiding K J).functor.obj (k, j)) ≫ (𝟙 ((Prod.braiding K J).functor ⋙ G)).app (k, j) =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
erw [NatTrans.id_app]
no goals
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).inv ≫
      limit.π G ((Prod.braiding K J).functor.obj (k, j)) ≫ 𝟙 (((Prod.braiding K J).functor ⋙ G).obj (k, j)) =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
simp