∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X)
  {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s)
  {c : CategoryTheory.Limits.PullbackCone s.ι h} (hc : CategoryTheory.Limits.IsLimit c)
  (s' : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)),
  CategoryTheory.Limits.liftPrecomp h hs hc s' =
    hc.lift
      (CategoryTheory.Limits.PullbackCone.mk
        (hs.lift (CategoryTheory.Limits.Fork.ofι (CategoryTheory.CategoryStruct.comp s'.ι h) ⋯)) s'.ι ⋯)