∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F G : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasLimit F] [inst_2 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G) (j : J)
  (x : CategoryTheory.Limits.limit F),
  CategoryTheory.Limits.limit.π G j (CategoryTheory.Limits.limMap α x) = α.app j (CategoryTheory.Limits.limit.π F j x)