def SimpleGraph.Walk.IsAlternatingFrom {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (M : G.Subgraph) : Prop

def SimpleGraph.Walk.IsAugmentingPath {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (M : G.Subgraph) : Prop

theorem SimpleGraph.Walk.edges_getElem_eq {V : Type u_2} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (i : ℕ) (hi : i < p.edges.length) : p.edges[i] = s(p.getVert i, p.getVert (i + 1))

def SimpleGraph.Subgraph.IsMaxMatching {V : Type u_1} {G : SimpleGraph V} (M : G.Subgraph) : Prop

def SimpleGraph.HasAugmentingPath {V : Type u_1} (G : SimpleGraph V) (M : G.Subgraph) : Prop

noncomputable def SimpleGraph.symmDiffMatching {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} {u v : V} (M : G.Subgraph) (p : G.Walk u v) : G.Subgraph

theorem SimpleGraph.augmenting_path_odd_length {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} {u v : V} {M : G.Subgraph} {p : G.Walk u v} (haug : p.IsAugmentingPath M) : Odd p.edges.length

theorem SimpleGraph.edge_incident_of_path {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hpath : p.IsPath) {n : ℕ} (hn_pos : 0 < n) (hn_lt : n < p.length) (z : V) (hz : s(p.getVert n, z) ∈ p.edges) : z = p.getVert (n - 1) ∨ z = p.getVert (n + 1)

theorem SimpleGraph.symmDiffMatching_isMatching {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} {u v : V} (M : G.Subgraph) (hM : M.IsMatching) (p : G.Walk u v) (haug : p.IsAugmentingPath M) : (symmDiffMatching M p).IsMatching

theorem SimpleGraph.symmDiffMatching_edgeSet_ncard {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} {u v : V} (M : G.Subgraph) (hM : M.IsMatching) (p : G.Walk u v) (haug : p.IsAugmentingPath M) (hfin : M.edgeSet.Finite) : M.edgeSet.ncard < (symmDiffMatching M p).edgeSet.ncard

theorem SimpleGraph.augmenting_path_gives_larger_matching {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) (hM : M.IsMatching) {u v : V} (p : G.Walk u v) (haug : p.IsAugmentingPath M) : ∃ (M' : G.Subgraph), M'.IsMatching ∧ M.edgeSet.ncard < M'.edgeSet.ncard

theorem SimpleGraph.matching_verts_twice_edges {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} {M : G.Subgraph} (hM : M.IsMatching) (hfin : M.edgeSet.Finite) : M.verts.ncard = 2 * M.edgeSet.ncard

noncomputable def SimpleGraph.matchingSwapEdge {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (Mstar' : G.Subgraph) (u v w : V) (hMstar' : Mstar'.IsMatching) (hAdj : Mstar'.Adj u v) (hGvw : G.Adj v w) (hw_fresh : w ∉ Mstar'.verts) : G.Subgraph

theorem SimpleGraph.matchingSwapEdge_isMatching {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (Mstar' : G.Subgraph) (u v w : V) (hMstar' : Mstar'.IsMatching) (hAdj : Mstar'.Adj u v) (hGvw : G.Adj v w) (hw_fresh : w ∉ Mstar'.verts) : (matchingSwapEdge Mstar' u v w hMstar' hAdj hGvw hw_fresh).IsMatching

theorem SimpleGraph.matchingSwapEdge_edgeSet_finite {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (Mstar' : G.Subgraph) (u v w : V) (hMstar' : Mstar'.IsMatching) (hAdj : Mstar'.Adj u v) (hGvw : G.Adj v w) (hw_fresh : w ∉ Mstar'.verts) (hfin : Mstar'.edgeSet.Finite) : (matchingSwapEdge Mstar' u v w hMstar' hAdj hGvw hw_fresh).edgeSet.Finite

theorem SimpleGraph.matchingSwapEdge_ncard {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (Mstar' : G.Subgraph) (u v w : V) (hMstar' : Mstar'.IsMatching) (hAdj : Mstar'.Adj u v) (hGvw : G.Adj v w) (hw_fresh : w ∉ Mstar'.verts) (hfin : Mstar'.edgeSet.Finite) (hvw_notMstar : s(v, w) ∉ Mstar'.edgeSet) : (matchingSwapEdge Mstar' u v w hMstar' hAdj hGvw hw_fresh).edgeSet.ncard = Mstar'.edgeSet.ncard

theorem SimpleGraph.matchingSwapEdge_diff_le {n : ℕ} {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (M Mstar' : G.Subgraph) (u v w : V) (hMstar' : Mstar'.IsMatching) (hAdj : Mstar'.Adj u v) (hGvw : G.Adj v w) (hw_fresh : w ∉ Mstar'.verts) (huv_notM : s(u, v) ∉ M.edgeSet) (hvw_inM : s(v, w) ∈ M.edgeSet) (hfin : Mstar'.edgeSet.Finite) (hn : (Mstar'.edgeSet \ M.edgeSet).ncard ≤ n + 1) : ((matchingSwapEdge Mstar' u v w hMstar' hAdj hGvw hw_fresh).edgeSet \ M.edgeSet).ncard ≤ n

theorem SimpleGraph.larger_matching_gives_augmenting_path {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (M Mstar : G.Subgraph) (hM : M.IsMatching) (hMstar : Mstar.IsMatching) (hMfin : M.edgeSet.Finite) (hcard : M.edgeSet.ncard < Mstar.edgeSet.ncard) : G.HasAugmentingPath M

theorem SimpleGraph.not_isMaxMatching_of_hasAugmentingPath {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) (hM : M.IsMatching) (haug : G.HasAugmentingPath M) : ¬M.IsMaxMatching

theorem SimpleGraph.hasAugmentingPath_of_not_isMaxMatching {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) (hM : M.IsMatching) (hMfin : M.edgeSet.Finite) (hnmax : ¬M.IsMaxMatching) : G.HasAugmentingPath M

theorem SimpleGraph.berge_lemma {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) (hM : M.IsMatching) (hMfin : M.edgeSet.Finite) : M.IsMaxMatching ↔ ¬G.HasAugmentingPath M