[Merged by Bors] - feat(Combinatorics/SimpleGraph): define odd components

Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

@@ -240,6 +240,11 @@ lemma disjiUnion_supp_toFinset_eq_supp_toFinset {G' : SimpleGraph V} (h : G ≤
 
 end Fintype
 
+
+/-- The odd components are the connected components of odd cardinality. This definition excludes
+infinite components. -/
+abbrev oddComponents : Set G.ConnectedComponent := {c : G.ConnectedComponent | Odd c.supp.ncard}
+
 lemma ConnectedComponent.odd_card_supp_iff_odd_subcomponents [Finite V] {G'}
     (h : G ≤ G') (c' : ConnectedComponent G') :
     Odd c'.supp.ncard ↔
@@ -253,8 +258,7 @@ lemma ConnectedComponent.odd_card_supp_iff_odd_subcomponents [Finite V] {G'}
   simp only [Nat.card_eq_fintype_card, Finset.filter_filter]
   rfl
 
-lemma odd_card_iff_odd_components [Finite V] : Odd (Nat.card V) ↔
-    Odd {c : ConnectedComponent G | Odd c.supp.ncard}.ncard := by
+lemma odd_card_iff_odd_components [Finite V] : Odd (Nat.card V) ↔ Odd G.oddComponents.ncard := by
   classical
   cases nonempty_fintype V
   rw [Nat.card_eq_fintype_card]
@@ -268,15 +272,13 @@ lemma odd_card_iff_odd_components [Finite V] : Odd (Nat.card V) ↔
   exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard))
 
 lemma ncard_odd_components_mono [Finite V] {G' : SimpleGraph V} (h : G ≤ G') :
-     {c : ConnectedComponent G' | Odd c.supp.ncard}.ncard
-      ≤ {c : ConnectedComponent G | Odd c.supp.ncard}.ncard := by
+     G'.oddComponents.ncard ≤ G.oddComponents.ncard := by
   have aux (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard) :
       {c' : G.ConnectedComponent | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty := by
     refine Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_
     simpa [-Nat.card_eq_fintype_card, -Set.coe_setOf, h']
       using (c.odd_card_supp_iff_odd_subcomponents _ h).mp hc
-  let f : {c : ConnectedComponent G' | Odd (Nat.card c.supp)} →
-      {c : ConnectedComponent G | Odd (Nat.card c.supp)} :=
+  let f : G'.oddComponents → G.oddComponents :=
     fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.2⟩
   refine Finite.card_le_of_injective f fun c c' fcc' ↦ ?_
   simp only [Subtype.mk.injEq, f] at fcc'

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -276,11 +276,10 @@ lemma even_card_of_isPerfectMatching [Fintype V] [DecidableEq V] [DecidableRel G
   simpa using (hM.induce_connectedComponent_isMatching c).even_card
 
 lemma odd_matches_node_outside [Finite V] {u : Set V}
-    {c : ConnectedComponent (Subgraph.deleteVerts ⊤ u).coe}
-    (hM : M.IsPerfectMatching) (codd : Odd c.supp.ncard) :
-    ∃ᵉ (w ∈ u) (v : ((⊤ : G.Subgraph).deleteVerts u).verts), M.Adj v w ∧ v ∈ c.supp := by
+    (hM : M.IsPerfectMatching) (c : (Subgraph.deleteVerts ⊤ u).coe.oddComponents) :
+    ∃ᵉ (w ∈ u) (v : ((⊤ : G.Subgraph).deleteVerts u).verts), M.Adj v w ∧ v ∈ c.val.supp := by
   by_contra! h
-  have hMmatch : (M.induce c.supp).IsMatching := by
+  have hMmatch : (M.induce c.val.supp).IsMatching := by
     intro v hv
     obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
     obtain ⟨⟨v', hv'⟩, ⟨hv , rfl⟩⟩ := hv
@@ -292,10 +291,10 @@ lemma odd_matches_node_outside [Finite V] {u : Set V}
       Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
       and_true] at hv' ⊢
     trivial
-  apply Nat.not_even_iff_odd.2 codd
-  haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c)).verts := Fintype.ofFinite _
+  apply Nat.not_even_iff_odd.2 c.prop
+  haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c.val)).verts := Fintype.ofFinite _
   classical
-  haveI : Fintype (c.supp) := Fintype.ofFinite _
+  haveI : Fintype (c.val.supp) := Fintype.ofFinite _
   simpa [Subgraph.induce_verts, Subgraph.verts_top, Set.toFinset_image, Nat.card_eq_fintype_card,
     Set.toFinset_image,Finset.card_image_of_injective _ (Subtype.val_injective), Set.toFinset_card,
     ← Set.Nat.card_coe_set_eq] using hMmatch.even_card