J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) =
    (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (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 K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) = limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
rw [← cancel_epi (limitUncurryIsoLimitCompLim F).hom]
no goals
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) =
    (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
simp