∀ {α : Type u} [inst : CompleteLattice α] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J α), (CategoryTheory.Limits.CompleteLattice.colimitCocone F).cocone.pt = iSup F.obj