∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z : C} {f : X ⟶ Y} {g g' : Y ⟶ Z}
  (H : CategoryTheory.IsPullback f f g g') (s : CategoryTheory.Limits.Fork g g')
  (m : s.pt ⟶ (CategoryTheory.Limits.Fork.ofι f ⋯).pt),
  CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Fork.ofι f ⋯).ι = s.ι →
    m = H.isLimit.lift (CategoryTheory.Limits.PullbackCone.mk s.ι s.ι ⋯)