∀ {J : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} J] {K : Type u_5}
  [inst_1 : CategoryTheory.Category.{u_6, u_5} K] {C : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} C]
  {F : CategoryTheory.Functor J C} (e : K ≌ J) (s : CategoryTheory.Limits.Cone F) (j : J),
  ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).π.app j =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).pt).hom
      ((((CategoryTheory.Limits.Cones.whiskering e.functor).comp
                  ((CategoryTheory.Limits.Cones.whiskering e.inverse).comp
                    (CategoryTheory.Limits.Cones.postcompose (e.invFunIdAssoc F).hom))).obj
              s).π.app
        j)