∀ {α : Type u_2} {J : Type u_1} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeInf α] [inst_3 : OrderTop α] (F : CategoryTheory.Functor J α) (s : CategoryTheory.Limits.Cone F)
  (m : s.pt ⟶ { pt := Finset.univ.inf F.obj, π := { app := fun x => CategoryTheory.homOfLE ⋯, naturality := ⋯ } }.pt),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp m
          ({ pt := Finset.univ.inf F.obj, π := { app := fun x => CategoryTheory.homOfLE ⋯, naturality := ⋯ } }.π.app
            j) =
        s.π.app j) →
    m = CategoryTheory.homOfLE ⋯