{α : Sort u} →
  {motive : Lean.Order.CompleteLattice α → Sort u_1} →
    (t : Lean.Order.CompleteLattice α) →
      ([toPartialOrder : Lean.Order.PartialOrder α] →
          (has_sup : ∀ (c : α → Prop), Exists (Lean.Order.is_sup c)) →
            motive { toPartialOrder := toPartialOrder, has_sup := has_sup }) →
        motive t