∀ ⦃J : Type u_1⦄ (F : J → CategoryTheory.Grpd) (s : CategoryTheory.Limits.Fan F)
  (m : s.pt ⟶ (CategoryTheory.Grpd.piLimitFan F).pt),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp m ((CategoryTheory.Grpd.piLimitFan F).proj j) = s.proj j) →
    m = (fun s => CategoryTheory.Functor.pi' fun j => s.proj j) s