∀ {J : Type u_3} {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : Nonempty J] {s : CategoryTheory.Limits.Trident f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X)
  (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)),
  CategoryTheory.CategoryStruct.comp (hs.lift (CategoryTheory.Limits.Trident.ofι k h))
      (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero) =
    (CategoryTheory.Limits.Trident.ofι k h).π.app CategoryTheory.Limits.WalkingParallelFamily.zero