def SimpleGraph.augPathLengths {V : Type u_1} (G : SimpleGraph V) (M : G.Subgraph) : Set ℕ∞

noncomputable def SimpleGraph.shortestAugPathLength {V : Type u_1} (G : SimpleGraph V) (M : G.Subgraph) : ℕ∞

structure SimpleGraph.VertexDisjointAugPaths {V : Type u_1} (G : SimpleGraph V) (M : G.Subgraph) (k : ℕ) : Type (max u_1 (u_2 + 1))

• ι : Type u_2
• src : self.ι → V
• tgt : self.ι → V
• path (i : self.ι) : G.Walk (self.src i) (self.tgt i)
• isAug (i : self.ι) : (self.path i).IsAugmentingPath M
• hasLen (i : self.ι) : (self.path i).length = k
• disjoint (i j : self.ι) : i ≠ j → (self.path i).support.Disjoint (self.path j).support

def SimpleGraph.VertexDisjointAugPaths.IsMaximal {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} {k : ℕ} (paths : G.VertexDisjointAugPaths M k) : Prop

def SimpleGraph.IsAugmentationAlongPaths {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M M' : G.Subgraph) {k : ℕ} (paths : G.VertexDisjointAugPaths M k) : Prop

theorem SimpleGraph.symm_diff_graph_decomposition {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (M M' : G.Subgraph) (hM : M.IsMatching) (k : ℕ) (hk : G.shortestAugPathLength M = ↑k) (paths : G.VertexDisjointAugPaths M k) (haug : IsAugmentationAlongPaths M M' paths) {u v : V} (Q : G.Walk u v) (hQ : Q.IsAugmentingPath M') (hle : Q.length ≤ k) : ∃ (n : ℕ) (_ : n ≥ 1) (srcs : Fin n → V) (tgts : Fin n → V) (Rs : (j : Fin n) → G.Walk (srcs j) (tgts j)), (∀ (j : Fin n), (Rs j).IsAugmentingPath M) ∧ ∑ j : Fin n, (Rs j).length ≤ n * k ∧ ∀ (j : Fin n) (i : paths.ι), (Rs j).support.Disjoint (paths.path i).support

theorem SimpleGraph.symm_diff_decomposition_length_bound {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (M M' : G.Subgraph) (hM : M.IsMatching) (k : ℕ) (hk : G.shortestAugPathLength M = ↑k) (paths : G.VertexDisjointAugPaths M k) (haug : IsAugmentationAlongPaths M M' paths) {u v : V} (Q : G.Walk u v) (hQ : Q.IsAugmentingPath M') (hle : Q.length ≤ k) : ∃ (a : V) (b : V) (R : G.Walk a b), R.IsAugmentingPath M ∧ R.length ≤ k ∧ ∀ (i : paths.ι), R.support.Disjoint (paths.path i).support

theorem SimpleGraph.aug_path_length_gt_of_maximal_phase {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M M' : G.Subgraph) (hM : M.IsMatching) (k : ℕ) (hk : G.shortestAugPathLength M = ↑k) (paths : G.VertexDisjointAugPaths M k) (hmax : paths.IsMaximal) (haug : IsAugmentationAlongPaths M M' paths) {u v : V} (Q : G.Walk u v) (hQ : Q.IsAugmentingPath M') : k < Q.length

theorem SimpleGraph.shortest_aug_path_length_strict_increase {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M M' : G.Subgraph) (hM : M.IsMatching) (k : ℕ) (hk : G.shortestAugPathLength M = ↑k) (paths : G.VertexDisjointAugPaths M k) (hmax : paths.IsMaximal) (haug : IsAugmentationAlongPaths M M' paths) : G.shortestAugPathLength M' > ↑k