def SimpleGraph.blossomContractMap {V : Type u_1} [DecidableEq V] (B : Finset V) (base : V) : V → V

@[simp]

theorem SimpleGraph.blossomContractMap_mem {V : Type u_1} [DecidableEq V] (B : Finset V) (base v : V) (hv : v ∈ B) : blossomContractMap B base v = base

@[simp]

theorem SimpleGraph.blossomContractMap_not_mem {V : Type u_1} [DecidableEq V] (B : Finset V) (base v : V) (hv : v ∉ B) : blossomContractMap B base v = v

def SimpleGraph.contractBlossom {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (B : Finset V) (base : V) : SimpleGraph V

structure SimpleGraph.IsBlossom {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (M : G.Subgraph) (B : Finset V) (base : V) : Prop

• base_mem : base ∈ B
• card_odd : Odd B.card
• card_ge : B.card ≥ 3
• cycle_exists : ∃ (c : G.Walk base base), c.IsCycle ∧ c.support.toFinset = B
• matched_internal (v : V) : v ∈ B → v ≠ base → ∃ w ∈ B, w ≠ v ∧ M.Adj v w
• stem : ∃ w ∉ B, M.Adj base w

def SimpleGraph.inducedMatchingSubgraph {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) (B : Finset V) (base : V) : (G.contractBlossom B base).Subgraph

theorem SimpleGraph.inducedMatchingSubgraph_isMatching {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsMatching) (B : Finset V) (base : V) (hB : G.IsBlossom M B base) : (inducedMatchingSubgraph M B base).IsMatching

theorem SimpleGraph.blossom_verts_in_M_verts {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) (B : Finset V) (base : V) (hB : G.IsBlossom M B base) (v : V) : v ∈ B → v ∈ M.verts

theorem SimpleGraph.odd_cycle_matching_avoiding_any_vertex {V : Type u_2} [DecidableEq V] [Fintype V] (G : SimpleGraph V) (B : Finset V) (base : V) (hbase : base ∈ B) (hB_odd : Odd B.card) (hB_ge : 3 ≤ B.card) (c : G.Walk base base) (hc : c.IsCycle) (hsupp : c.support.toFinset = B) (v : V) (hv : v ∈ B) : ∃ S ⊆ G.edgeSet, (∀ e ∈ S, ∀ w ∈ e, w ∈ B ∧ w ≠ v) ∧ S.ncard = (B.card - 1) / 2 ∧ ∀ e₁ ∈ S, ∀ e₂ ∈ S, e₁ ≠ e₂ → Disjoint ↑e₁ ↑e₂

theorem SimpleGraph.lift_matching_size {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsMatching) (B : Finset V) (base : V) (hB : G.IsBlossom M B base) (N' : (G.contractBlossom B base).Subgraph) (hN' : N'.IsMatching) : ∃ (N : G.Subgraph), N.IsMatching ∧ N'.edgeSet.ncard + (B.card - 1) / 2 ≤ N.edgeSet.ncard

theorem SimpleGraph.induced_matching_edgeSet_ncard {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsMatching) (B : Finset V) (base : V) (hB : G.IsBlossom M B base) : M.edgeSet.ncard = (inducedMatchingSubgraph M B base).edgeSet.ncard + (B.card - 1) / 2

theorem SimpleGraph.augmenting_path_lift {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsMatching) (B : Finset V) (base : V) (hB : G.IsBlossom M B base) (haug' : (G.contractBlossom B base).HasAugmentingPath (inducedMatchingSubgraph M B base)) : G.HasAugmentingPath M

theorem SimpleGraph.walk_edges_in_contractBlossom {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (B : Finset V) (base : V) {u v : V} (p : G.Walk u v) (hdisjoint : ∀ w ∈ p.support, w ∉ B) (e : Sym2 V) : e ∈ p.edges → e ∈ (G.contractBlossom B base).edgeSet

theorem SimpleGraph.inducedMatching_adj_iff_of_not_mem {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (B : Finset V) (base : V) (hbase : base ∈ B) {a b : V} (ha : a ∉ B) (hb : b ∉ B) (hadj_G : G.Adj a b) : (inducedMatchingSubgraph M B base).Adj a b ↔ M.Adj a b

theorem SimpleGraph.inducedMatching_edgeSet_iff_of_support_disjoint {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (B : Finset V) (base : V) (hbase : base ∈ B) {u v : V} (p : G.Walk u v) (hdisjoint : ∀ w ∈ p.support, w ∉ B) {e : Sym2 V} (he : e ∈ p.edges) : e ∈ (inducedMatchingSubgraph M B base).edgeSet ↔ e ∈ M.edgeSet

theorem SimpleGraph.unmatched_not_in_induced_verts {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (B : Finset V) (base : V) (hbase : base ∈ B) (hM : M.IsMatching) (hB : G.IsBlossom M B base) {w : V} (hw : w ∉ M.verts) (hwB : w ∉ B) : w ∉ (inducedMatchingSubgraph M B base).verts

theorem SimpleGraph.augmenting_path_project {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsMatching) (B : Finset V) (base : V) (hB : G.IsBlossom M B base) (haug : G.HasAugmentingPath M) : (G.contractBlossom B base).HasAugmentingPath (inducedMatchingSubgraph M B base)

theorem SimpleGraph.blossom_shrinking {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsMatching) (B : Finset V) (base : V) (hB : G.IsBlossom M B base) : M.IsMaxMatching ↔ (inducedMatchingSubgraph M B base).IsMaxMatching