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✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape (J × K) C
inst✝ : HasLimitsOfShape (K × J) C
j : J
k : K
⊢ ((limitUncurryIsoLimitCompLim (Functor.flip F)).inv ≫
        (HasLimit.isoOfNatIso (uncurryObjFlip F)).hom ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents fun x => Iso.refl ((F.obj x.snd).obj x.fst))).hom ≫
            (limitUncurryIsoLimitCompLim F).hom) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (Functor.flip F ⋙ lim) k ≫ limit.π ((Functor.flip F).obj k) j
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✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape (J × K) C
inst✝ : HasLimitsOfShape (K × J) C
j : J
k : K
⊢ (limitFlipCompLimIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (Functor.flip F ⋙ lim) k ≫ limit.π ((Functor.flip F).obj k) j
dsimp [limitFlipCompLimIsoLimitCompLim]
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✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape (J × K) C
inst✝ : HasLimitsOfShape (K × J) C
j : J
k : K
⊢ ((limitUncurryIsoLimitCompLim (Functor.flip F)).inv ≫
        (HasLimit.isoOfNatIso (uncurryObjFlip F)).hom ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents fun x => Iso.refl ((F.obj x.snd).obj x.fst))).hom ≫
            (limitUncurryIsoLimitCompLim F).hom) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (Functor.flip F ⋙ lim) k ≫ limit.π ((Functor.flip F).obj k) j
simp