structure SimpleGraph.AlternatingForest {V : Type u_1} (G : SimpleGraph V) (M : G.Subgraph) : Type u_1

• forestVerts : Finset V
• root : V → V
• level : V → ℕ
• roots_unmatched (v : V) : v ∈ self.forestVerts → self.level v = 0 → v ∉ M.verts
• root_mem (v : V) : v ∈ self.forestVerts → self.root v ∈ self.forestVerts
• root_level (v : V) : v ∈ self.forestVerts → self.level (self.root v) = 0
• root_self (v : V) : v ∈ self.forestVerts → (self.root v = v ↔ self.level v = 0)
• odd_level_matched (v : V) : v ∈ self.forestVerts → Odd (self.level v) → v ∈ M.verts
• unmatched_are_roots (v : V) : v ∉ M.verts → v ∈ self.forestVerts
• unmatched_level_zero (v : V) : v ∈ self.forestVerts → v ∉ M.verts → self.level v = 0
• matched_partner_even (v : V) : v ∈ self.forestVerts → Odd (self.level v) → ∀ (w : V), M.Adj v w → w ∈ self.forestVerts ∧ Even (self.level w) ∧ self.root w = self.root v

def SimpleGraph.AlternatingForest.isEvenLevel {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} (F : G.AlternatingForest M) (v : V) : Prop

theorem SimpleGraph.walk_level_induction {V : Type u_1} {G : SimpleGraph V} (M : G.Subgraph) (F : G.AlternatingForest M) (hsat : ∀ (u v : V), G.Adj u v → F.isEvenLevel u → v ∈ F.forestVerts ∧ Odd (F.level v)) {s t : V} (p : G.Walk s t) (halt : p.IsAlternatingFrom M) (hs_forest : s ∈ F.forestVerts) (hs_even : Even (F.level s)) (i : ℕ) : i ≤ p.length → p.getVert i ∈ F.forestVerts ∧ (Even i → Even (F.level (p.getVert i))) ∧ (Odd i → Odd (F.level (p.getVert i)))

theorem SimpleGraph.no_augmenting_path_of_saturated {V : Type u_1} {G : SimpleGraph V} (M : G.Subgraph) (F : G.AlternatingForest M) (hsat : ∀ (u v : V), G.Adj u v → F.isEvenLevel u → v ∈ F.forestVerts ∧ Odd (F.level v)) : ¬G.HasAugmentingPath M

theorem SimpleGraph.edmonds_progress {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsMatching) (F : G.AlternatingForest M) : (∃ (u : V) (v : V), G.Adj u v ∧ F.isEvenLevel u ∧ v ∉ F.forestVerts) ∨ (∃ (u : V) (v : V), G.Adj u v ∧ F.isEvenLevel u ∧ F.isEvenLevel v ∧ F.root u = F.root v) ∨ (∃ (u : V) (v : V), G.Adj u v ∧ F.isEvenLevel u ∧ F.isEvenLevel v ∧ F.root u ≠ F.root v) ∨ M.IsMaxMatching