CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π

theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π : ∀ {J K : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.SmallCategory K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C] [inst_4 : CategoryTheory.Limits.HasLimit G] [inst_5 : CategoryTheory.Limits.HasLimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K}, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)) = CategoryTheory.Limits.limit.π G (j, k)

This theorem states that for any two types `J` and `K`, which are small categories, and a type `C` which is a category, given a functor `G` from the product of `J` and `K` to `C`, if `C` has limits of shape `K` and the functor `G` and the composition of the curry of `G` with the limit have limits, then the composition of the homomorphism from the isomorphism between the limit and the curry composition limit of `G` with the composition of two projections (the first from the limit of the composition of the curry of `G` with the limit to an object `j` of `J`, the second from the object `j` of the curry of `G` to an object `k` of `K`) is equal to the projection from the limit of `G` to the pair `(j, k)`.

More concisely: Given functors `G: J × K → C` from the product of small categories `J` and `K` to a category `C` with limits of shape `K`, if `C` has limits of shape `J × K` and the limit of `G` and the limit of the composition `G ∘ (π1 ∘ product.fst) ∘ limit` exist, then the composition of the homomorphism from the limit to `G` with the projections `π1` and `π2` equals the projection from the limit of `G` to `J × K`.