∀ {X Y Z : Type u_1} (f : X ⟶ Y) {g h : Y ⟶ Z}
  (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h)
  (t : ∀ (y : Y), g y = h y → ∃! x, f x = y) (s : CategoryTheory.Limits.Fork g h),
  CategoryTheory.CategoryStruct.comp (fun i => Classical.choose ⋯) (CategoryTheory.Limits.Fork.ofι f w).ι = s.ι ∧
    ∀
      {m :
        ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
            CategoryTheory.Limits.WalkingParallelPair.zero ⟶
          ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj
                (CategoryTheory.Limits.Fork.ofι f w).pt).obj
            CategoryTheory.Limits.WalkingParallelPair.zero},
      CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Fork.ofι f w).ι = s.ι →
        m = fun i => Classical.choose ⋯