How to compare cardinalities of subgraph vertice sets

Stream: Is there code for X?

[Lessness]

import Mathlib

def IsMaximum {V} [Finite V] {G: SimpleGraph V} {M: SimpleGraph.Subgraph G} (_: M.IsMatching): Prop :=
  ∀ (M': SimpleGraph.Subgraph G), M'.IsMatching →
  ∃ (f: M'.support -> M.support), Function.Injective f

Is such definition okay?

And, if I want to rewrite to version that explicitly compares cardinalities, I get stuck with error (one of two such errors) failed to synthesize instance Fintype M.verts:

import Mathlib

def IsMaximum' {V} [Finite V] {G: SimpleGraph V} {M: SimpleGraph.Subgraph G} (_: M.IsMatching): Prop :=
  ∀ (M': SimpleGraph.Subgraph G), M'.IsMatching →
  Finset.card (Set.toFinset M'.support) ≤ Finset.card (Set.toFinset M.support)

What's the correct/best way to do such direct comparison of cardinalities?

[Lessness]

Changed vertsto support, because verts can be whatever size even if the graph has no edges.

[Kyle Miller]

You can remove Finite V (generally in mathlib we don't include hypotheses that are unnecessary to make the definition, even if the definition is absurd if, for example, V is infinite). There's docs#Set.ncard for getting the cardinality of a Set without any finiteness assumptions (it's defined to be 0 outside the domain of finite sets).

[Lessness]

Thank you!