Vertex covers for simple graphs exist as SimpleGraph.IsVertexCover.
I suggest we're missing the following definitions:
open Cardinal
def IsMinimalCover (G : SimpleGraph V) (c : Set V) :=
Minimal G.IsVertexCover c
def IsMinimumCover (G : SimpleGraph V) (c : Set V) :=
MinimalFor G.IsVertexCover (#·) c
and basic API for them.