∀ {V : Type u_1} {G : SimpleGraph V} [Finite V],
  Even (Nat.card V) →
    ¬G.IsTutteViolator G.universalVerts →
      (∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp) →
        ∃ M, M.IsPerfectMatching