diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean index 7aa3f1ffe46bd8..fc95e6e51ddd10 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean @@ -240,21 +240,26 @@ lemma disjiUnion_supp_toFinset_eq_supp_toFinset {G' : SimpleGraph V} (h : G ≤ end Fintype -lemma ConnectedComponent.odd_card_supp_iff_odd_subcomponents [Finite V] {G'} +/-- 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_oddComponents_ncard_subset_supp [Finite V] {G'} (h : G ≤ G') (c' : ConnectedComponent G') : - Odd c'.supp.ncard ↔ - Odd {c : ConnectedComponent G | c.supp ⊆ c'.supp ∧ Odd c.supp.ncard}.ncard := by + Odd {c ∈ G.oddComponents | c.supp ⊆ c'.supp}.ncard ↔ Odd c'.supp.ncard := by simp_rw [← Set.Nat.card_coe_set_eq] classical cases nonempty_fintype V - rw [Nat.card_eq_card_toFinset, ← disjiUnion_supp_toFinset_eq_supp_toFinset h] - simp only [Finset.card_disjiUnion, Set.toFinset_card] + rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h] + simp only [Finset.card_disjiUnion, Set.toFinset_card, Fintype.card_ofFinset] rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset] - simp only [Nat.card_eq_fintype_card, Finset.filter_filter] + congr! 2 + ext c + simp only [Set.toFinset_setOf, mem_filter, mem_univ, true_and, ← Set.ncard_coe_Finset, coe_filter, + mem_supp_iff, and_comm (a := _ ⊆ _)] 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_ncard_oddComponents [Finite V] : Odd G.oddComponents.ncard ↔ Odd (Nat.card V) := by classical cases nonempty_fintype V rw [Nat.card_eq_fintype_card] @@ -265,24 +270,22 @@ lemma odd_card_iff_odd_components [Finite V] : Odd (Nat.card V) ↔ (fun x _ y _ hxy ↦ Set.disjoint_toFinset.mpr (pairwise_disjoint_supp_connectedComponent _ hxy))] simp_rw [Set.toFinset_card, ← Nat.card_eq_fintype_card, ← Finset.coe_filter_univ, Set.ncard_coe_Finset, Set.Nat.card_coe_set_eq] - exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard)) + exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard)).symm -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 +lemma ncard_oddComponents_mono [Finite V] {G' : SimpleGraph V} (h : G ≤ G') : + 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 + {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.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)} := - fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.2⟩ + using (c.odd_oddComponents_ncard_subset_supp _ h).2 hc + let f : G'.oddComponents → G.oddComponents := + fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.1⟩ refine Finite.card_le_of_injective f fun c c' fcc' ↦ ?_ simp only [Subtype.mk.injEq, f] at fcc' exact Subtype.val_injective (ConnectedComponent.eq_of_common_vertex - ((fcc' ▸ (aux c.1 c.2).choose_spec.1) (ConnectedComponent.nonempty_supp _).some_mem) - ((aux c'.1 c'.2).choose_spec.1 (ConnectedComponent.nonempty_supp _).some_mem)) + ((fcc' ▸ (aux c.1 c.2).choose_spec.2) (ConnectedComponent.nonempty_supp _).some_mem) + ((aux c'.1 c'.2).choose_spec.2 (ConnectedComponent.nonempty_supp _).some_mem)) end WalkCounting diff --git a/Mathlib/Combinatorics/SimpleGraph/Matching.lean b/Mathlib/Combinatorics/SimpleGraph/Matching.lean index 9f08e58e0746e5..63804da1d12ce3 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Matching.lean +++ b/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