∀ {J : Type u_2} [inst : CategoryTheory.Category.{u_4, u_2} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_1, u_3} C] {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F}
  (P : CategoryTheory.Limits.IsLimit r) (i : r ≅ t) (s : CategoryTheory.Limits.Cone F) (m : s ⟶ t),
  m = (fun s => CategoryTheory.CategoryStruct.comp (P.liftConeMorphism s) i.hom) s