Formalization auxiliary result of Edmonds-Gallai

Stream: graph theory

[Roman Dragnyev]

Hello hello, i'm a masters student doing a research semester; as a part of it i've formalized an auxiliary result (Thm 2.2.3) of the edmonds-gallai theorem from diestels book.

The main results are:

lemma exists_isPerfectMatching_iff_card_eq (h₀ : G.IsMatchableToComponents S)
  (h₁ : ∀ (C : (G.induce Sᶜ).ConnectedComponent), (G.induce Sᶜ).IsFactorCriticalArea C.supp) :
  card S = card (G.induce Sᶜ).ConnectedComponent ↔ ∃ M : Subgraph G, M.IsPerfectMatching := ...

and

theorem aux (G : SimpleGraph V) : ∃ (S : Set V),
  (G.IsMatchableToComponents S) ∧
  (∀ (C : (G.induce Sᶜ).ConnectedComponent), (G.induce Sᶜ).IsFactorCriticalArea C.supp) := ...

where

def IsFactorCriticalArea (G : SimpleGraph V) (S : Set V) : Prop :=
  S.Nonempty ∧ ∀ v ∈ S, ∃ M : G.Subgraph, M.IsMatching ∧ M.support = S \ {v}

def IsMatchableToComponents (S : Set V) : Prop :=
  ∃ (f : S → (G.induce Sᶜ).ConnectedComponent),
  Function.Injective f ∧ (∀ s : S, ∃ y ∈ (f s), G.Adj ↑s ↑y)

My code can be found here "https://github.com/wetpant93/pfs/blob/master/Pfs/edmonds_gallai.lean". It is currently a bit raw - a short summary of my formalization can be found here "https://github.com/wetpant93/pfs/blob/master/Summary-Edmonds-Gallai.pdf"; Given a bit more polish, is there some intrest in this?