noncomputable def SimpleGraph.matchingNum {V : Type u_1} (G : SimpleGraph V) : ℕ∞

theorem SimpleGraph.mem_edgeSet_adj {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) {v : V} {e : Sym2 V} (he : e ∈ M.edgeSet) (hve : v ∈ e) : ∃ (w : V), M.Adj v w ∧ e = s(v, w)

theorem SimpleGraph.Subgraph.IsMatching.edgeSet_encard_le_of_isVertexCover {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {M : G.Subgraph} (hM : M.IsMatching) {C : Set V} (hC : G.IsVertexCover C) : M.edgeSet.encard ≤ C.encard

theorem SimpleGraph.matchingNum_le_vertexCoverNum {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} : G.matchingNum ≤ G.vertexCoverNum

def SimpleGraph.alternatingForestSet {V : Type u_1} (G : SimpleGraph V) (M : G.Subgraph) (A : Set V) : Set V

def SimpleGraph.konigCover {V : Type u_1} (G : SimpleGraph V) (M : G.Subgraph) (A B : Set V) : Set V

theorem SimpleGraph.unmatched_A_in_forest {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {M : G.Subgraph} {A : Set V} {v : V} (hvA : v ∈ A) (hvM : v ∉ M.verts) : G.IsInAlternatingForest M A v

theorem SimpleGraph.Walk.edges_takeUntil_isPrefix {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (hw : w ∈ p.support) : (p.takeUntil w hw).edges <+: p.edges

theorem SimpleGraph.alternatingFrom_takeUntil {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {M : G.Subgraph} (halt : p.IsAlternatingFrom M) (hw : w ∈ p.support) : (p.takeUntil w hw).IsAlternatingFrom M

theorem SimpleGraph.forest_edge_not_in_M {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {A B : Set V} (hBip : G.IsBipartiteWith A B) {M : G.Subgraph} (hM : M.IsMatching) {a v w : V} {p : G.Walk a v} (haA : a ∈ A) (haM : a ∉ M.verts) (hvA : v ∈ A) (hpath : p.IsPath) (halt : p.IsAlternatingFrom M) (hadj : G.Adj v w) (hw_supp : w ∉ p.support) : s(v, w) ∉ M.edgeSet

theorem SimpleGraph.konig_cover_isVertexCover {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {A B : Set V} (hBip : G.IsBipartiteWith A B) {M : G.Subgraph} (hM : M.IsMatching) (hMax : M.IsMaxMatching) : G.IsVertexCover (G.konigCover M A B)

theorem SimpleGraph.konig_cover_encard_eq {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {A B : Set V} (hBip : G.IsBipartiteWith A B) {M : G.Subgraph} (hM : M.IsMatching) (hMfin : M.edgeSet.Finite) (hMax : M.IsMaxMatching) : (G.konigCover M A B).encard = M.edgeSet.encard

theorem SimpleGraph.vertexCoverNum_eq_maxMatching_edgeSet {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {A B : Set V} (hBip : G.IsBipartiteWith A B) {M : G.Subgraph} (hM : M.IsMatching) (hMfin : M.edgeSet.Finite) (hMax : M.IsMaxMatching) : G.vertexCoverNum = M.edgeSet.encard

theorem SimpleGraph.konig_theorem {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {A B : Set V} (hBip : G.IsBipartiteWith A B) {M : G.Subgraph} (hM : M.IsMatching) (hMfin : M.edgeSet.Finite) (hMax : M.IsMaxMatching) : G.matchingNum = G.vertexCoverNum