/- SPDX-FileCopyrightText: 2026 Advameg, Inc. SPDX-License-Identifier: Apache-2.0 -/ import Mathlib.Combinatorics.SimpleGraph.Acyclic import Mathlib.Combinatorics.SimpleGraph.Coloring import Mathlib.Combinatorics.SimpleGraph.ConcreteColorings import Mathlib.Combinatorics.SimpleGraph.Circulant import Mathlib.Combinatorics.SimpleGraph.Hamiltonian import Mathlib.Combinatorics.SimpleGraph.Matching import Mathlib.Combinatorics.SimpleGraph.Metric import Mathlib.Tactic /-! # Brooks Theorem Seed This file prepares a proof-facing statement of Brooks's theorem using mathlib graph coloring and cycle-graph APIs. -/ namespace AtlasKnownTheorems.BrooksTheorem variable {V : Type} [Fintype V] [DecidableEq V] /-- The exceptional odd-cycle graphs in Brooks's theorem. -/ def IsOddCycleGraph (G : SimpleGraph V) : Prop := ∃ n : ℕ, Odd n ∧ 3 ≤ n ∧ Nonempty (G ≃g SimpleGraph.cycleGraph n) /-- Minimum Brooks coloring target. -/ def BrooksTheoremStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → G.Colorable G.maxDegree /-- Remaining Brooks core after the acyclic case is dispatched. -/ def BrooksNonAcyclicStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → G.Colorable G.maxDegree /-- The remaining non-acyclic Brooks core restricted to maximum degree two. -/ def BrooksDegreeTwoStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → G.maxDegree = 2 → G.Colorable G.maxDegree /-- The remaining non-acyclic Brooks core restricted to maximum degree at least three. -/ def BrooksDegreeAtLeastThreeStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → G.Colorable G.maxDegree /-- The high-degree Brooks core when some vertex has degree below `G.maxDegree`. -/ def BrooksHighDegreeNonregularStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → (∃ v : V, G.degree v < G.maxDegree) → G.Colorable G.maxDegree /-- The high-degree Brooks core for regular graphs. -/ def BrooksHighDegreeRegularStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → (∀ v : V, G.degree v = G.maxDegree) → G.Colorable G.maxDegree /-- Regular high-degree endpoint reduced to a deleted-vertex coloring with two equal neighbor colors. -/ def BrooksHighDegreeRegularPairColoringStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → (∀ v : V, G.degree v = G.maxDegree) → ∃ (u v w : V) (hwu : G.Adj w u) (hwv : G.Adj w v), u ≠ v ∧ ∃ C : (G.induce {x | x ≠ w}).Coloring (Fin G.maxDegree), C ⟨u, (G.ne_of_adj hwu).symm⟩ = C ⟨v, (G.ne_of_adj hwv).symm⟩ /-- Regular high-degree endpoint reduced to selecting one of the checked pair-coloring configurations. -/ def BrooksHighDegreeRegularStructuralStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → (∀ v : V, G.degree v = G.maxDegree) → ∃ (u v w : V) (hwu : G.Adj w u) (hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ ((G.induce {x | x ≠ w}).connectedComponentMk ⟨u, (G.ne_of_adj hwu).symm⟩ ≠ (G.induce {x | x ≠ w}).connectedComponentMk ⟨v, (G.ne_of_adj hwv).symm⟩ ∨ ∃ z : V, G.Adj w z ∧ z ≠ u ∧ z ≠ v ∧ ((G.induce {x | x ≠ w}).induce {x : {x // x ≠ w} | x ≠ ⟨u, (G.ne_of_adj hwu).symm⟩ ∧ x ≠ ⟨v, (G.ne_of_adj hwv).symm⟩}).Connected) /-- Regular high-degree connectivity endpoint before the automatic third-neighbor witness is inserted. -/ def BrooksHighDegreeRegularConnectivityStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → (∀ v : V, G.degree v = G.maxDegree) → ∃ (u v w : V) (hwu : G.Adj w u) (hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ ((G.induce {x | x ≠ w}).connectedComponentMk ⟨u, (G.ne_of_adj hwu).symm⟩ ≠ (G.induce {x | x ≠ w}).connectedComponentMk ⟨v, (G.ne_of_adj hwv).symm⟩ ∨ ((G.induce {x | x ≠ w}).induce {x : {x // x ≠ w} | x ≠ ⟨u, (G.ne_of_adj hwu).symm⟩ ∧ x ≠ ⟨v, (G.ne_of_adj hwv).symm⟩}).Connected) /-- The remaining regular high-degree selection endpoint after the cut-vertex branch is removed. -/ def BrooksHighDegreeRegularTwoConnectedSelectionStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → (∀ v : V, G.degree v = G.maxDegree) → (∀ w : V, (G.induce {x | x ≠ w}).Connected) → ∃ (u v w : V) (hwu : G.Adj w u) (hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ ((G.induce {x | x ≠ w}).induce {x : {x // x ≠ w} | x ≠ ⟨u, (G.ne_of_adj hwu).symm⟩ ∧ x ≠ ⟨v, (G.ne_of_adj hwv).symm⟩}).Connected /-- Regular high-degree selection endpoint using the standard Brooks pair-deletion connectivity condition. -/ def BrooksHighDegreeRegularPairDeletionStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → (∀ v : V, G.degree v = G.maxDegree) → (∀ w : V, (G.induce {x | x ≠ w}).Connected) → ∃ (u v w : V) (_hwu : G.Adj w u) (_hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected /-- Pure graph-theoretic endpoint matching the standard Brooks selection lemma: a finite connected non-complete graph with minimum degree at least three and no cut vertex has an induced length-two path whose endpoints can be deleted while leaving a connected graph. -/ def NonseparatingPairDeletionPathStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → (∀ x : V, 3 ≤ G.degree x) → (∀ w : V, (G.induce {x | x ≠ w}).Connected) → ∃ (u v w : V) (_hwu : G.Adj w u) (_hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected /-- Two-vertex-cut subcase of the pure Brooks selection lemma. The complementary case where every pair deletion is connected is closed by `exists_nonseparating_pair_of_forall_pair_deletion_connected`. -/ def NonseparatingPairDeletionTwoCutStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → (∀ x : V, 3 ≤ G.degree x) → (∀ w : V, (G.induce {x | x ≠ w}).Connected) → (∃ a b : V, a ≠ b ∧ ¬ (G.induce {x | x ≠ a ∧ x ≠ b}).Connected) → ∃ (u v w : V) (_hwu : G.Adj w u) (_hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected /-- Remaining two-component subcase of the pure Brooks pair-deletion selection lemma. For the witnessed disconnected pair deletion, there are no three distinct connected components. The complementary three-component case is closed by `exists_nonseparating_pair_of_three_pair_deleted_components`. -/ def NonseparatingPairDeletionTwoComponentStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → (∀ x : V, 3 ≤ G.degree x) → (∀ w : V, (G.induce {x | x ≠ w}).Connected) → ∀ a b : V, a ≠ b → ¬ (G.induce {x | x ≠ a ∧ x ≠ b}).Connected → (∀ c d e : (G.induce {x | x ≠ a ∧ x ≠ b}).ConnectedComponent, c ≠ d → e ≠ c → e ≠ d → False) → ∃ (u v w : V) (_hwu : G.Adj w u) (_hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected /-- Remaining two-component subcase after the retained cut vertices are also assumed nonadjacent. The adjacent retained-cut-vertices case is closed by `exists_nonseparating_pair_of_adj_pair_cut_not_connected`. -/ def NonseparatingPairDeletionTwoComponentNonadjacentStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → (∀ x : V, 3 ≤ G.degree x) → (∀ w : V, (G.induce {x | x ≠ w}).Connected) → ∀ a b : V, a ≠ b → ¬ G.Adj a b → ¬ (G.induce {x | x ≠ a ∧ x ≠ b}).Connected → (∀ c d e : (G.induce {x | x ≠ a ∧ x ≠ b}).ConnectedComponent, c ≠ d → e ≠ c → e ≠ d → False) → ∃ (u v w : V) (_hwu : G.Adj w u) (_hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected /-- Pure graph-theoretic endpoint left by the regular Brooks route: a finite connected non-complete graph whose every single-vertex deletion is connected has an induced path of length two whose vertex deletion leaves a connected graph. -/ def NonseparatingLengthTwoPathStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → (∀ w : V, (G.induce {x | x ≠ w}).Connected) → ∃ (u v w : V) (hwu : G.Adj w u) (hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ ((G.induce {x | x ≠ w}).induce {x : {x // x ≠ w} | x ≠ ⟨u, (G.ne_of_adj hwu).symm⟩ ∧ x ≠ ⟨v, (G.ne_of_adj hwv).symm⟩}).Connected /-- A nonregular high-degree induction endpoint: color the graph after deleting a low-degree vertex. -/ def BrooksHighDegreeDeleteColoringStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → ∀ v : V, G.degree v < G.maxDegree → (G.induce {w | w ≠ v}).Colorable G.maxDegree /-- Component-level endpoint for coloring the graph after deleting a low-degree vertex. -/ def BrooksHighDegreeDeleteComponentColoringStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → G ≠ ⊤ → ¬ IsOddCycleGraph G → ¬ G.IsAcyclic → 3 ≤ G.maxDegree → ∀ v : V, G.degree v < G.maxDegree → ∀ c : (G.induce {w | w ≠ v}).ConnectedComponent, c.toSimpleGraph.Colorable G.maxDegree /-- The cycle-coloring core needed to close the maximum-degree-two Brooks branch. -/ def BrooksSpanningCycleColoringStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G ≠ ⊤ → ¬ IsOddCycleGraph G → (∃ (v : V) (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = Set.univ) → G.maxDegree = 2 → G.Colorable G.maxDegree /-- The remaining structural core for a spanning cycle in maximum degree two. -/ def BrooksSpanningCycleIsoStatement : Prop := ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], (∃ (v : V) (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = Set.univ) → G.maxDegree = 2 → ∃ n : ℕ, 3 ≤ n ∧ Nonempty (G ≃g SimpleGraph.cycleGraph n) /-- Checked statement wrapper for the minimum theorem. -/ theorem brooksTheorem_statement : BrooksTheoremStatement ↔ BrooksTheoremStatement := by rfl omit [DecidableEq V] in lemma colorable_of_fintype_card_le {G : SimpleGraph V} {k : ℕ} (hcard : Fintype.card V ≤ k) : G.Colorable k := SimpleGraph.Colorable.mono hcard (SimpleGraph.colorable_of_fintype G) omit [Fintype V] [DecidableEq V] in lemma colorable_three_of_cycleGraph_iso {G : SimpleGraph V} {n : ℕ} (htwo : 2 ≤ n) (hiso : Nonempty (G ≃g SimpleGraph.cycleGraph n)) : G.Colorable 3 := by obtain ⟨e⟩ := hiso exact SimpleGraph.Colorable.of_hom e.toHom (SimpleGraph.cycleGraph.tricoloring n htwo).colorable omit [Fintype V] [DecidableEq V] in lemma colorable_of_isOddCycleGraph_of_three_le {G : SimpleGraph V} {k : ℕ} (hodd : IsOddCycleGraph G) (hk : 3 ≤ k) : G.Colorable k := by obtain ⟨n, _hoddn, hthree, hiso⟩ := hodd exact (colorable_three_of_cycleGraph_iso (G := G) (n := n) (by omega) hiso).mono hk lemma colorable_of_induce_compl_singleton_colorable_of_degree_lt {G : SimpleGraph V} [DecidableRel G.Adj] (v : V) {k : ℕ} (hcol : (G.induce {w | w ≠ v}).Colorable k) (hdeg : G.degree v < k) : G.Colorable k := by classical obtain ⟨C⟩ := hcol let neighborColors : Finset (Fin k) := (G.neighborFinset v).attach.image (fun w : {x // x ∈ G.neighborFinset v} => C ⟨w.1, (G.ne_of_adj ((G.mem_neighborFinset v w.1).mp w.2)).symm⟩) have hcard_colors : neighborColors.card ≤ G.degree v := by calc neighborColors.card ≤ (G.neighborFinset v).attach.card := Finset.card_image_le _ = (G.neighborFinset v).card := by simp _ = G.degree v := by rw [G.card_neighborFinset_eq_degree] have hcard_lt : neighborColors.card < (Finset.univ : Finset (Fin k)).card := by simpa using hcard_colors.trans_lt hdeg obtain ⟨c, _hcuniv, hcnot⟩ := Finset.exists_mem_notMem_of_card_lt_card (s := neighborColors) (t := (Finset.univ : Finset (Fin k))) hcard_lt have color_mem_of_adj {w : V} (hvw : G.Adj v w) : C ⟨w, (G.ne_of_adj hvw).symm⟩ ∈ neighborColors := by have hwmem : w ∈ G.neighborFinset v := by rw [G.mem_neighborFinset] exact hvw let w' : {x // x ∈ G.neighborFinset v} := ⟨w, hwmem⟩ have hwattach : w' ∈ (G.neighborFinset v).attach := by simp [w'] have hvalue : (fun w : {x // x ∈ G.neighborFinset v} => C ⟨w.1, (G.ne_of_adj ((G.mem_neighborFinset v w.1).mp w.2)).symm⟩) w' = C ⟨w, (G.ne_of_adj hvw).symm⟩ := by simp [w'] exact Finset.mem_image.mpr ⟨w', hwattach, hvalue⟩ refine ⟨SimpleGraph.Coloring.mk (G := G) (fun x => if hx : x = v then c else C ⟨x, hx⟩) ?_⟩ rintro x y hxy by_cases hx : x = v · subst x have hy : y ≠ v := (G.ne_of_adj hxy).symm simp [hy] intro hEq exact hcnot (by simpa [hEq] using color_mem_of_adj hxy) · by_cases hy : y = v · subst y simp [hx] intro hEq exact hcnot (by simpa [← hEq] using color_mem_of_adj hxy.symm) · simp [hx, hy] exact C.valid hxy lemma colorable_of_delete_vertex_coloring_eq_on_neighbors {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} {u v w : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (huv : u ≠ v) (hcolor : ∃ C : (G.induce {x | x ≠ w}).Coloring (Fin k), C ⟨u, (G.ne_of_adj hwu).symm⟩ = C ⟨v, (G.ne_of_adj hwv).symm⟩) (hdeg : G.degree w ≤ k) : G.Colorable k := by classical obtain ⟨C, hCuv⟩ := hcolor let neighborColors : Finset (Fin k) := (G.neighborFinset w).attach.image (fun z : {x // x ∈ G.neighborFinset w} => C ⟨z.1, (G.ne_of_adj ((G.mem_neighborFinset w z.1).mp z.2)).symm⟩) let reducedColors : Finset (Fin k) := ((G.neighborFinset w).erase u).attach.image (fun z : {x // x ∈ (G.neighborFinset w).erase u} => C ⟨z.1, (G.ne_of_adj ((G.mem_neighborFinset w z.1).mp (Finset.mem_of_mem_erase z.2))).symm⟩) have hsubset : neighborColors ⊆ reducedColors := by intro color hcolor_mem rcases Finset.mem_image.mp hcolor_mem with ⟨z, _hzattach, hzcolor⟩ by_cases hzu : z.1 = u · have hv_mem : v ∈ (G.neighborFinset w).erase u := by rw [Finset.mem_erase, G.mem_neighborFinset] exact ⟨huv.symm, hwv⟩ let vz : {x // x ∈ (G.neighborFinset w).erase u} := ⟨v, hv_mem⟩ have hvattach : vz ∈ ((G.neighborFinset w).erase u).attach := by simp [vz] have hvalue : (fun z : {x // x ∈ (G.neighborFinset w).erase u} => C ⟨z.1, (G.ne_of_adj ((G.mem_neighborFinset w z.1).mp (Finset.mem_of_mem_erase z.2))).symm⟩) vz = color := by have hzvalue : C ⟨u, (G.ne_of_adj hwu).symm⟩ = color := by simpa [hzu] using hzcolor exact hCuv.symm.trans hzvalue exact Finset.mem_image.mpr ⟨vz, hvattach, hvalue⟩ · have hz_mem : z.1 ∈ (G.neighborFinset w).erase u := by rw [Finset.mem_erase] exact ⟨hzu, z.2⟩ let z0 : {x // x ∈ (G.neighborFinset w).erase u} := ⟨z.1, hz_mem⟩ have hz0attach : z0 ∈ ((G.neighborFinset w).erase u).attach := by simp [z0] have hvalue : (fun z : {x // x ∈ (G.neighborFinset w).erase u} => C ⟨z.1, (G.ne_of_adj ((G.mem_neighborFinset w z.1).mp (Finset.mem_of_mem_erase z.2))).symm⟩) z0 = color := by simpa [z0] using hzcolor exact Finset.mem_image.mpr ⟨z0, hz0attach, hvalue⟩ have hcard_colors : neighborColors.card ≤ ((G.neighborFinset w).erase u).card := by calc neighborColors.card ≤ reducedColors.card := Finset.card_le_card hsubset _ ≤ ((G.neighborFinset w).erase u).attach.card := Finset.card_image_le _ = ((G.neighborFinset w).erase u).card := by simp have hu_mem : u ∈ G.neighborFinset w := by rw [G.mem_neighborFinset] exact hwu have hdeg_pos : 0 < G.degree w := by rw [← G.card_neighborFinset_eq_degree] exact Finset.card_pos.mpr ⟨u, hu_mem⟩ have hcard_lt : neighborColors.card < (Finset.univ : Finset (Fin k)).card := by rw [Finset.card_univ, Fintype.card_fin] refine hcard_colors.trans_lt ?_ rw [Finset.card_erase_of_mem hu_mem, G.card_neighborFinset_eq_degree] omega obtain ⟨c, _hcuniv, hcnot⟩ := Finset.exists_mem_notMem_of_card_lt_card (s := neighborColors) (t := (Finset.univ : Finset (Fin k))) hcard_lt have color_mem_of_adj {y : V} (hwy : G.Adj w y) : C ⟨y, (G.ne_of_adj hwy).symm⟩ ∈ neighborColors := by have hymem : y ∈ G.neighborFinset w := by rw [G.mem_neighborFinset] exact hwy let yz : {x // x ∈ G.neighborFinset w} := ⟨y, hymem⟩ have hyattach : yz ∈ (G.neighborFinset w).attach := by simp [yz] have hvalue : (fun z : {x // x ∈ G.neighborFinset w} => C ⟨z.1, (G.ne_of_adj ((G.mem_neighborFinset w z.1).mp z.2)).symm⟩) yz = C ⟨y, (G.ne_of_adj hwy).symm⟩ := by simp [yz] exact Finset.mem_image.mpr ⟨yz, hyattach, hvalue⟩ refine ⟨SimpleGraph.Coloring.mk (G := G) (fun x => if hx : x = w then c else C ⟨x, hx⟩) ?_⟩ intro x y hxy by_cases hx : x = w · subst x have hy : y ≠ w := (G.ne_of_adj hxy).symm simp [hy] intro hEq exact hcnot (by simpa [hEq] using color_mem_of_adj hxy) · by_cases hy : y = w · subst y simp [hx] intro hEq exact hcnot (by simpa [← hEq] using color_mem_of_adj hxy.symm) · simp [hx, hy] exact C.valid hxy omit [Fintype V] in lemma colorable_induce_finset_of_erase {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} {s : Finset V} {v : V} (hv : v ∈ s) (hcol : (G.induce ((s.erase v : Finset V) : Set V)).Colorable k) (hdeg : (G.induce ((s : Finset V) : Set V)).degree ⟨v, by simpa using hv⟩ < k) : (G.induce ((s : Finset V) : Set V)).Colorable k := by classical let H : SimpleGraph {x // x ∈ ((s : Finset V) : Set V)} := G.induce ((s : Finset V) : Set V) let vs : {x // x ∈ ((s : Finset V) : Set V)} := ⟨v, by simpa using hv⟩ obtain ⟨C⟩ := hcol let neighborColors : Finset (Fin k) := (H.neighborFinset vs).attach.image (fun w : {x // x ∈ H.neighborFinset vs} => C ⟨w.1.1, by have hadjH : H.Adj vs w.1 := (H.mem_neighborFinset vs w.1).mp w.2 have hne : w.1.1 ≠ v := (G.ne_of_adj hadjH).symm simp [hne, w.1.2]⟩) have hcard_colors : neighborColors.card ≤ H.degree vs := by calc neighborColors.card ≤ (H.neighborFinset vs).attach.card := Finset.card_image_le _ = (H.neighborFinset vs).card := by simp _ = H.degree vs := by rw [H.card_neighborFinset_eq_degree] have hcard_lt : neighborColors.card < (Finset.univ : Finset (Fin k)).card := by simpa [vs] using hcard_colors.trans_lt hdeg obtain ⟨c, _hcuniv, hcnot⟩ := Finset.exists_mem_notMem_of_card_lt_card (s := neighborColors) (t := (Finset.univ : Finset (Fin k))) hcard_lt have color_mem_of_adj {w : {x // x ∈ ((s : Finset V) : Set V)}} (hvw : H.Adj vs w) : C ⟨w.1, by have hne : w.1 ≠ v := (G.ne_of_adj hvw).symm simp [hne, w.2]⟩ ∈ neighborColors := by have hwmem : w ∈ H.neighborFinset vs := (H.mem_neighborFinset vs w).mpr hvw let w0 : {x // x ∈ H.neighborFinset vs} := ⟨w, hwmem⟩ have hwattach : w0 ∈ (H.neighborFinset vs).attach := by simp [w0] have hvalue : (fun w : {x // x ∈ H.neighborFinset vs} => C ⟨w.1.1, by have hadjH : H.Adj vs w.1 := (H.mem_neighborFinset vs w.1).mp w.2 have hne : w.1.1 ≠ v := (G.ne_of_adj hadjH).symm simp [hne, w.1.2]⟩) w0 = C ⟨w.1, by have hne : w.1 ≠ v := (G.ne_of_adj hvw).symm simp [hne, w.2]⟩ := by simp [w0] exact Finset.mem_image.mpr ⟨w0, hwattach, hvalue⟩ refine ⟨SimpleGraph.Coloring.mk (G := H) (fun x => if hx : x.1 = v then c else C ⟨x.1, by simp [hx, x.2]⟩) ?_⟩ rintro x y hxy by_cases hx : x.1 = v · have hy : y.1 ≠ v := by intro hy exact (H.ne_of_adj hxy) (Subtype.ext (hx.trans hy.symm)) simp [hx, hy] intro hEq have hxsub : x = vs := Subtype.ext hx exact hcnot (by simpa [hEq] using color_mem_of_adj (w := y) (by simpa [hxsub] using hxy)) · by_cases hy : y.1 = v · simp [hx, hy] intro hEq have hysub : y = vs := Subtype.ext hy exact hcnot (by simpa [← hEq] using color_mem_of_adj (w := x) (by simpa [hysub] using hxy.symm)) · simp [hx, hy] exact C.valid hxy omit [Fintype V] in lemma exists_coloring_eq_induce_finset_of_erase {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} {s : Finset V} {x u v : V} (hx : x ∈ s) (hu : u ∈ s) (hv : v ∈ s) (hxu : x ≠ u) (hxv : x ≠ v) (hcol : ∃ C : (G.induce (((s.erase x) : Finset V) : Set V)).Coloring (Fin k), C ⟨u, by simp [hxu.symm, hu]⟩ = C ⟨v, by simp [hxv.symm, hv]⟩) (hdeg : (G.induce ((s : Finset V) : Set V)).degree ⟨x, by simpa using hx⟩ < k) : ∃ C : (G.induce ((s : Finset V) : Set V)).Coloring (Fin k), C ⟨u, by simpa using hu⟩ = C ⟨v, by simpa using hv⟩ := by classical let H : SimpleGraph {y // y ∈ ((s : Finset V) : Set V)} := G.induce ((s : Finset V) : Set V) let xs : {y // y ∈ ((s : Finset V) : Set V)} := ⟨x, by simpa using hx⟩ obtain ⟨C, hCuv⟩ := hcol let neighborColors : Finset (Fin k) := (H.neighborFinset xs).attach.image (fun y : {z // z ∈ H.neighborFinset xs} => C ⟨y.1.1, by have hadjH : H.Adj xs y.1 := (H.mem_neighborFinset xs y.1).mp y.2 have hy_ne : y.1.1 ≠ x := (G.ne_of_adj hadjH).symm simp [hy_ne, y.1.2]⟩) have hcard_colors : neighborColors.card ≤ H.degree xs := by calc neighborColors.card ≤ (H.neighborFinset xs).attach.card := Finset.card_image_le _ = (H.neighborFinset xs).card := by simp _ = H.degree xs := by rw [H.card_neighborFinset_eq_degree] have hcard_lt : neighborColors.card < (Finset.univ : Finset (Fin k)).card := by simpa [xs] using hcard_colors.trans_lt hdeg obtain ⟨c, _hcuniv, hcnot⟩ := Finset.exists_mem_notMem_of_card_lt_card (s := neighborColors) (t := (Finset.univ : Finset (Fin k))) hcard_lt have color_mem_of_adj {y : {z // z ∈ ((s : Finset V) : Set V)}} (hxy : H.Adj xs y) : C ⟨y.1, by have hy_ne : y.1 ≠ x := (G.ne_of_adj hxy).symm simp [hy_ne, y.2]⟩ ∈ neighborColors := by have hymem : y ∈ H.neighborFinset xs := (H.mem_neighborFinset xs y).mpr hxy let y0 : {z // z ∈ H.neighborFinset xs} := ⟨y, hymem⟩ have hyattach : y0 ∈ (H.neighborFinset xs).attach := by simp [y0] have hvalue : (fun y : {z // z ∈ H.neighborFinset xs} => C ⟨y.1.1, by have hadjH : H.Adj xs y.1 := (H.mem_neighborFinset xs y.1).mp y.2 have hy_ne : y.1.1 ≠ x := (G.ne_of_adj hadjH).symm simp [hy_ne, y.1.2]⟩) y0 = C ⟨y.1, by have hy_ne : y.1 ≠ x := (G.ne_of_adj hxy).symm simp [hy_ne, y.2]⟩ := by simp [y0] exact Finset.mem_image.mpr ⟨y0, hyattach, hvalue⟩ refine ⟨SimpleGraph.Coloring.mk (G := H) (fun y => if hy : y.1 = x then c else C ⟨y.1, by simp [hy, y.2]⟩) ?_, ?_⟩ · rintro y z hyz by_cases hy : y.1 = x · have hz : z.1 ≠ x := by intro hz exact (H.ne_of_adj hyz) (Subtype.ext (hy.trans hz.symm)) simp [hy, hz] intro hEq have hysub : y = xs := Subtype.ext hy exact hcnot (by simpa [hEq] using color_mem_of_adj (y := z) (by simpa [hysub] using hyz)) · by_cases hz : z.1 = x · simp [hy, hz] intro hEq have hzsub : z = xs := Subtype.ext hz exact hcnot (by simpa [← hEq] using color_mem_of_adj (y := y) (by simpa [hzsub] using hyz.symm)) · simp [hy, hz] exact C.valid hyz · simpa [SimpleGraph.Coloring.mk, hxu.symm, hxv.symm] using hCuv omit [Fintype V] in lemma exists_coloring_eq_induce_finset_of_forall_exists_low_degree_except_pair {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} {u v : V} (hk : 0 < k) (hnadj : ¬ G.Adj u v) (h : ∀ s : Finset V, u ∈ s → v ∈ s → (∃ x ∈ s, x ≠ u ∧ x ≠ v) → ∃ x : {y // y ∈ s}, x.1 ≠ u ∧ x.1 ≠ v ∧ (G.induce ((s : Finset V) : Set V)).degree x < k) (s : Finset V) (hu : u ∈ s) (hv : v ∈ s) : ∃ C : (G.induce ((s : Finset V) : Set V)).Coloring (Fin k), C ⟨u, by simpa using hu⟩ = C ⟨v, by simpa using hv⟩ := by classical let P : ℕ → Prop := fun n => ∀ (s : Finset V), s.card = n → (hu : u ∈ s) → (hv : v ∈ s) → ∃ C : (G.induce ((s : Finset V) : Set V)).Coloring (Fin k), C ⟨u, hu⟩ = C ⟨v, hv⟩ have hP : ∀ n, P n := by intro n induction n using Nat.strong_induction_on with | h n ih => intro s hs_card hu hv by_cases hother : ∃ x ∈ s, x ≠ u ∧ x ≠ v · obtain ⟨x, hxu, hxv, hxdeg⟩ := h s hu hv hother have hcard_erase : (s.erase x.1).card < n := by rw [← hs_card] exact Finset.card_erase_lt_of_mem x.2 have hu_erase : u ∈ s.erase x.1 := by rw [Finset.mem_erase] exact ⟨hxu.symm, hu⟩ have hv_erase : v ∈ s.erase x.1 := by rw [Finset.mem_erase] exact ⟨hxv.symm, hv⟩ have hcol_erase : ∃ C : (G.induce ((((s.erase x.1) : Finset V)) : Set V)).Coloring (Fin k), C ⟨u, hu_erase⟩ = C ⟨v, hv_erase⟩ := ih (s.erase x.1).card hcard_erase (s.erase x.1) rfl hu_erase hv_erase exact exists_coloring_eq_induce_finset_of_erase (G := G) (k := k) (s := s) (x := x.1) (u := u) (v := v) x.2 hu hv hxu hxv hcol_erase hxdeg · have hmem_uv {y : V} (hy : y ∈ s) : y = u ∨ y = v := by by_cases hyu : y = u · exact Or.inl hyu · by_cases hyv : y = v · exact Or.inr hyv · exact False.elim (hother ⟨y, hy, hyu, hyv⟩) let c : Fin k := ⟨0, hk⟩ refine ⟨SimpleGraph.Coloring.mk (G := G.induce ((s : Finset V) : Set V)) (fun _ => c) ?_, ?_⟩ · intro y z hyz _hEq rcases hmem_uv y.2 with hyu | hyv <;> rcases hmem_uv z.2 with hzu | hzv · exact (G.ne_of_adj hyz) (hyu.trans hzu.symm) · exact hnadj (by simpa [hyu, hzv] using hyz) · exact hnadj (by simpa [hyv, hzu] using hyz.symm) · exact (G.ne_of_adj hyz) (hyv.trans hzv.symm) · rfl exact hP s.card s rfl hu hv omit [Fintype V] in lemma colorable_induce_finset_of_forall_exists_low_degree {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} (h : ∀ s : Finset V, s.Nonempty → ∃ v : {x // x ∈ s}, (G.induce ((s : Finset V) : Set V)).degree v < k) (s : Finset V) : (G.induce ((s : Finset V) : Set V)).Colorable k := by classical let P : ℕ → Prop := fun n => ∀ s : Finset V, s.card = n → (G.induce ((s : Finset V) : Set V)).Colorable k have hP : ∀ n, P n := by intro n induction n using Nat.strong_induction_on with | h n ih => intro s hs_card by_cases hs_nonempty : s.Nonempty · obtain ⟨v, hvdeg⟩ := h s hs_nonempty have hcard_erase : (s.erase v.1).card < n := by rw [← hs_card] exact Finset.card_erase_lt_of_mem v.2 have hcol_erase : (G.induce (((s.erase v.1) : Finset V) : Set V)).Colorable k := ih (s.erase v.1).card hcard_erase (s.erase v.1) rfl exact colorable_induce_finset_of_erase (G := G) (k := k) (s := s) (v := v.1) v.2 hcol_erase hvdeg · haveI : IsEmpty {x // x ∈ ((s : Finset V) : Set V)} := ⟨fun x => hs_nonempty ⟨x.1, x.2⟩⟩ exact SimpleGraph.Colorable.of_isEmpty k exact hP s.card s rfl lemma colorable_of_forall_finset_exists_low_degree {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} (h : ∀ s : Finset V, s.Nonempty → ∃ v : {x // x ∈ s}, (G.induce ((s : Finset V) : Set V)).degree v < k) : G.Colorable k := by classical obtain ⟨C⟩ := colorable_induce_finset_of_forall_exists_low_degree (G := G) (k := k) h Finset.univ refine ⟨SimpleGraph.Coloring.mk (G := G) (fun x => C ⟨x, by simp⟩) ?_⟩ intro x y hxy exact C.valid hxy lemma degree_induce_le {G : SimpleGraph V} [DecidableRel G.Adj] {s : Set V} [DecidablePred (· ∈ s)] (v : s) : (G.induce s).degree v ≤ G.degree v := by classical rw [← (G.induce s).card_neighborFinset_eq_degree v, ← G.card_neighborFinset_eq_degree v] calc ((G.induce s).neighborFinset v).card = (((G.induce s).neighborFinset v).map (.subtype (· ∈ s))).card := by rw [Finset.card_map] _ = (G.neighborFinset v ∩ s.toFinset).card := by simpa using congrArg Finset.card (G.map_neighborFinset_induce v) _ ≤ (G.neighborFinset v).card := by exact Finset.card_le_card Finset.inter_subset_left lemma degree_induce_lt_of_adj_notMem {G : SimpleGraph V} [DecidableRel G.Adj] {s : Set V} [DecidablePred (· ∈ s)] {x y : V} (hx : x ∈ s) (hy : y ∉ s) (hxy : G.Adj x y) : (G.induce s).degree ⟨x, hx⟩ < G.degree x := by classical rw [← (G.induce s).card_neighborFinset_eq_degree ⟨x, hx⟩, ← G.card_neighborFinset_eq_degree x] calc ((G.induce s).neighborFinset ⟨x, hx⟩).card = (((G.induce s).neighborFinset ⟨x, hx⟩).map (.subtype (· ∈ s))).card := by rw [Finset.card_map] _ = (G.neighborFinset x ∩ s.toFinset).card := by simpa using congrArg Finset.card (G.map_neighborFinset_induce ⟨x, hx⟩) _ < (G.neighborFinset x).card := by apply Finset.card_lt_card rw [Finset.ssubset_iff_subset_ne] refine ⟨Finset.inter_subset_left, ?_⟩ intro heq have hy_neigh : y ∈ G.neighborFinset x := by rw [G.mem_neighborFinset] exact hxy have hy_inter : y ∈ G.neighborFinset x ∩ s.toFinset := by simpa [heq] using hy_neigh exact hy (by simpa using (Finset.mem_of_mem_inter_right hy_inter)) omit [DecidableEq V] in lemma degree_induce_finset_le {G : SimpleGraph V} [DecidableRel G.Adj] {s : Finset V} (v : {x // x ∈ ((s : Finset V) : Set V)}) : (G.induce ((s : Finset V) : Set V)).degree v ≤ G.degree v.1 := by classical let H : SimpleGraph {x // x ∈ ((s : Finset V) : Set V)} := G.induce ((s : Finset V) : Set V) let f : H.neighborSet v → G.neighborSet v.1 := fun y => ⟨y.1.1, y.2⟩ have hf_inj : Function.Injective f := by intro y z hyz have hval : y.1.1 = z.1.1 := congrArg (fun q : G.neighborSet v.1 => q.1) hyz exact Subtype.ext (Subtype.ext hval) have hcard : Fintype.card (H.neighborSet v) ≤ Fintype.card (G.neighborSet v.1) := Fintype.card_le_of_injective f hf_inj rw [← H.card_neighborFinset_eq_degree v, ← G.card_neighborFinset_eq_degree v.1] rwa [← Set.toFinset_card (H.neighborSet v), ← Set.toFinset_card (G.neighborSet v.1)] at hcard omit [DecidableEq V] in lemma degree_induce_finset_lt_of_adj_notMem {G : SimpleGraph V} [DecidableRel G.Adj] {s : Finset V} {x y : V} (hx : x ∈ s) (hy : y ∉ s) (hxy : G.Adj x y) : (G.induce ((s : Finset V) : Set V)).degree ⟨x, by simpa using hx⟩ < G.degree x := by classical let H : SimpleGraph {x // x ∈ ((s : Finset V) : Set V)} := G.induce ((s : Finset V) : Set V) rw [← H.card_neighborFinset_eq_degree ⟨x, by simpa using hx⟩, ← G.card_neighborFinset_eq_degree x] calc (H.neighborFinset ⟨x, by simpa using hx⟩).card = ((H.neighborFinset ⟨x, by simpa using hx⟩).map (.subtype (· ∈ ((s : Finset V) : Set V)))).card := by rw [Finset.card_map] _ < (G.neighborFinset x).card := by apply Finset.card_lt_card rw [Finset.ssubset_iff_subset_ne] refine ⟨?_, ?_⟩ · intro z hz obtain ⟨z', hz', rfl⟩ := Finset.mem_map.mp hz rw [G.mem_neighborFinset] exact (H.mem_neighborFinset ⟨x, by simpa using hx⟩ z').mp hz' · intro heq have hy_neigh : y ∈ G.neighborFinset x := by rw [G.mem_neighborFinset] exact hxy have hy_image : y ∈ (H.neighborFinset ⟨x, by simpa using hx⟩).map (.subtype (· ∈ ((s : Finset V) : Set V))) := by simpa [heq] using hy_neigh obtain ⟨z, _hz, hz_eq⟩ := Finset.mem_map.mp hy_image have hy_mem : y ∈ s := by rw [← hz_eq] exact z.2 exact hy hy_mem lemma exists_low_degree_outside_pair_of_connected_compl_pair {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} {u v z : V} (hconn : (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) (hdeg_le : ∀ x : V, G.degree x ≤ k) (hzu : z ≠ u) (hzv : z ≠ v) (hzdeg : G.degree z < k) : ∀ s : Finset V, u ∈ s → v ∈ s → (∃ x ∈ s, x ≠ u ∧ x ≠ v) → ∃ x : {y // y ∈ s}, x.1 ≠ u ∧ x.1 ≠ v ∧ (G.induce ((s : Finset V) : Set V)).degree x < k := by classical intro s _hu _hv hother by_cases hfull : ∀ y : V, y ≠ u → y ≠ v → y ∈ s · have hzmem : z ∈ s := hfull z hzu hzv refine ⟨⟨z, hzmem⟩, hzu, hzv, ?_⟩ exact (degree_induce_finset_le (G := G) (s := s) ⟨z, by simpa using hzmem⟩).trans_lt hzdeg · push Not at hfull obtain ⟨y, hyu, hyv, hyns⟩ := hfull obtain ⟨x, hxs, hxu, hxv⟩ := hother let K : SimpleGraph {a // a ≠ u ∧ a ≠ v} := G.induce {a | a ≠ u ∧ a ≠ v} let a : {a // a ≠ u ∧ a ≠ v} := ⟨x, hxu, hxv⟩ let b : {a // a ≠ u ∧ a ≠ v} := ⟨y, hyu, hyv⟩ let S : Set {a // a ≠ u ∧ a ≠ v} := {a | a.1 ∈ s} obtain ⟨p⟩ := hconn a b obtain ⟨d, _hd, hfstS, hsnd_notS⟩ := p.exists_boundary_dart S (by simpa [S, a] using hxs) (by simpa [S, b] using hyns) refine ⟨⟨d.fst.1, by simpa [S] using hfstS⟩, d.fst.2.1, d.fst.2.2, ?_⟩ have hlt : (G.induce ((s : Finset V) : Set V)).degree ⟨d.fst.1, by simpa [S] using hfstS⟩ < G.degree d.fst.1 := degree_induce_finset_lt_of_adj_notMem (G := G) (s := s) (by simpa [S] using hfstS) (by simpa [S] using hsnd_notS) (by simpa [K] using d.adj) exact hlt.trans_le (hdeg_le d.fst.1) lemma exists_low_degree_outside_pair_of_connected_delete_pair {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} {u v w z : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (hwz : G.Adj w z) (hconn_pair : (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) (hdeg_le : ∀ x : V, G.degree x ≤ k) (hzu : z ≠ u) (hzv : z ≠ v) : ∀ s : Finset {x // x ≠ w}, (⟨u, (G.ne_of_adj hwu).symm⟩ : {x // x ≠ w}) ∈ s → (⟨v, (G.ne_of_adj hwv).symm⟩ : {x // x ≠ w}) ∈ s → (∃ x ∈ s, x ≠ ⟨u, (G.ne_of_adj hwu).symm⟩ ∧ x ≠ ⟨v, (G.ne_of_adj hwv).symm⟩) → ∃ x : {y // y ∈ s}, x.1 ≠ ⟨u, (G.ne_of_adj hwu).symm⟩ ∧ x.1 ≠ ⟨v, (G.ne_of_adj hwv).symm⟩ ∧ ((G.induce {x | x ≠ w}).induce ((s : Finset {x // x ≠ w}) : Set {x // x ≠ w})).degree x < k := by classical let H : SimpleGraph {x // x ≠ w} := G.induce {x | x ≠ w} let K : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} let uH : {x // x ≠ w} := ⟨u, (G.ne_of_adj hwu).symm⟩ let vH : {x // x ≠ w} := ⟨v, (G.ne_of_adj hwv).symm⟩ intro s _hu_mem _hv_mem hother by_cases hfull : ∀ (y : V) (hyw : y ≠ w) (hyu : y ≠ u) (hyv : y ≠ v), (⟨y, hyw⟩ : {x // x ≠ w}) ∈ s · have hzw : z ≠ w := (G.ne_of_adj hwz).symm let zH : {x // x ≠ w} := ⟨z, hzw⟩ have hzmem : zH ∈ s := hfull z hzw hzu hzv refine ⟨⟨zH, hzmem⟩, ?_, ?_, ?_⟩ · intro h exact hzu (congrArg Subtype.val h) · intro h exact hzv (congrArg Subtype.val h) · have hle : (H.induce ((s : Finset {x // x ≠ w}) : Set {x // x ≠ w})).degree ⟨zH, hzmem⟩ ≤ H.degree zH := degree_induce_finset_le (G := H) (s := s) ⟨zH, hzmem⟩ have hlt : H.degree zH < G.degree z := degree_induce_lt_of_adj_notMem (G := G) (s := {x | x ≠ w}) zH.2 (by simp) hwz.symm exact hle.trans_lt (hlt.trans_le (hdeg_le z)) · push Not at hfull obtain ⟨y, hyw, hyu, hyv, hyns⟩ := hfull obtain ⟨xH, hxs, hxuH, hxvH⟩ := hother have hx_ne_u : xH.1 ≠ u := by intro h exact hxuH (Subtype.ext h) have hx_ne_v : xH.1 ≠ v := by intro h exact hxvH (Subtype.ext h) let a : {x // x ≠ u ∧ x ≠ v} := ⟨xH.1, hx_ne_u, hx_ne_v⟩ let b : {x // x ≠ u ∧ x ≠ v} := ⟨y, hyu, hyv⟩ let S : Set {x // x ≠ u ∧ x ≠ v} := {q | ∃ hqw : q.1 ≠ w, (⟨q.1, hqw⟩ : {x // x ≠ w}) ∈ s} have haS : a ∈ S := ⟨xH.2, hxs⟩ have hbS : b ∉ S := by rintro ⟨hyw', hy_mem⟩ exact hyns (by simpa [b] using hy_mem) obtain ⟨p⟩ := hconn_pair a b obtain ⟨d, _hdmem, hfstS, hsnd_notS⟩ := p.exists_boundary_dart S haS hbS obtain ⟨hfst_ne_w, hfst_mem_s⟩ := hfstS let fstH : {x // x ≠ w} := ⟨d.fst.1, hfst_ne_w⟩ have hfst_ne_uH : fstH ≠ uH := by intro h exact d.fst.2.1 (congrArg Subtype.val h) have hfst_ne_vH : fstH ≠ vH := by intro h exact d.fst.2.2 (congrArg Subtype.val h) refine ⟨⟨fstH, hfst_mem_s⟩, hfst_ne_uH, hfst_ne_vH, ?_⟩ by_cases hsndw : d.snd.1 = w · have hle : (H.induce ((s : Finset {x // x ≠ w}) : Set {x // x ≠ w})).degree ⟨fstH, hfst_mem_s⟩ ≤ H.degree fstH := degree_induce_finset_le (G := H) (s := s) ⟨fstH, hfst_mem_s⟩ have hlt : H.degree fstH < G.degree fstH.1 := have hfstw : G.Adj fstH.1 w := by have hadjG : G.Adj d.fst.1 d.snd.1 := by simpa [K] using d.adj change G.Adj d.fst.1 w simpa [hsndw] using hadjG degree_induce_lt_of_adj_notMem (G := G) (s := {x | x ≠ w}) fstH.2 (by simp) hfstw exact hle.trans_lt (hlt.trans_le (hdeg_le fstH.1)) · let sndH : {x // x ≠ w} := ⟨d.snd.1, hsndw⟩ have hsnd_not_s : sndH ∉ s := by intro hs exact hsnd_notS ⟨hsndw, by simpa [sndH] using hs⟩ have hlt : (H.induce ((s : Finset {x // x ≠ w}) : Set {x // x ≠ w})).degree ⟨fstH, hfst_mem_s⟩ < H.degree fstH := degree_induce_finset_lt_of_adj_notMem (G := H) (s := s) hfst_mem_s hsnd_not_s (show H.Adj fstH sndH from d.adj) have hHle : H.degree fstH ≤ k := (degree_induce_le (G := G) (s := {x | x ≠ w}) fstH).trans (hdeg_le fstH.1) exact hlt.trans_le hHle lemma maxDegree_induce_le {G : SimpleGraph V} [DecidableRel G.Adj] (s : Set V) [DecidablePred (· ∈ s)] : (G.induce s).maxDegree ≤ G.maxDegree := by exact (G.induce s).maxDegree_le_of_forall_degree_le G.maxDegree fun v => (degree_induce_le (G := G) v).trans (G.degree_le_maxDegree v) omit [Fintype V] in lemma exists_adj_deleted_vertex_of_component {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) (v : V) (c : (G.induce {w | w ≠ v}).ConnectedComponent) : ∃ x : {w // w ≠ v}, x ∈ c.supp ∧ G.Adj x.1 v := by classical let H : SimpleGraph {w // w ≠ v} := G.induce {w | w ≠ v} obtain ⟨x, hxc⟩ := c.nonempty_supp let S : Set V := {z | ∃ hz : z ≠ v, (⟨z, hz⟩ : {w // w ≠ v}) ∈ c.supp} have hxS : x.1 ∈ S := ⟨x.2, hxc⟩ have hvS : v ∉ S := by rintro ⟨hv, _⟩ exact hv rfl obtain ⟨p⟩ := hconn x.1 v obtain ⟨d, _hdmem, hfstS, hsnd_notS⟩ := p.exists_boundary_dart S hxS hvS obtain ⟨hfst_ne, hfst_c⟩ := hfstS have hsnd_eq : d.snd = v := by by_contra hsnd_ne have hsnd_c : (⟨d.snd, hsnd_ne⟩ : {w // w ≠ v}) ∈ c.supp := by exact c.mem_supp_of_adj_mem_supp hfst_c (show H.Adj ⟨d.fst, hfst_ne⟩ ⟨d.snd, hsnd_ne⟩ from d.adj) exact hsnd_notS ⟨hsnd_ne, hsnd_c⟩ exact ⟨⟨d.fst, hfst_ne⟩, hfst_c, by simpa [hsnd_eq] using d.adj⟩ omit [Fintype V] in lemma exists_adj_deleted_pair_vertex_of_component {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) (u v : V) (c : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent) : ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ (G.Adj x.1 u ∨ G.Adj x.1 v) := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨x, hxc⟩ := c.nonempty_supp let S : Set V := {z | ∃ hz : z ≠ u ∧ z ≠ v, (⟨z, hz⟩ : {x // x ≠ u ∧ x ≠ v}) ∈ c.supp} have hxS : x.1 ∈ S := ⟨x.2, hxc⟩ have huS : u ∉ S := by rintro ⟨hu, _⟩ exact hu.1 rfl obtain ⟨p⟩ := hconn x.1 u obtain ⟨d, _hdmem, hfstS, hsnd_notS⟩ := p.exists_boundary_dart S hxS huS obtain ⟨hfst_ne, hfst_c⟩ := hfstS have hsnd_eq_or : d.snd = u ∨ d.snd = v := by by_cases hsndu : d.snd = u · exact Or.inl hsndu · by_cases hsndv : d.snd = v · exact Or.inr hsndv · have hsnd_c : (⟨d.snd, hsndu, hsndv⟩ : {x // x ≠ u ∧ x ≠ v}) ∈ c.supp := by exact c.mem_supp_of_adj_mem_supp hfst_c (show H.Adj ⟨d.fst, hfst_ne⟩ ⟨d.snd, hsndu, hsndv⟩ from d.adj) exact False.elim (hsnd_notS ⟨⟨hsndu, hsndv⟩, hsnd_c⟩) refine ⟨⟨d.fst, hfst_ne⟩, hfst_c, ?_⟩ rcases hsnd_eq_or with rfl | rfl · exact Or.inl d.adj · exact Or.inr d.adj omit [Fintype V] in lemma exists_adj_left_deleted_pair_vertex_of_component {G : SimpleGraph V} [DecidableRel G.Adj] {u v : V} (huv : u ≠ v) (hconn : (G.induce {x | x ≠ v}).Connected) (c : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent) : ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 u := by classical let K : SimpleGraph {x // x ≠ v} := G.induce {x | x ≠ v} let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} let uK : {x // x ≠ v} := ⟨u, huv⟩ obtain ⟨x, hxc⟩ := c.nonempty_supp let xK : {x // x ≠ v} := ⟨x.1, x.2.2⟩ let S : Set {x // x ≠ v} := {z | ∃ hzu : z.1 ≠ u, (⟨z.1, hzu, z.2⟩ : {x // x ≠ u ∧ x ≠ v}) ∈ c.supp} have hxS : xK ∈ S := ⟨x.2.1, hxc⟩ have huS : uK ∉ S := by rintro ⟨hu, _⟩ exact hu rfl obtain ⟨p⟩ := hconn xK uK obtain ⟨d, _hdmem, hfstS, hsnd_notS⟩ := p.exists_boundary_dart S hxS huS obtain ⟨hfst_ne_u, hfst_c⟩ := hfstS have hsnd_eq : d.snd = uK := by by_contra hsnd_ne have hsnd_ne_u : d.snd.1 ≠ u := by intro h exact hsnd_ne (Subtype.ext h) have hsnd_c : (⟨d.snd.1, hsnd_ne_u, d.snd.2⟩ : {x // x ≠ u ∧ x ≠ v}) ∈ c.supp := by exact c.mem_supp_of_adj_mem_supp hfst_c (show H.Adj ⟨d.fst.1, hfst_ne_u, d.fst.2⟩ ⟨d.snd.1, hsnd_ne_u, d.snd.2⟩ from d.adj) exact hsnd_notS ⟨hsnd_ne_u, hsnd_c⟩ refine ⟨⟨d.fst.1, hfst_ne_u, d.fst.2⟩, hfst_c, ?_⟩ simpa [K, uK, hsnd_eq] using d.adj omit [Fintype V] in lemma exists_adj_right_deleted_pair_vertex_of_component {G : SimpleGraph V} [DecidableRel G.Adj] {u v : V} (huv : u ≠ v) (hconn : (G.induce {x | x ≠ u}).Connected) (c : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent) : ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 v := by classical let K : SimpleGraph {x // x ≠ u} := G.induce {x | x ≠ u} let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} let vK : {x // x ≠ u} := ⟨v, huv.symm⟩ obtain ⟨x, hxc⟩ := c.nonempty_supp let xK : {x // x ≠ u} := ⟨x.1, x.2.1⟩ let S : Set {x // x ≠ u} := {z | ∃ hzv : z.1 ≠ v, (⟨z.1, z.2, hzv⟩ : {x // x ≠ u ∧ x ≠ v}) ∈ c.supp} have hxS : xK ∈ S := ⟨x.2.2, hxc⟩ have hvS : vK ∉ S := by rintro ⟨hv, _⟩ exact hv rfl obtain ⟨p⟩ := hconn xK vK obtain ⟨d, _hdmem, hfstS, hsnd_notS⟩ := p.exists_boundary_dart S hxS hvS obtain ⟨hfst_ne_v, hfst_c⟩ := hfstS have hsnd_eq : d.snd = vK := by by_contra hsnd_ne have hsnd_ne_v : d.snd.1 ≠ v := by intro h exact hsnd_ne (Subtype.ext h) have hsnd_c : (⟨d.snd.1, d.snd.2, hsnd_ne_v⟩ : {x // x ≠ u ∧ x ≠ v}) ∈ c.supp := by exact c.mem_supp_of_adj_mem_supp hfst_c (show H.Adj ⟨d.fst.1, d.fst.2, hfst_ne_v⟩ ⟨d.snd.1, d.snd.2, hsnd_ne_v⟩ from d.adj) exact hsnd_notS ⟨hsnd_ne_v, hsnd_c⟩ refine ⟨⟨d.fst.1, d.fst.2, hfst_ne_v⟩, hfst_c, ?_⟩ simpa [K, vK, hsnd_eq] using d.adj omit [Fintype V] in lemma exists_adj_both_deleted_pair_vertex_of_component {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (huv : u ≠ v) (c : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent) : (∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 u) ∧ ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 v := ⟨exists_adj_left_deleted_pair_vertex_of_component (G := G) huv (hall_connected v) c, exists_adj_right_deleted_pair_vertex_of_component (G := G) huv (hall_connected u) c⟩ lemma exists_ne_mem_deleted_pair_component_of_three_le_degree {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) {u v : V} (c : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent) : ∃ x y : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ y ∈ c.supp ∧ x ≠ y := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨x, hxc⟩ := c.nonempty_supp by_cases htwo : ∃ y : {x // x ≠ u ∧ x ≠ v}, y ∈ c.supp ∧ y ≠ x · obtain ⟨y, hyc, hyx⟩ := htwo exact ⟨x, y, hxc, hyc, fun h => hyx h.symm⟩ · push Not at htwo have hneighbor_subset : G.neighborFinset x.1 ⊆ ({u, v} : Finset V) := by intro z hz rw [Finset.mem_insert, Finset.mem_singleton] by_contra hz_not rw [not_or] at hz_not have hz_adj : G.Adj x.1 z := by rw [G.mem_neighborFinset] at hz exact hz let zH : {x // x ≠ u ∧ x ≠ v} := ⟨z, hz_not.1, hz_not.2⟩ have hzH_mem : zH ∈ c.supp := by exact c.mem_supp_of_adj_mem_supp hxc (show H.Adj x zH from hz_adj) have hzH_eq : zH = x := htwo zH hzH_mem have hz_eq : z = x.1 := congrArg Subtype.val hzH_eq exact (G.ne_of_adj hz_adj) hz_eq.symm have hdeg_le_two : G.degree x.1 ≤ 2 := by rw [← G.card_neighborFinset_eq_degree x.1] exact (Finset.card_le_card hneighbor_subset).trans Finset.card_le_two have hthree : 3 ≤ G.degree x.1 := hmindeg x.1 omega lemma exists_ne_mem_deleted_pair_component_of_three_le_degree_ne {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) {u v : V} (c : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent) (x : {x // x ≠ u ∧ x ≠ v}) : ∃ y : {x // x ≠ u ∧ x ≠ v}, y ∈ c.supp ∧ y ≠ x := by obtain ⟨a, b, ha, hb, hab⟩ := exists_ne_mem_deleted_pair_component_of_three_le_degree (G := G) hmindeg c by_cases hax : a = x · refine ⟨b, hb, ?_⟩ intro hbx exact hab (hax.trans hbx.symm) · exact ⟨a, ha, hax⟩ lemma exists_adj_mem_deleted_pair_component_of_three_le_degree {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) {u v : V} (c : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent) : ∃ x y : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ y ∈ c.supp ∧ G.Adj x.1 y.1 := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨x, y, hxc, hyc, hxy⟩ := exists_ne_mem_deleted_pair_component_of_three_le_degree (G := G) hmindeg c have hxyc : (⟨x, hxc⟩ : c) ≠ ⟨y, hyc⟩ := by intro h exact hxy (congrArg Subtype.val h) haveI : Nontrivial c := ⟨⟨⟨x, hxc⟩, ⟨y, hyc⟩, hxyc⟩⟩ obtain ⟨z, hxz⟩ := (SimpleGraph.ConnectedComponent.connected_toSimpleGraph c).preconnected |>.exists_adj_of_nontrivial (⟨x, hxc⟩ : c) refine ⟨x, z.1, hxc, z.2, ?_⟩ exact (show H.Adj x z.1 from hxz) lemma exists_adj_deleted_pair_vertex_of_component_avoiding {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (c : (G.induce {z | z ≠ u ∧ z ≠ v}).ConnectedComponent) (x : {z // z ≠ u ∧ z ≠ v}) : ∃ y : {z // z ≠ u ∧ z ≠ v}, y ∈ c.supp ∧ y ≠ x ∧ (G.Adj y.1 u ∨ G.Adj y.1 v) := by classical let H : SimpleGraph {z // z ≠ u ∧ z ≠ v} := G.induce {z | z ≠ u ∧ z ≠ v} let K : SimpleGraph {z // z ≠ x.1} := G.induce {z | z ≠ x.1} obtain ⟨y0, hy0c, hy0_ne_x⟩ := exists_ne_mem_deleted_pair_component_of_three_le_degree_ne (G := G) hmindeg c x let y0K : {z // z ≠ x.1} := ⟨y0.1, fun h => hy0_ne_x (Subtype.ext h)⟩ let uK : {z // z ≠ x.1} := ⟨u, fun h => x.2.1 h.symm⟩ let vK : {z // z ≠ x.1} := ⟨v, fun h => x.2.2 h.symm⟩ let S : Set {z // z ≠ x.1} := {z | ∃ hzu : z.1 ≠ u, ∃ hzv : z.1 ≠ v, (⟨z.1, hzu, hzv⟩ : {z // z ≠ u ∧ z ≠ v}) ∈ c.supp ∧ (⟨z.1, hzu, hzv⟩ : {z // z ≠ u ∧ z ≠ v}) ≠ x} have hy0S : y0K ∈ S := by refine ⟨y0.2.1, y0.2.2, ?_, ?_⟩ · simpa [y0K] · simpa [y0K] have huS : uK ∉ S := by rintro ⟨hzu, _hzv, _hmem, _hne⟩ exact hzu rfl obtain ⟨p⟩ := (hall_connected x.1) y0K uK obtain ⟨d, _hdmem, hfstS, hsnd_notS⟩ := p.exists_boundary_dart S hy0S huS obtain ⟨hfst_ne_u, hfst_ne_v, hfst_c, hfst_ne_x⟩ := hfstS have hsnd_eq_or : d.snd = uK ∨ d.snd = vK := by by_contra hnot rw [not_or] at hnot have hsnd_ne_u : d.snd.1 ≠ u := by intro h exact hnot.1 (Subtype.ext h) have hsnd_ne_v : d.snd.1 ≠ v := by intro h exact hnot.2 (Subtype.ext h) have hsnd_ne_x : (⟨d.snd.1, hsnd_ne_u, hsnd_ne_v⟩ : {z // z ≠ u ∧ z ≠ v}) ≠ x := by intro h exact d.snd.2 (congrArg Subtype.val h) have hsnd_c : (⟨d.snd.1, hsnd_ne_u, hsnd_ne_v⟩ : {z // z ≠ u ∧ z ≠ v}) ∈ c.supp := by exact c.mem_supp_of_adj_mem_supp hfst_c (show H.Adj ⟨d.fst.1, hfst_ne_u, hfst_ne_v⟩ ⟨d.snd.1, hsnd_ne_u, hsnd_ne_v⟩ from d.adj) exact hsnd_notS ⟨hsnd_ne_u, hsnd_ne_v, hsnd_c, hsnd_ne_x⟩ let y : {z // z ≠ u ∧ z ≠ v} := ⟨d.fst.1, hfst_ne_u, hfst_ne_v⟩ refine ⟨y, hfst_c, hfst_ne_x, ?_⟩ rcases hsnd_eq_or with hsnd_eq | hsnd_eq · exact Or.inl (by simpa [K, uK, hsnd_eq] using d.adj) · exact Or.inr (by simpa [K, vK, hsnd_eq] using d.adj) omit [Fintype V] [DecidableEq V] in lemma reachable_delete_pair_cut_vertices_of_component_touch_both {G : SimpleGraph V} {x y a b : V} (hxa : x ≠ a) (hxb : x ≠ b) (hya : y ≠ a) (hyb : y ≠ b) (c : (G.induce {z | z ≠ a ∧ z ≠ b}).ConnectedComponent) (hx_not : (⟨x, hxa, hxb⟩ : {z // z ≠ a ∧ z ≠ b}) ∉ c.supp) (hy_not : (⟨y, hya, hyb⟩ : {z // z ≠ a ∧ z ≠ b}) ∉ c.supp) {p q : {z // z ≠ a ∧ z ≠ b}} (hpc : p ∈ c.supp) (hqc : q ∈ c.supp) (hpa : G.Adj p.1 a) (hqb : G.Adj q.1 b) : (G.induce {z | z ≠ x ∧ z ≠ y}).Reachable ⟨a, hxa.symm, hya.symm⟩ ⟨b, hxb.symm, hyb.symm⟩ := by classical let K : SimpleGraph {z // z ≠ x ∧ z ≠ y} := G.induce {z | z ≠ x ∧ z ≠ y} let aK : {z // z ≠ x ∧ z ≠ y} := ⟨a, hxa.symm, hya.symm⟩ let bK : {z // z ≠ x ∧ z ≠ y} := ⟨b, hxb.symm, hyb.symm⟩ have hp_ne_x : p.1 ≠ x := by intro hpx have hp_eq : p = (⟨x, hxa, hxb⟩ : {z // z ≠ a ∧ z ≠ b}) := Subtype.ext hpx exact hx_not (hp_eq ▸ hpc) have hp_ne_y : p.1 ≠ y := by intro hpy have hp_eq : p = (⟨y, hya, hyb⟩ : {z // z ≠ a ∧ z ≠ b}) := Subtype.ext hpy exact hy_not (hp_eq ▸ hpc) have hq_ne_x : q.1 ≠ x := by intro hqx have hq_eq : q = (⟨x, hxa, hxb⟩ : {z // z ≠ a ∧ z ≠ b}) := Subtype.ext hqx exact hx_not (hq_eq ▸ hqc) have hq_ne_y : q.1 ≠ y := by intro hqy have hq_eq : q = (⟨y, hya, hyb⟩ : {z // z ≠ a ∧ z ≠ b}) := Subtype.ext hqy exact hy_not (hq_eq ▸ hqc) let pK : {z // z ≠ x ∧ z ≠ y} := ⟨p.1, hp_ne_x, hp_ne_y⟩ let qK : {z // z ≠ x ∧ z ≠ y} := ⟨q.1, hq_ne_x, hq_ne_y⟩ let pC : c := ⟨p, hpc⟩ let qC : c := ⟨q, hqc⟩ let φ : c.toSimpleGraph →g K := { toFun := fun r => (⟨r.1.1, by intro hrx have hr_eq : r.1 = (⟨x, hxa, hxb⟩ : {z // z ≠ a ∧ z ≠ b}) := Subtype.ext hrx exact hx_not (hr_eq ▸ r.2), by intro hry have hr_eq : r.1 = (⟨y, hya, hyb⟩ : {z // z ≠ a ∧ z ≠ b}) := Subtype.ext hry exact hy_not (hr_eq ▸ r.2)⟩ : {z // z ≠ x ∧ z ≠ y}) map_rel' := by intro r s hrs exact (show G.Adj r.1.1 s.1.1 from hrs) } have hpqC : c.toSimpleGraph.Reachable pC qC := (SimpleGraph.ConnectedComponent.connected_toSimpleGraph c).preconnected pC qC have hpqK : K.Reachable pK qK := by simpa [φ, pC, qC, pK, qK] using hpqC.map φ have hapK : K.Adj aK pK := by exact hpa.symm have hqbK : K.Adj qK bK := by exact hqb simpa [K, aK, bK] using hapK.reachable.trans (hpqK.trans hqbK.reachable) omit [Fintype V] in lemma reachable_delete_pair_cut_vertices_of_third_component {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (huv : u ≠ v) {c d e : (G.induce {z | z ≠ u ∧ z ≠ v}).ConnectedComponent} (hec : e ≠ c) (hed : e ≠ d) {x y : {z // z ≠ u ∧ z ≠ v}} (hxc : x ∈ c.supp) (hyd : y ∈ d.supp) : (G.induce {z | z ≠ x.1 ∧ z ≠ y.1}).Reachable ⟨u, x.2.1.symm, y.2.1.symm⟩ ⟨v, x.2.2.symm, y.2.2.symm⟩ := by classical have hx_not : x ∉ e.supp := by intro hxe exact hec (SimpleGraph.ConnectedComponent.eq_of_common_vertex hxe hxc) have hy_not : y ∉ e.supp := by intro hye exact hed (SimpleGraph.ConnectedComponent.eq_of_common_vertex hye hyd) obtain ⟨⟨p, hpe, hpu⟩, ⟨q, hqe, hqv⟩⟩ := exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv e exact reachable_delete_pair_cut_vertices_of_component_touch_both (G := G) (x := x.1) (y := y.1) (a := u) (b := v) x.2.1 x.2.2 y.2.1 y.2.2 e (by simpa using hx_not) (by simpa using hy_not) hpe hqe hpu hqv omit [Fintype V] [DecidableEq V] in lemma reachable_pair_deleted_of_mem_four_deleted_component {G : SimpleGraph V} {x y a b : V} (hax : a ≠ x) (hay : a ≠ y) (hbx : b ≠ x) (hby : b ≠ y) (c : ((G.induce {z | z ≠ x ∧ z ≠ y}).induce {z | z ≠ (⟨a, hax, hay⟩ : {z // z ≠ x ∧ z ≠ y}) ∧ z ≠ (⟨b, hbx, hby⟩ : {z // z ≠ x ∧ z ≠ y})}).ConnectedComponent) {p q : {z : {z // z ≠ x ∧ z ≠ y} | z ≠ (⟨a, hax, hay⟩ : {z // z ≠ x ∧ z ≠ y}) ∧ z ≠ (⟨b, hbx, hby⟩ : {z // z ≠ x ∧ z ≠ y})}} (hpc : p ∈ c.supp) (hqc : q ∈ c.supp) : (G.induce {z | z ≠ a ∧ z ≠ b}).Reachable ⟨p.1.1, by intro hpa exact p.2.1 (Subtype.ext hpa), by intro hpb exact p.2.2 (Subtype.ext hpb)⟩ ⟨q.1.1, by intro hqa exact q.2.1 (Subtype.ext hqa), by intro hqb exact q.2.2 (Subtype.ext hqb)⟩ := by classical let K : SimpleGraph {z // z ≠ x ∧ z ≠ y} := G.induce {z | z ≠ x ∧ z ≠ y} let L : SimpleGraph {z : {z // z ≠ x ∧ z ≠ y} | z ≠ (⟨a, hax, hay⟩ : {z // z ≠ x ∧ z ≠ y}) ∧ z ≠ (⟨b, hbx, hby⟩ : {z // z ≠ x ∧ z ≠ y})} := K.induce {z | z ≠ (⟨a, hax, hay⟩ : {z // z ≠ x ∧ z ≠ y}) ∧ z ≠ (⟨b, hbx, hby⟩ : {z // z ≠ x ∧ z ≠ y})} let H : SimpleGraph {z // z ≠ a ∧ z ≠ b} := G.induce {z | z ≠ a ∧ z ≠ b} let pC : c := ⟨p, hpc⟩ let qC : c := ⟨q, hqc⟩ let φ : c.toSimpleGraph →g H := { toFun := fun r => (⟨r.1.1.1, by intro hra exact r.1.2.1 (Subtype.ext hra), by intro hrb exact r.1.2.2 (Subtype.ext hrb)⟩ : {z // z ≠ a ∧ z ≠ b}) map_rel' := by intro r s hrs exact (show G.Adj r.1.1.1 s.1.1.1 from hrs) } have hpqC : c.toSimpleGraph.Reachable pC qC := (SimpleGraph.ConnectedComponent.connected_toSimpleGraph c).preconnected pC qC simpa [H, φ, pC, qC] using hpqC.map φ omit [Fintype V] in lemma exists_adj_cut_vertex_of_four_deleted_component {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {z | z ≠ w}).Connected) {a b : V} {x y : {z // z ≠ a ∧ z ≠ b}} (hxy_comp : (G.induce {z | z ≠ a ∧ z ≠ b}).connectedComponentMk x ≠ (G.induce {z | z ≠ a ∧ z ≠ b}).connectedComponentMk y) (c : ((G.induce {z | z ≠ x.1 ∧ z ≠ y.1}).induce {z | z ≠ (⟨a, x.2.1.symm, y.2.1.symm⟩ : {z // z ≠ x.1 ∧ z ≠ y.1}) ∧ z ≠ (⟨b, x.2.2.symm, y.2.2.symm⟩ : {z // z ≠ x.1 ∧ z ≠ y.1})}).ConnectedComponent) : ∃ z : {z : {z // z ≠ x.1 ∧ z ≠ y.1} | z ≠ (⟨a, x.2.1.symm, y.2.1.symm⟩ : {z // z ≠ x.1 ∧ z ≠ y.1}) ∧ z ≠ (⟨b, x.2.2.symm, y.2.2.symm⟩ : {z // z ≠ x.1 ∧ z ≠ y.1})}, z ∈ c.supp ∧ (G.Adj z.1.1 a ∨ G.Adj z.1.1 b) := by classical let H : SimpleGraph {z // z ≠ a ∧ z ≠ b} := G.induce {z | z ≠ a ∧ z ≠ b} let K : SimpleGraph {z // z ≠ x.1 ∧ z ≠ y.1} := G.induce {z | z ≠ x.1 ∧ z ≠ y.1} let aK : {z // z ≠ x.1 ∧ z ≠ y.1} := ⟨a, x.2.1.symm, y.2.1.symm⟩ let bK : {z // z ≠ x.1 ∧ z ≠ y.1} := ⟨b, x.2.2.symm, y.2.2.symm⟩ let L : SimpleGraph {z : {z // z ≠ x.1 ∧ z ≠ y.1} | z ≠ aK ∧ z ≠ bK} := K.induce {z | z ≠ aK ∧ z ≠ bK} obtain ⟨t, htc⟩ := c.nonempty_supp let tH : {z // z ≠ a ∧ z ≠ b} := ⟨t.1.1, by intro hta exact t.2.1 (Subtype.ext hta), by intro htb exact t.2.2 (Subtype.ext htb)⟩ have hxy_ne : x.1 ≠ y.1 := by intro hxy exact hxy_comp (by rw [Subtype.ext hxy]) by_cases ht_y : H.connectedComponentMk tH = H.connectedComponentMk y · let Y : SimpleGraph {z // z ≠ y.1} := G.induce {z | z ≠ y.1} let tY : {z // z ≠ y.1} := ⟨t.1.1, t.1.2.2⟩ let aY : {z // z ≠ y.1} := ⟨a, y.2.1.symm⟩ let bY : {z // z ≠ y.1} := ⟨b, y.2.2.symm⟩ let xY : {z // z ≠ y.1} := ⟨x.1, hxy_ne⟩ let mkLY (z : {z // z ≠ y.1}) (hzx : z.1 ≠ x.1) (hza : z.1 ≠ a) (hzb : z.1 ≠ b) : {z : {z // z ≠ x.1 ∧ z ≠ y.1} | z ≠ aK ∧ z ≠ bK} := ⟨⟨z.1, hzx, z.2⟩, by intro h exact hza (congrArg Subtype.val h), by intro h exact hzb (congrArg Subtype.val h)⟩ let S : Set {z // z ≠ y.1} := {z | ∃ hzx : z.1 ≠ x.1, ∃ hza : z.1 ≠ a, ∃ hzb : z.1 ≠ b, mkLY z hzx hza hzb ∈ c.supp} have htS : tY ∈ S := by refine ⟨t.1.2.1, ?_, ?_, ?_⟩ · intro hta exact t.2.1 (Subtype.ext hta) · intro htb exact t.2.2 (Subtype.ext htb) · simpa [tY, mkLY] using htc have haS : aY ∉ S := by rintro ⟨_, hza, _hzb, _hmem⟩ exact hza rfl obtain ⟨p⟩ := (hall_connected y.1) tY aY obtain ⟨d, _hdmem, hfstS, hsnd_notS⟩ := p.exists_boundary_dart S htS haS rcases hfstS with ⟨hfst_ne_x, hfst_ne_a, hfst_ne_b, hfst_mem⟩ let fstL : {z : {z // z ≠ x.1 ∧ z ≠ y.1} | z ≠ aK ∧ z ≠ bK} := mkLY d.fst hfst_ne_x hfst_ne_a hfst_ne_b have hfst_mem' : fstL ∈ c.supp := by simpa [fstL] using hfst_mem have hsnd_eq_or : d.snd = aY ∨ d.snd = bY ∨ d.snd = xY := by by_contra hnot rw [not_or] at hnot rw [not_or] at hnot have hsnd_ne_a : d.snd.1 ≠ a := by intro h exact hnot.1 (Subtype.ext h) have hsnd_ne_b : d.snd.1 ≠ b := by intro h exact hnot.2.1 (Subtype.ext h) have hsnd_ne_x : d.snd.1 ≠ x.1 := by intro h exact hnot.2.2 (Subtype.ext h) have hsnd_mem : mkLY d.snd hsnd_ne_x hsnd_ne_a hsnd_ne_b ∈ c.supp := by exact c.mem_supp_of_adj_mem_supp hfst_mem' (show L.Adj fstL (mkLY d.snd hsnd_ne_x hsnd_ne_a hsnd_ne_b) from d.adj) exact hsnd_notS ⟨hsnd_ne_x, hsnd_ne_a, hsnd_ne_b, hsnd_mem⟩ rcases hsnd_eq_or with hsnd_eq | hsnd_eq_or · refine ⟨fstL, hfst_mem', Or.inl ?_⟩ simpa [Y, aY, hsnd_eq, fstL, mkLY] using d.adj rcases hsnd_eq_or with hsnd_eq | hsnd_eq · refine ⟨fstL, hfst_mem', Or.inr ?_⟩ simpa [Y, bY, hsnd_eq, fstL, mkLY] using d.adj · let fstH : {z // z ≠ a ∧ z ≠ b} := ⟨fstL.1.1, by intro h exact fstL.2.1 (Subtype.ext h), by intro h exact fstL.2.2 (Subtype.ext h)⟩ have htfst : H.Reachable tH fstH := by simpa [H, tH, fstH, fstL] using reachable_pair_deleted_of_mem_four_deleted_component (G := G) x.2.1.symm y.2.1.symm x.2.2.symm y.2.2.symm c htc hfst_mem' have ht_fst_comp : H.connectedComponentMk tH = H.connectedComponentMk fstH := SimpleGraph.ConnectedComponent.sound htfst have hfst_adj_x : H.Adj fstH x := by simpa [H, Y, xY, hsnd_eq, fstH, fstL, mkLY] using d.adj have hfst_comp_x : H.connectedComponentMk fstH = H.connectedComponentMk x := SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hfst_adj_x exact False.elim (hxy_comp (hfst_comp_x.symm.trans (ht_fst_comp.symm.trans ht_y))) · let X : SimpleGraph {z // z ≠ x.1} := G.induce {z | z ≠ x.1} let tX : {z // z ≠ x.1} := ⟨t.1.1, t.1.2.1⟩ let aX : {z // z ≠ x.1} := ⟨a, x.2.1.symm⟩ let bX : {z // z ≠ x.1} := ⟨b, x.2.2.symm⟩ let yX : {z // z ≠ x.1} := ⟨y.1, hxy_ne.symm⟩ let mkLX (z : {z // z ≠ x.1}) (hzy : z.1 ≠ y.1) (hza : z.1 ≠ a) (hzb : z.1 ≠ b) : {z : {z // z ≠ x.1 ∧ z ≠ y.1} | z ≠ aK ∧ z ≠ bK} := ⟨⟨z.1, z.2, hzy⟩, by intro h exact hza (congrArg Subtype.val h), by intro h exact hzb (congrArg Subtype.val h)⟩ let S : Set {z // z ≠ x.1} := {z | ∃ hzy : z.1 ≠ y.1, ∃ hza : z.1 ≠ a, ∃ hzb : z.1 ≠ b, mkLX z hzy hza hzb ∈ c.supp} have htS : tX ∈ S := by refine ⟨t.1.2.2, ?_, ?_, ?_⟩ · intro hta exact t.2.1 (Subtype.ext hta) · intro htb exact t.2.2 (Subtype.ext htb) · simpa [tX, mkLX] using htc have haS : aX ∉ S := by rintro ⟨_hzy, hza, _hzb, _hmem⟩ exact hza rfl obtain ⟨p⟩ := (hall_connected x.1) tX aX obtain ⟨d, _hdmem, hfstS, hsnd_notS⟩ := p.exists_boundary_dart S htS haS rcases hfstS with ⟨hfst_ne_y, hfst_ne_a, hfst_ne_b, hfst_mem⟩ let fstL : {z : {z // z ≠ x.1 ∧ z ≠ y.1} | z ≠ aK ∧ z ≠ bK} := mkLX d.fst hfst_ne_y hfst_ne_a hfst_ne_b have hfst_mem' : fstL ∈ c.supp := by simpa [fstL] using hfst_mem have hsnd_eq_or : d.snd = aX ∨ d.snd = bX ∨ d.snd = yX := by by_contra hnot rw [not_or] at hnot rw [not_or] at hnot have hsnd_ne_a : d.snd.1 ≠ a := by intro h exact hnot.1 (Subtype.ext h) have hsnd_ne_b : d.snd.1 ≠ b := by intro h exact hnot.2.1 (Subtype.ext h) have hsnd_ne_y : d.snd.1 ≠ y.1 := by intro h exact hnot.2.2 (Subtype.ext h) have hsnd_mem : mkLX d.snd hsnd_ne_y hsnd_ne_a hsnd_ne_b ∈ c.supp := by exact c.mem_supp_of_adj_mem_supp hfst_mem' (show L.Adj fstL (mkLX d.snd hsnd_ne_y hsnd_ne_a hsnd_ne_b) from d.adj) exact hsnd_notS ⟨hsnd_ne_y, hsnd_ne_a, hsnd_ne_b, hsnd_mem⟩ rcases hsnd_eq_or with hsnd_eq | hsnd_eq_or · refine ⟨fstL, hfst_mem', Or.inl ?_⟩ simpa [X, aX, hsnd_eq, fstL, mkLX] using d.adj rcases hsnd_eq_or with hsnd_eq | hsnd_eq · refine ⟨fstL, hfst_mem', Or.inr ?_⟩ simpa [X, bX, hsnd_eq, fstL, mkLX] using d.adj · let fstH : {z // z ≠ a ∧ z ≠ b} := ⟨fstL.1.1, by intro h exact fstL.2.1 (Subtype.ext h), by intro h exact fstL.2.2 (Subtype.ext h)⟩ have htfst : H.Reachable tH fstH := by simpa [H, tH, fstH, fstL] using reachable_pair_deleted_of_mem_four_deleted_component (G := G) x.2.1.symm y.2.1.symm x.2.2.symm y.2.2.symm c htc hfst_mem' have ht_fst_comp : H.connectedComponentMk tH = H.connectedComponentMk fstH := SimpleGraph.ConnectedComponent.sound htfst have hfst_adj_y : H.Adj fstH y := by simpa [H, X, yX, hsnd_eq, fstH, fstL, mkLX] using d.adj have hfst_comp_y : H.connectedComponentMk fstH = H.connectedComponentMk y := SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hfst_adj_y exact False.elim (ht_y (ht_fst_comp.trans hfst_comp_y)) omit [Fintype V] [DecidableEq V] in lemma connected_of_reachable_pair_and_components_touch {G : SimpleGraph V} {a b : V} (hab_reach : G.Reachable a b) (htouch : ∀ c : (G.induce {x | x ≠ a ∧ x ≠ b}).ConnectedComponent, ∃ x : {x // x ≠ a ∧ x ≠ b}, x ∈ c.supp ∧ (G.Adj x.1 a ∨ G.Adj x.1 b)) : G.Connected := by classical let H : SimpleGraph {x // x ≠ a ∧ x ≠ b} := G.induce {x | x ≠ a ∧ x ≠ b} have reaches_a : ∀ w : V, G.Reachable w a := by intro w by_cases hwa : w = a · subst w exact SimpleGraph.Reachable.rfl by_cases hwb : w = b · subst w exact hab_reach.symm let wH : {x // x ≠ a ∧ x ≠ b} := ⟨w, hwa, hwb⟩ let c : H.ConnectedComponent := H.connectedComponentMk wH obtain ⟨z, hzc, hza | hzb⟩ := htouch c · have hwzH : H.Reachable wH z := by have hcz : H.connectedComponentMk z = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hzc exact SimpleGraph.ConnectedComponent.exact (G := H) hcz.symm have hwzG : G.Reachable w z.1 := by simpa [H, wH] using (hwzH.map (SimpleGraph.Embedding.induce {x | x ≠ a ∧ x ≠ b}).toHom) exact hwzG.trans hza.reachable · have hwzH : H.Reachable wH z := by have hcz : H.connectedComponentMk z = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hzc exact SimpleGraph.ConnectedComponent.exact (G := H) hcz.symm have hwzG : G.Reachable w z.1 := by simpa [H, wH] using (hwzH.map (SimpleGraph.Embedding.induce {x | x ≠ a ∧ x ≠ b}).toHom) exact (hwzG.trans hzb.reachable).trans hab_reach.symm exact { preconnected := by intro u v exact (reaches_a u).trans (reaches_a v).symm nonempty := ⟨a⟩ } omit [Fintype V] [DecidableEq V] in lemma connected_delete_pair_of_reachable_pair_and_components_touch {G : SimpleGraph V} {x y a b : V} (hax : a ≠ x) (hay : a ≠ y) (hbx : b ≠ x) (hby : b ≠ y) (hab_reach : (G.induce {z | z ≠ x ∧ z ≠ y}).Reachable ⟨a, hax, hay⟩ ⟨b, hbx, hby⟩) (htouch : ∀ c : ((G.induce {z | z ≠ x ∧ z ≠ y}).induce {z | z ≠ (⟨a, hax, hay⟩ : {z // z ≠ x ∧ z ≠ y}) ∧ z ≠ (⟨b, hbx, hby⟩ : {z // z ≠ x ∧ z ≠ y})}).ConnectedComponent, ∃ z : {z : {z // z ≠ x ∧ z ≠ y} | z ≠ (⟨a, hax, hay⟩ : {z // z ≠ x ∧ z ≠ y}) ∧ z ≠ (⟨b, hbx, hby⟩ : {z // z ≠ x ∧ z ≠ y})}, z ∈ c.supp ∧ (G.Adj z.1.1 a ∨ G.Adj z.1.1 b)) : (G.induce {z | z ≠ x ∧ z ≠ y}).Connected := by classical let K : SimpleGraph {z // z ≠ x ∧ z ≠ y} := G.induce {z | z ≠ x ∧ z ≠ y} let aK : {z // z ≠ x ∧ z ≠ y} := ⟨a, hax, hay⟩ let bK : {z // z ≠ x ∧ z ≠ y} := ⟨b, hbx, hby⟩ refine connected_of_reachable_pair_and_components_touch (G := K) (a := aK) (b := bK) hab_reach ?_ intro c obtain ⟨z, hzc, hza | hzb⟩ := htouch c · refine ⟨z, hzc, Or.inl ?_⟩ exact (show K.Adj z.1 aK from hza) · refine ⟨z, hzc, Or.inr ?_⟩ exact (show K.Adj z.1 bK from hzb) omit [Fintype V] in lemma connected_delete_pair_of_third_component {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {z | z ≠ w}).Connected) {u v : V} (huv : u ≠ v) {c d e : (G.induce {z | z ≠ u ∧ z ≠ v}).ConnectedComponent} (hcd : c ≠ d) (hec : e ≠ c) (hed : e ≠ d) {x y : {z // z ≠ u ∧ z ≠ v}} (hxc : x ∈ c.supp) (hyd : y ∈ d.supp) : (G.induce {z | z ≠ x.1 ∧ z ≠ y.1}).Connected := by classical let H : SimpleGraph {z // z ≠ u ∧ z ≠ v} := G.induce {z | z ≠ u ∧ z ≠ v} have hxy_comp : H.connectedComponentMk x ≠ H.connectedComponentMk y := by have hcx : H.connectedComponentMk x = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hxc have hdy : H.connectedComponentMk y = d := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hyd intro hcomp exact hcd (by rw [← hcx, ← hdy, hcomp]) have huv_reach : (G.induce {z | z ≠ x.1 ∧ z ≠ y.1}).Reachable ⟨u, x.2.1.symm, y.2.1.symm⟩ ⟨v, x.2.2.symm, y.2.2.symm⟩ := reachable_delete_pair_cut_vertices_of_third_component (G := G) hall_connected huv hec hed hxc hyd exact connected_delete_pair_of_reachable_pair_and_components_touch (G := G) (x := x.1) (y := y.1) (a := u) (b := v) x.2.1.symm y.2.1.symm x.2.2.symm y.2.2.symm huv_reach (by intro r simpa [H] using exists_adj_cut_vertex_of_four_deleted_component (G := G) hall_connected (a := u) (b := v) (x := x) (y := y) hxy_comp r) omit [Fintype V] in lemma exists_nonseparating_pair_of_three_pair_deleted_components {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {z | z ≠ w}).Connected) {u v : V} (huv : u ≠ v) {c d e : (G.induce {z | z ≠ u ∧ z ≠ v}).ConnectedComponent} (hcd : c ≠ d) (hec : e ≠ c) (hed : e ≠ d) : ∃ (x y w : V) (_hwx : G.Adj w x) (_hwy : G.Adj w y), x ≠ y ∧ ¬ G.Adj x y ∧ (G.induce {z | z ≠ x ∧ z ≠ y}).Connected := by classical let H : SimpleGraph {z // z ≠ u ∧ z ≠ v} := G.induce {z | z ≠ u ∧ z ≠ v} obtain ⟨⟨x, hxc, hxu⟩, _⟩ := exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv c obtain ⟨⟨y, hyd, hyu⟩, _⟩ := exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv d have hcx : H.connectedComponentMk x = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hxc have hdy : H.connectedComponentMk y = d := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hyd have hcomp_ne : H.connectedComponentMk x ≠ H.connectedComponentMk y := by intro hcomp exact hcd (by rw [← hcx, ← hdy, hcomp]) have hxy : x.1 ≠ y.1 := by intro hxy exact hcomp_ne (by rw [Subtype.ext hxy]) have hnadj : ¬ G.Adj x.1 y.1 := by intro hxy_adj have hH_adj : H.Adj x y := hxy_adj exact hcomp_ne (SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hH_adj) exact ⟨x.1, y.1, u, hxu.symm, hyu.symm, hxy, hnadj, connected_delete_pair_of_third_component (G := G) hall_connected huv hcd hec hed hxc hyd⟩ omit [Fintype V] in lemma exists_nonseparating_pair_of_adj_pair_deleted_components {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {z | z ≠ w}).Connected) {u v : V} (huv : u ≠ v) (huv_adj : G.Adj u v) {c d : (G.induce {z | z ≠ u ∧ z ≠ v}).ConnectedComponent} (hcd : c ≠ d) : ∃ (x y w : V) (_hwx : G.Adj w x) (_hwy : G.Adj w y), x ≠ y ∧ ¬ G.Adj x y ∧ (G.induce {z | z ≠ x ∧ z ≠ y}).Connected := by classical let H : SimpleGraph {z // z ≠ u ∧ z ≠ v} := G.induce {z | z ≠ u ∧ z ≠ v} obtain ⟨⟨x, hxc, hxu⟩, _⟩ := exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv c obtain ⟨⟨y, hyd, hyu⟩, _⟩ := exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv d have hcx : H.connectedComponentMk x = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hxc have hdy : H.connectedComponentMk y = d := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hyd have hcomp_ne : H.connectedComponentMk x ≠ H.connectedComponentMk y := by intro hcomp exact hcd (by rw [← hcx, ← hdy, hcomp]) have hxy : x.1 ≠ y.1 := by intro hxy exact hcomp_ne (by rw [Subtype.ext hxy]) have hnadj : ¬ G.Adj x.1 y.1 := by intro hxy_adj have hH_adj : H.Adj x y := hxy_adj exact hcomp_ne (SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hH_adj) have huv_reach : (G.induce {z | z ≠ x.1 ∧ z ≠ y.1}).Reachable ⟨u, x.2.1.symm, y.2.1.symm⟩ ⟨v, x.2.2.symm, y.2.2.symm⟩ := by have huvK : (G.induce {z | z ≠ x.1 ∧ z ≠ y.1}).Adj ⟨u, x.2.1.symm, y.2.1.symm⟩ ⟨v, x.2.2.symm, y.2.2.symm⟩ := huv_adj exact huvK.reachable have hconn_pair : (G.induce {z | z ≠ x.1 ∧ z ≠ y.1}).Connected := connected_delete_pair_of_reachable_pair_and_components_touch (G := G) (x := x.1) (y := y.1) (a := u) (b := v) x.2.1.symm y.2.1.symm x.2.2.symm y.2.2.symm huv_reach (by intro r simpa [H] using exists_adj_cut_vertex_of_four_deleted_component (G := G) hall_connected (a := u) (b := v) (x := x) (y := y) hcomp_ne r) exact ⟨x.1, y.1, u, hxu.symm, hyu.symm, hxy, hnadj, hconn_pair⟩ theorem nonseparatingPairDeletionTwoCut_of_twoComponent : NonseparatingPairDeletionTwoComponentStatement → NonseparatingPairDeletionTwoCutStatement := by intro htwo V _ _ G _ hconn hne_top hmindeg hall_connected hcut obtain ⟨a, b, hab, hnot_conn⟩ := hcut let H : SimpleGraph {x // x ≠ a ∧ x ≠ b} := G.induce {x | x ≠ a ∧ x ≠ b} by_cases hthree : ∃ c d e : H.ConnectedComponent, c ≠ d ∧ e ≠ c ∧ e ≠ d · obtain ⟨c, d, e, hcd, hec, hed⟩ := hthree simpa [H] using exists_nonseparating_pair_of_three_pair_deleted_components (G := G) hall_connected hab hcd hec hed · exact htwo V G hconn hne_top hmindeg hall_connected a b hab hnot_conn (by intro c d e hcd hec hed exact hthree ⟨c, d, e, hcd, hec, hed⟩) omit [Fintype V] in lemma exists_pair_deleted_components_touch_both_of_not_connected {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v w : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (huv : u ≠ v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ c d : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent, c ≠ d ∧ ((∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 u) ∧ ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 v) ∧ ((∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ d.supp ∧ G.Adj x.1 u) ∧ ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ d.supp ∧ G.Adj x.1 v) := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} have hw_ne_u : w ≠ u := G.ne_of_adj hwu have hw_ne_v : w ≠ v := G.ne_of_adj hwv have hnonempty : Nonempty {x // x ≠ u ∧ x ≠ v} := ⟨⟨w, hw_ne_u, hw_ne_v⟩⟩ have hnot_pre : ¬ H.Preconnected := by intro hpre apply hnot_conn rw [SimpleGraph.connected_iff] exact ⟨hpre, hnonempty⟩ rw [SimpleGraph.Preconnected] at hnot_pre push Not at hnot_pre obtain ⟨a, b, hab_not⟩ := hnot_pre let ca : H.ConnectedComponent := H.connectedComponentMk a let cb : H.ConnectedComponent := H.connectedComponentMk b have hca_ne_cb : ca ≠ cb := by intro h exact hab_not (SimpleGraph.ConnectedComponent.exact (G := H) h) refine ⟨ca, cb, hca_ne_cb, ?_, ?_⟩ · exact exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv ca · exact exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv cb omit [Fintype V] in lemma exists_nonadjacent_neighbors_left_of_pair_delete_not_connected {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v w : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (huv : u ≠ v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ x y : {x // x ≠ u ∧ x ≠ v}, G.Adj u x.1 ∧ G.Adj u y.1 ∧ x.1 ≠ y.1 ∧ ¬ G.Adj x.1 y.1 ∧ (G.induce {z | z ≠ u ∧ z ≠ v}).connectedComponentMk x ≠ (G.induce {z | z ≠ u ∧ z ≠ v}).connectedComponentMk y := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨c, d, hcd, hc, hd⟩ := exists_pair_deleted_components_touch_both_of_not_connected (G := G) hall_connected hwu hwv huv hnot_conn obtain ⟨x, hxc, hxu⟩ := hc.1 obtain ⟨y, hyd, hyu⟩ := hd.1 have hcx : H.connectedComponentMk x = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hxc have hdy : H.connectedComponentMk y = d := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hyd have hcomp_ne : H.connectedComponentMk x ≠ H.connectedComponentMk y := by intro hcomp exact hcd (by rw [← hcx, ← hdy, hcomp]) have hxy : x.1 ≠ y.1 := by intro hxy exact hcomp_ne (by rw [Subtype.ext hxy]) have hnot_adj : ¬ G.Adj x.1 y.1 := by intro hxy_adj have hH_adj : H.Adj x y := hxy_adj exact hcomp_ne (SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hH_adj) refine ⟨x, y, hxu.symm, hyu.symm, hxy, hnot_adj, ?_⟩ simpa [H] using hcomp_ne omit [Fintype V] in lemma exists_nonadjacent_neighbors_right_of_pair_delete_not_connected {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v w : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (huv : u ≠ v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ x y : {x // x ≠ u ∧ x ≠ v}, G.Adj v x.1 ∧ G.Adj v y.1 ∧ x.1 ≠ y.1 ∧ ¬ G.Adj x.1 y.1 ∧ (G.induce {z | z ≠ u ∧ z ≠ v}).connectedComponentMk x ≠ (G.induce {z | z ≠ u ∧ z ≠ v}).connectedComponentMk y := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨c, d, hcd, hc, hd⟩ := exists_pair_deleted_components_touch_both_of_not_connected (G := G) hall_connected hwu hwv huv hnot_conn obtain ⟨x, hxc, hxv⟩ := hc.2 obtain ⟨y, hyd, hyv⟩ := hd.2 have hcx : H.connectedComponentMk x = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hxc have hdy : H.connectedComponentMk y = d := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hyd have hcomp_ne : H.connectedComponentMk x ≠ H.connectedComponentMk y := by intro hcomp exact hcd (by rw [← hcx, ← hdy, hcomp]) have hxy : x.1 ≠ y.1 := by intro hxy exact hcomp_ne (by rw [Subtype.ext hxy]) have hnot_adj : ¬ G.Adj x.1 y.1 := by intro hxy_adj have hH_adj : H.Adj x y := hxy_adj exact hcomp_ne (SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hH_adj) refine ⟨x, y, hxv.symm, hyv.symm, hxy, hnot_adj, ?_⟩ simpa [H] using hcomp_ne omit [Fintype V] in lemma exists_separated_neighbors_of_delete_not_preconnected {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) {w : V} (hnot_pre : ¬ (G.induce {x | x ≠ w}).Preconnected) : ∃ (u v : V) (hwu : G.Adj w u) (hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ (G.induce {x | x ≠ w}).connectedComponentMk ⟨u, (G.ne_of_adj hwu).symm⟩ ≠ (G.induce {x | x ≠ w}).connectedComponentMk ⟨v, (G.ne_of_adj hwv).symm⟩ := by classical let H : SimpleGraph {x // x ≠ w} := G.induce {x | x ≠ w} have hnot_pre' : ¬ H.Preconnected := hnot_pre rw [SimpleGraph.Preconnected] at hnot_pre' push Not at hnot_pre' obtain ⟨a, b, hab_not⟩ := hnot_pre' let ca : H.ConnectedComponent := H.connectedComponentMk a let cb : H.ConnectedComponent := H.connectedComponentMk b have hca_ne_cb : ca ≠ cb := by intro h exact hab_not (SimpleGraph.ConnectedComponent.exact (G := H) h) obtain ⟨uH, hu_mem, huw⟩ := exists_adj_deleted_vertex_of_component (G := G) hconn w ca obtain ⟨vH, hv_mem, hvw⟩ := exists_adj_deleted_vertex_of_component (G := G) hconn w cb have hcu : H.connectedComponentMk uH = ca := by simpa [SimpleGraph.ConnectedComponent.mem_supp_iff] using hu_mem have hcv : H.connectedComponentMk vH = cb := by simpa [SimpleGraph.ConnectedComponent.mem_supp_iff] using hv_mem have huvH : uH ≠ vH := by intro huv exact hca_ne_cb (by rw [← hcu, ← hcv, huv]) have huv : uH.1 ≠ vH.1 := fun huv => huvH (Subtype.ext huv) have hnadj : ¬ G.Adj uH.1 vH.1 := by intro huv_adj have hHadj : H.Adj uH vH := huv_adj have hcomp_eq : H.connectedComponentMk uH = H.connectedComponentMk vH := SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hHadj exact hca_ne_cb (by rw [← hcu, ← hcv, hcomp_eq]) refine ⟨uH.1, vH.1, huw.symm, hvw.symm, huv, hnadj, ?_⟩ simpa [H] using (show H.connectedComponentMk uH ≠ H.connectedComponentMk vH from by intro hcomp exact hca_ne_cb (by rw [← hcu, ← hcv, hcomp])) omit [Fintype V] in lemma exists_separated_neighbors_of_delete_not_connected {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) {w x : V} (hwx : G.Adj w x) (hnot_conn : ¬ (G.induce {y | y ≠ w}).Connected) : ∃ (u v : V) (hwu : G.Adj w u) (hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ (G.induce {x | x ≠ w}).connectedComponentMk ⟨u, (G.ne_of_adj hwu).symm⟩ ≠ (G.induce {x | x ≠ w}).connectedComponentMk ⟨v, (G.ne_of_adj hwv).symm⟩ := by let H : SimpleGraph {y // y ≠ w} := G.induce {y | y ≠ w} have hnonempty : Nonempty {y // y ≠ w} := ⟨⟨x, (G.ne_of_adj hwx).symm⟩⟩ have hnot_pre : ¬ H.Preconnected := by intro hpre apply hnot_conn rw [SimpleGraph.connected_iff] exact ⟨hpre, hnonempty⟩ exact exists_separated_neighbors_of_delete_not_preconnected (G := G) hconn hnot_pre lemma colorable_complete_deleted_component {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) (v : V) (c : (G.induce {w | w ≠ v}).ConnectedComponent) (hcomplete : c.toSimpleGraph = ⊤) : c.toSimpleGraph.Colorable G.maxDegree := by classical obtain ⟨x, hxc, hxv⟩ := exists_adj_deleted_vertex_of_component (G := G) hconn v c let xc : c := ⟨x, hxc⟩ let adjOfNe (y : c) (hy : y.1 ≠ x) : G.Adj x.1 y.1.1 := by have hy_ne_xc : y ≠ xc := by intro h exact hy (congrArg Subtype.val h) have hadjC : c.toSimpleGraph.Adj xc y := by rw [hcomplete] exact (SimpleGraph.top_adj _ _).mpr hy_ne_xc.symm exact hadjC let f : c → G.neighborSet x.1 := fun y => if hy : y.1 = x then ⟨v, hxv⟩ else ⟨y.1.1, adjOfNe y hy⟩ have hf_inj : Function.Injective f := by intro y z hyz by_cases hy : y.1 = x · by_cases hz : z.1 = x · apply Subtype.ext exact hy.trans hz.symm · have fy : f y = (⟨v, hxv⟩ : G.neighborSet x.1) := by dsimp [f] split_ifs with h · rfl · exact False.elim (h hy) have fz : f z = (⟨z.1.1, adjOfNe z hz⟩ : G.neighborSet x.1) := by dsimp [f] split_ifs with h · exact False.elim (hz h) · rfl rw [fy, fz] at hyz have hv_eq : v = z.1.1 := congrArg (fun q : G.neighborSet x.1 => q.1) hyz exact False.elim (z.1.2 hv_eq.symm) · by_cases hz : z.1 = x · have fy : f y = (⟨y.1.1, adjOfNe y hy⟩ : G.neighborSet x.1) := by dsimp [f] split_ifs with h · exact False.elim (hy h) · rfl have fz : f z = (⟨v, hxv⟩ : G.neighborSet x.1) := by dsimp [f] split_ifs with h · rfl · exact False.elim (h hz) rw [fy, fz] at hyz have hy_eq : y.1.1 = v := congrArg (fun q : G.neighborSet x.1 => q.1) hyz exact False.elim (y.1.2 hy_eq) · have fy : f y = (⟨y.1.1, adjOfNe y hy⟩ : G.neighborSet x.1) := by dsimp [f] split_ifs with h · exact False.elim (hy h) · rfl have fz : f z = (⟨z.1.1, adjOfNe z hz⟩ : G.neighborSet x.1) := by dsimp [f] split_ifs with h · exact False.elim (hz h) · rfl rw [fy, fz] at hyz have hyz_val : y.1.1 = z.1.1 := congrArg (fun q : G.neighborSet x.1 => q.1) hyz apply Subtype.ext exact Subtype.ext hyz_val have hcard : Fintype.card c ≤ G.degree x.1 := by have hcard' : Fintype.card c ≤ Fintype.card (G.neighborSet x.1) := Fintype.card_le_of_injective f hf_inj rw [← G.card_neighborFinset_eq_degree x.1] rwa [← Set.toFinset_card (G.neighborSet x.1)] at hcard' exact colorable_of_fintype_card_le (G := c.toSimpleGraph) (hcard.trans (G.degree_le_maxDegree x.1)) lemma colorable_deleted_component_of_complete_or_odd {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) {v : V} (c : (G.induce {w | w ≠ v}).ConnectedComponent) (hthree : 3 ≤ G.maxDegree) (hexception : c.toSimpleGraph = ⊤ ∨ IsOddCycleGraph c.toSimpleGraph) : c.toSimpleGraph.Colorable G.maxDegree := by rcases hexception with hcomplete | hodd · exact colorable_complete_deleted_component (G := G) hconn v c hcomplete · exact colorable_of_isOddCycleGraph_of_three_le hodd hthree lemma degree_deleted_component_le_deleted_degree {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} (c : (G.induce {w | w ≠ v}).ConnectedComponent) [Fintype c] [DecidableRel c.toSimpleGraph.Adj] (x : c) : c.toSimpleGraph.degree x ≤ (G.induce {w | w ≠ v}).degree x.1 := by classical let H : SimpleGraph {w // w ≠ v} := G.induce {w | w ≠ v} let K : SimpleGraph c := c.toSimpleGraph let f : K.neighborSet x → H.neighborSet x.1 := fun y => ⟨y.1.1, y.2⟩ have hf_inj : Function.Injective f := by intro y z hyz have hval : y.1.1 = z.1.1 := congrArg (fun q : H.neighborSet x.1 => q.1) hyz exact Subtype.ext (Subtype.ext hval) have hcard : Fintype.card (K.neighborSet x) ≤ Fintype.card (H.neighborSet x.1) := Fintype.card_le_of_injective f hf_inj rw [← K.card_neighborFinset_eq_degree x] change (K.neighborFinset x).card ≤ H.degree x.1 rw [← H.card_neighborFinset_eq_degree x.1] rwa [← Set.toFinset_card (K.neighborSet x), ← Set.toFinset_card (H.neighborSet x.1)] at hcard lemma degree_deleted_component_le_maxDegree {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} (c : (G.induce {w | w ≠ v}).ConnectedComponent) [Fintype c] [DecidableRel c.toSimpleGraph.Adj] (x : c) : c.toSimpleGraph.degree x ≤ G.maxDegree := by classical let H : SimpleGraph {w // w ≠ v} := G.induce {w | w ≠ v} have hcomponent : c.toSimpleGraph.degree x ≤ H.degree x.1 := degree_deleted_component_le_deleted_degree (G := G) c x have hdeleted : H.degree x.1 ≤ G.degree x.1.1 := degree_induce_le (G := G) (s := {w | w ≠ v}) x.1 exact hcomponent.trans (hdeleted.trans (G.degree_le_maxDegree x.1.1)) lemma degree_deleted_component_lt_maxDegree_of_adj_deleted {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} (c : (G.induce {w | w ≠ v}).ConnectedComponent) [Fintype c] [DecidableRel c.toSimpleGraph.Adj] {x : {w // w ≠ v}} (hxc : x ∈ c.supp) (hxv : G.Adj x.1 v) : c.toSimpleGraph.degree ⟨x, hxc⟩ < G.maxDegree := by classical let H : SimpleGraph {w // w ≠ v} := G.induce {w | w ≠ v} have hcomponent : c.toSimpleGraph.degree ⟨x, hxc⟩ ≤ H.degree x := degree_deleted_component_le_deleted_degree (G := G) c ⟨x, hxc⟩ have hdeleted : H.degree x < G.degree x.1 := degree_induce_lt_of_adj_notMem (G := G) (s := {w | w ≠ v}) x.2 (by simp) hxv exact hcomponent.trans_lt (hdeleted.trans_le (G.degree_le_maxDegree x.1)) lemma exists_low_degree_in_deleted_component_induce {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) (v : V) (c : (G.induce {w | w ≠ v}).ConnectedComponent) [Fintype c] [DecidableRel c.toSimpleGraph.Adj] : ∀ s : Finset c, s.Nonempty → ∃ x : {y // y ∈ s}, (c.toSimpleGraph.induce ((s : Finset c) : Set c)).degree x < G.maxDegree := by classical haveI : DecidablePred (fun x : {w // w ≠ v} => x ∈ c) := fun _ => Classical.propDecidable _ haveI : Fintype c := Subtype.fintype (fun x : {w // w ≠ v} => x ∈ c) intro s hs_nonempty let K : SimpleGraph c := c.toSimpleGraph by_cases hs_univ : s = Finset.univ · obtain ⟨x, hxc, hxv⟩ := exists_adj_deleted_vertex_of_component (G := G) hconn v c let xc : c := ⟨x, hxc⟩ have hmem : xc ∈ s := by rw [hs_univ]; exact Finset.mem_univ xc refine ⟨⟨xc, hmem⟩, ?_⟩ have hle : (K.induce ((s : Finset c) : Set c)).degree ⟨xc, hmem⟩ ≤ K.degree xc := degree_induce_finset_le (G := K) (s := s) ⟨xc, hmem⟩ exact hle.trans_lt (degree_deleted_component_lt_maxDegree_of_adj_deleted (G := G) c hxc hxv) · obtain ⟨a, ha⟩ := hs_nonempty obtain ⟨b, hb⟩ : ∃ b : c, b ∉ s := by by_contra hnone push Not at hnone apply hs_univ ext z exact ⟨fun _ => Finset.mem_univ z, fun _ => hnone z⟩ obtain ⟨p⟩ := (SimpleGraph.ConnectedComponent.connected_toSimpleGraph c) a b obtain ⟨d, _hdmem, hfst, hsnd⟩ := p.exists_boundary_dart ((s : Finset c) : Set c) (by simpa using ha) (by simpa using hb) refine ⟨⟨d.fst, hfst⟩, ?_⟩ have hlt : (K.induce ((s : Finset c) : Set c)).degree ⟨d.fst, hfst⟩ < K.degree d.fst := degree_induce_finset_lt_of_adj_notMem (G := K) (s := s) hfst hsnd d.adj exact hlt.trans_le (degree_deleted_component_le_maxDegree (G := G) c d.fst) lemma two_le_degree_of_adj_of_adj_ne {G : SimpleGraph V} [DecidableRel G.Adj] {x u w : V} (hxu : G.Adj x u) (hxw : G.Adj x w) (huw : u ≠ w) : 2 ≤ G.degree x := by rw [← G.card_neighborFinset_eq_degree x] have hsub : ({u, w} : Finset V) ⊆ G.neighborFinset x := by intro y hy rw [Finset.mem_insert, Finset.mem_singleton] at hy rw [G.mem_neighborFinset] rcases hy with rfl | rfl · exact hxu · exact hxw have hcard : ({u, w} : Finset V).card = 2 := by simp [huw] exact hcard ▸ Finset.card_le_card hsub lemma exists_neighbor_ne_pair_of_three_le_degree {G : SimpleGraph V} [DecidableRel G.Adj] {w u v : V} (hthree : 3 ≤ G.degree w) : ∃ z : V, G.Adj w z ∧ z ≠ u ∧ z ≠ v := by classical by_contra hnone push Not at hnone have hsubset : G.neighborFinset w ⊆ {u, v} := by intro z hz rw [G.mem_neighborFinset] at hz have hzu_or_zv : z = u ∨ z = v := by by_cases hzu : z = u · exact Or.inl hzu · exact Or.inr (hnone z hz hzu) simpa [Finset.mem_insert, Finset.mem_singleton] using hzu_or_zv have hdeg_le_two : G.degree w ≤ 2 := by rw [← G.card_neighborFinset_eq_degree w] calc (G.neighborFinset w).card ≤ ({u, v} : Finset V).card := Finset.card_le_card hsubset _ ≤ 2 := Finset.card_le_two omega lemma exists_pair_deleted_components_touch_both_of_pair_delete_not_connected {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (huv : u ≠ v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ c d : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent, c ≠ d ∧ ((∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 u) ∧ ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 v) ∧ ((∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ d.supp ∧ G.Adj x.1 u) ∧ ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ d.supp ∧ G.Adj x.1 v) := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨z, _huz, hzu, hzv⟩ := exists_neighbor_ne_pair_of_three_le_degree (G := G) (w := u) (u := u) (v := v) (hmindeg u) have hnonempty : Nonempty {x // x ≠ u ∧ x ≠ v} := ⟨⟨z, hzu, hzv⟩⟩ have hnot_pre : ¬ H.Preconnected := by intro hpre apply hnot_conn rw [SimpleGraph.connected_iff] exact ⟨hpre, hnonempty⟩ rw [SimpleGraph.Preconnected] at hnot_pre push Not at hnot_pre obtain ⟨a, b, hab_not⟩ := hnot_pre let ca : H.ConnectedComponent := H.connectedComponentMk a let cb : H.ConnectedComponent := H.connectedComponentMk b have hca_ne_cb : ca ≠ cb := by intro h exact hab_not (SimpleGraph.ConnectedComponent.exact (G := H) h) refine ⟨ca, cb, hca_ne_cb, ?_, ?_⟩ · exact exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv ca · exact exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv cb omit [Fintype V] [DecidableEq V] in lemma connectedComponent_eq_left_or_right_of_no_three {H : SimpleGraph V} {c d e : H.ConnectedComponent} (htwo : ∀ c d e : H.ConnectedComponent, c ≠ d → e ≠ c → e ≠ d → False) (hcd : c ≠ d) : e = c ∨ e = d := by by_cases hec : e = c · exact Or.inl hec · by_cases hed : e = d · exact Or.inr hed · exact False.elim (htwo c d e hcd hec hed) omit [Fintype V] in lemma reachable_delete_vertex_of_dist_le {H : SimpleGraph V} [DecidableRel H.Adj] {a b c : V} (ha : a ≠ c) (hb : b ≠ c) (hr : H.Reachable a b) (hle : H.dist a b ≤ H.dist a c) : (H.induce {x | x ≠ c}).Reachable ⟨a, ha⟩ ⟨b, hb⟩ := by classical obtain ⟨p, hpdist⟩ := hr.exists_walk_length_eq_dist have hc_not : c ∉ p.support := by intro hc have hlen_c : (p.takeUntil c hc).length = H.dist a c := SimpleGraph.length_eq_dist_of_subwalk hpdist (p.isSubwalk_takeUntil hc) have hlt : (p.takeUntil c hc).length < p.length := p.length_takeUntil_lt hc hb.symm have hdist_lt : H.dist a c < H.dist a b := by rw [← hlen_c, ← hpdist] exact hlt exact (not_lt_of_ge hle) hdist_lt have hpall : ∀ x ∈ p.support, x ∈ {x | x ≠ c} := by intro x hx hxc exact hc_not (hxc ▸ hx) exact ⟨by simpa using p.induce {x | x ≠ c} hpall⟩ omit [Fintype V] in lemma exists_reachable_delete_farther_of_two {H : SimpleGraph V} [DecidableRel H.Adj] {s x y : V} (hxy : x ≠ y) (hsx : H.Reachable s x) (hsy : H.Reachable s y) : ∃ (near far : V) (hsfar : s ≠ far) (hnfar : near ≠ far), ((near = x ∧ far = y) ∨ (near = y ∧ far = x)) ∧ (H.induce {z | z ≠ far}).Reachable ⟨s, hsfar⟩ ⟨near, hnfar⟩ := by classical by_cases hle : H.dist s x ≤ H.dist s y · have hsy_ne : s ≠ y := by intro hsy_eq have hdistx0 : H.dist s x = 0 := by have : H.dist s x ≤ 0 := by simpa [hsy_eq] using hle exact Nat.eq_zero_of_le_zero this have hsx_eq : s = x := (hsx.dist_eq_zero_iff).mp hdistx0 exact hxy (hsx_eq.symm.trans hsy_eq) exact ⟨x, y, hsy_ne, hxy, Or.inl ⟨rfl, rfl⟩, reachable_delete_vertex_of_dist_le (H := H) hsy_ne hxy hsx hle⟩ · have hyx_le : H.dist s y ≤ H.dist s x := le_of_lt (Nat.lt_of_not_ge hle) have hsx_ne : s ≠ x := by intro hsx_eq have hdisty0 : H.dist s y = 0 := by have : H.dist s y ≤ 0 := by simpa [hsx_eq] using hyx_le exact Nat.eq_zero_of_le_zero this have hsy_eq : s = y := (hsy.dist_eq_zero_iff).mp hdisty0 exact hxy (hsx_eq.symm.trans hsy_eq) exact ⟨y, x, hsx_ne, hxy.symm, Or.inr ⟨rfl, rfl⟩, reachable_delete_vertex_of_dist_le (H := H) hsx_ne hxy.symm hsy hyx_le⟩ lemma exists_two_left_neighbors_in_pair_deleted_component_of_nonadjacent_two_component {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (huv : u ≠ v) (hnadj : ¬ G.Adj u v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) (htwo : ∀ c d e : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent, c ≠ d → e ≠ c → e ≠ d → False) : ∃ c : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent, ∃ x y : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ y ∈ c.supp ∧ G.Adj x.1 u ∧ G.Adj y.1 u ∧ x.1 ≠ y.1 := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨c, d, hcd, hc, hd⟩ := exists_pair_deleted_components_touch_both_of_pair_delete_not_connected (G := G) hmindeg hall_connected huv hnot_conn obtain ⟨xc, hxc, hxcu⟩ := hc.1 obtain ⟨xd, hxd, hxdu⟩ := hd.1 by_contra hnone push Not at hnone have hsubset : G.neighborFinset u ⊆ {xc.1, xd.1} := by intro z hz rw [G.mem_neighborFinset] at hz have hzu : z ≠ u := G.ne_of_adj hz.symm have hzv : z ≠ v := by intro hzv apply hnadj simpa [hzv] using hz let zH : {x // x ≠ u ∧ x ≠ v} := ⟨z, hzu, hzv⟩ have hcomp : H.connectedComponentMk zH = c ∨ H.connectedComponentMk zH = d := by simpa [H] using connectedComponent_eq_left_or_right_of_no_three (H := H) (c := c) (d := d) (e := H.connectedComponentMk zH) (by simpa [H] using htwo) hcd rcases hcomp with hcomp | hcomp · have hzmem_c : zH ∈ c.supp := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hcomp have hz_eq : z = xc.1 := hnone c zH xc hzmem_c hxc hz.symm hxcu simp [Finset.mem_insert, Finset.mem_singleton, hz_eq] · have hzmem_d : zH ∈ d.supp := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hcomp have hz_eq : z = xd.1 := hnone d zH xd hzmem_d hxd hz.symm hxdu simp [Finset.mem_insert, Finset.mem_singleton, hz_eq] have hdeg_le_two : G.degree u ≤ 2 := by rw [← G.card_neighborFinset_eq_degree u] calc (G.neighborFinset u).card ≤ ({xc.1, xd.1} : Finset V).card := Finset.card_le_card hsubset _ ≤ 2 := Finset.card_le_two have hdeg_ge_three : 3 ≤ G.degree u := hmindeg u omega lemma exists_left_side_path_avoiding_left_neighbor_of_nonadjacent_two_component {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (huv : u ≠ v) (hnadj : ¬ G.Adj u v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) (htwo : ∀ c d e : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent, c ≠ d → e ≠ c → e ≠ d → False) : ∃ (c : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent) (near far q : {x // x ≠ u ∧ x ≠ v}) (hqfar : q ≠ far) (hnfar : near ≠ far), near ∈ c.supp ∧ far ∈ c.supp ∧ q ∈ c.supp ∧ G.Adj near.1 u ∧ G.Adj far.1 u ∧ G.Adj q.1 v ∧ ((G.induce {x | x ≠ u ∧ x ≠ v}).induce {z | z ≠ far}).Reachable ⟨q, hqfar⟩ ⟨near, hnfar⟩ := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨c, x, y, hxc, hyc, hxu, hyu, hxy⟩ := exists_two_left_neighbors_in_pair_deleted_component_of_nonadjacent_two_component (G := G) hmindeg hall_connected huv hnadj hnot_conn htwo obtain ⟨_, ⟨q, hqc, hqv⟩⟩ := exists_adj_both_deleted_pair_vertex_of_component (G := G) hall_connected huv c have hxy_sub : x ≠ y := by intro h exact hxy (congrArg Subtype.val h) have hqx : H.Reachable q x := by have hq_comp : H.connectedComponentMk q = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hqc have hx_comp : H.connectedComponentMk x = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hxc exact SimpleGraph.ConnectedComponent.exact (G := H) (by rw [hq_comp, hx_comp]) have hqy : H.Reachable q y := by have hq_comp : H.connectedComponentMk q = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hqc have hy_comp : H.connectedComponentMk y = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hyc exact SimpleGraph.ConnectedComponent.exact (G := H) (by rw [hq_comp, hy_comp]) obtain ⟨near, far, hqfar, hnfar, hnearfar, hreach⟩ := exists_reachable_delete_farther_of_two (H := H) hxy_sub hqx hqy rcases hnearfar with hxycase | hyxcase · rcases hxycase with ⟨hnear, hfar⟩ subst near subst far exact ⟨c, x, y, q, hqfar, hnfar, hxc, hyc, hqc, hxu, hyu, hqv, by simpa [H] using hreach⟩ · rcases hyxcase with ⟨hnear, hfar⟩ subst near subst far exact ⟨c, y, x, q, hqfar, hnfar, hyc, hxc, hqc, hyu, hxu, hqv, by simpa [H] using hreach⟩ omit [Fintype V] [DecidableEq V] in lemma walk_support_subset_component {H : SimpleGraph V} {c : H.ConnectedComponent} {a b : V} (ha : a ∈ c.supp) (p : H.Walk a b) : ∀ z ∈ p.support, z ∈ c.supp := by induction p with | nil => intro z hz simp at hz subst z exact ha | @cons u v w h p ih => intro z hz simp only [SimpleGraph.Walk.support_cons, List.mem_cons] at hz rcases hz with rfl | hz · exact ha · exact ih (c.mem_supp_of_adj_mem_supp ha h) z hz omit [Fintype V] [DecidableEq V] in lemma reachable_retained_cut_vertices_of_left_side_path {G : SimpleGraph V} [DecidableRel G.Adj] {u v : V} {c d : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent} (hcd : c ≠ d) {near far q other : {x // x ≠ u ∧ x ≠ v}} (hnear_c : near ∈ c.supp) (hq_c : q ∈ c.supp) (hother_d : other ∈ d.supp) (hnearu : G.Adj near.1 u) (hqv : G.Adj q.1 v) (hqfar : q ≠ far) (hnfar : near ≠ far) (hreach : ((G.induce {x | x ≠ u ∧ x ≠ v}).induce {z | z ≠ far}).Reachable ⟨q, hqfar⟩ ⟨near, hnfar⟩) : (G.induce {z | z ≠ far.1 ∧ z ≠ other.1}).Reachable ⟨u, far.2.1.symm, other.2.1.symm⟩ ⟨v, far.2.2.symm, other.2.2.symm⟩ := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} let K : SimpleGraph {z // z ≠ far.1 ∧ z ≠ other.1} := G.induce {z | z ≠ far.1 ∧ z ≠ other.1} have hq_ne_other : q ≠ other := by intro h exact hcd (SimpleGraph.ConnectedComponent.eq_of_common_vertex (by simpa [h] using hq_c) hother_d) have hnear_ne_other : near ≠ other := by intro h exact hcd (SimpleGraph.ConnectedComponent.eq_of_common_vertex (by simpa [h] using hnear_c) hother_d) obtain ⟨p⟩ := hreach let pH : H.Walk q near := p.map (SimpleGraph.Embedding.induce {z : {x // x ≠ u ∧ x ≠ v} | z ≠ far}).toHom have hpH_mem_c : ∀ z ∈ pH.support, z ∈ c.supp := walk_support_subset_component hq_c pH have hpH_all : ∀ z ∈ pH.support, z ∈ {z : {x // x ≠ u ∧ x ≠ v} | z ≠ far ∧ z ≠ other} := by intro z hz constructor · intro hzf change z ∈ (p.map (SimpleGraph.Embedding.induce {z : {x // x ≠ u ∧ x ≠ v} | z ≠ far}).toHom).support at hz rw [SimpleGraph.Walk.support_map] at hz rcases List.mem_map.mp hz with ⟨r, _hr, hrz⟩ have hrval : r.1 = z := by simpa using hrz exact r.2 (by simp [hrval, hzf]) · intro hzo exact hcd (SimpleGraph.ConnectedComponent.eq_of_common_vertex (by simpa [hzo] using hpH_mem_c z hz) hother_d) let pHL : (H.induce {z : {x // x ≠ u ∧ x ≠ v} | z ≠ far ∧ z ≠ other}).Walk ⟨q, hqfar, hq_ne_other⟩ ⟨near, hnfar, hnear_ne_other⟩ := pH.induce {z : {x // x ≠ u ∧ x ≠ v} | z ≠ far ∧ z ≠ other} hpH_all let φ : (H.induce {z : {x // x ≠ u ∧ x ≠ v} | z ≠ far ∧ z ≠ other}) →g K := { toFun := fun r => (⟨r.1.1, by intro h exact r.2.1 (Subtype.ext h), by intro h exact r.2.2 (Subtype.ext h)⟩ : {z // z ≠ far.1 ∧ z ≠ other.1}) map_rel' := by intro r s hrs exact (show G.Adj r.1.1 s.1.1 from hrs) } let qK : {z // z ≠ far.1 ∧ z ≠ other.1} := ⟨q.1, by intro h exact hqfar (Subtype.ext h), by intro h exact hq_ne_other (Subtype.ext h)⟩ let nearK : {z // z ≠ far.1 ∧ z ≠ other.1} := ⟨near.1, by intro h exact hnfar (Subtype.ext h), by intro h exact hnear_ne_other (Subtype.ext h)⟩ let uK : {z // z ≠ far.1 ∧ z ≠ other.1} := ⟨u, far.2.1.symm, other.2.1.symm⟩ let vK : {z // z ≠ far.1 ∧ z ≠ other.1} := ⟨v, far.2.2.symm, other.2.2.symm⟩ have hq_near_K : K.Reachable qK nearK := by exact ⟨by simpa [pHL, pH, φ, qK, nearK, K, H] using pHL.map φ⟩ have hu_near_K : K.Adj uK nearK := by exact hnearu.symm have hq_v_K : K.Adj qK vK := by exact hqv simpa [K, uK, vK] using hu_near_K.reachable.trans (hq_near_K.symm.trans hq_v_K.reachable) omit [Fintype V] in lemma connected_delete_pair_of_left_side_path_and_other_component {G : SimpleGraph V} [DecidableRel G.Adj] (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} {c d : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent} (hcd : c ≠ d) {near far q other : {x // x ≠ u ∧ x ≠ v}} (hnear_c : near ∈ c.supp) (hfar_c : far ∈ c.supp) (hq_c : q ∈ c.supp) (hother_d : other ∈ d.supp) (hnearu : G.Adj near.1 u) (hqv : G.Adj q.1 v) (hqfar : q ≠ far) (hnfar : near ≠ far) (hreach : ((G.induce {x | x ≠ u ∧ x ≠ v}).induce {z | z ≠ far}).Reachable ⟨q, hqfar⟩ ⟨near, hnfar⟩) : (G.induce {z | z ≠ far.1 ∧ z ≠ other.1}).Connected := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} have hfar_comp : H.connectedComponentMk far = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hfar_c have hother_comp : H.connectedComponentMk other = d := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hother_d have hcomp_ne : H.connectedComponentMk far ≠ H.connectedComponentMk other := by intro h exact hcd (by rw [← hfar_comp, ← hother_comp, h]) have huv_reach : (G.induce {z | z ≠ far.1 ∧ z ≠ other.1}).Reachable ⟨u, far.2.1.symm, other.2.1.symm⟩ ⟨v, far.2.2.symm, other.2.2.symm⟩ := reachable_retained_cut_vertices_of_left_side_path (G := G) (u := u) (v := v) (c := c) (d := d) hcd hnear_c hq_c hother_d hnearu hqv hqfar hnfar hreach exact connected_delete_pair_of_reachable_pair_and_components_touch (G := G) (x := far.1) (y := other.1) (a := u) (b := v) far.2.1.symm other.2.1.symm far.2.2.symm other.2.2.symm huv_reach (by intro r simpa [H] using exists_adj_cut_vertex_of_four_deleted_component (G := G) hall_connected (a := u) (b := v) (x := far) (y := other) hcomp_ne r) theorem nonseparatingPairDeletionTwoComponentNonadjacent : NonseparatingPairDeletionTwoComponentNonadjacentStatement := by intro V _ _ G _ _hconn _hne_top hmindeg hall_connected a b hab hnadj hnot_conn htwo classical let H : SimpleGraph {x // x ≠ a ∧ x ≠ b} := G.induce {x | x ≠ a ∧ x ≠ b} obtain ⟨c, near, far, q, hqfar, hnfar, hnear_c, hfar_c, hq_c, hnearu, hfaru, hqv, hreach⟩ := exists_left_side_path_avoiding_left_neighbor_of_nonadjacent_two_component (G := G) hmindeg hall_connected hab hnadj hnot_conn htwo obtain ⟨c0, d0, hc0d0, hc0, hd0⟩ := exists_pair_deleted_components_touch_both_of_pair_delete_not_connected (G := G) hmindeg hall_connected hab hnot_conn have hc_eq : c = c0 ∨ c = d0 := by simpa [H] using connectedComponent_eq_left_or_right_of_no_three (H := H) (c := c0) (d := d0) (e := c) (by simpa [H] using htwo) hc0d0 rcases hc_eq with hc_eq | hc_eq · obtain ⟨other, hother_d, hotheru⟩ := hd0.1 have hnear_c0 : near ∈ c0.supp := by simpa [hc_eq] using hnear_c have hfar_c0 : far ∈ c0.supp := by simpa [hc_eq] using hfar_c have hq_c0 : q ∈ c0.supp := by simpa [hc_eq] using hq_c have hfar_other_sub : far ≠ other := by intro h exact hc0d0 (SimpleGraph.ConnectedComponent.eq_of_common_vertex (by simpa [h] using hfar_c0) hother_d) have hfar_other : far.1 ≠ other.1 := by intro h exact hfar_other_sub (Subtype.ext h) have hfar_comp : H.connectedComponentMk far = c0 := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hfar_c0 have hother_comp : H.connectedComponentMk other = d0 := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hother_d have hcomp_ne : H.connectedComponentMk far ≠ H.connectedComponentMk other := by intro h exact hc0d0 (by rw [← hfar_comp, ← hother_comp, h]) have hnot_adj : ¬ G.Adj far.1 other.1 := by intro hadj have hHadj : H.Adj far other := hadj exact hcomp_ne (SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hHadj) have hconn_pair : (G.induce {z | z ≠ far.1 ∧ z ≠ other.1}).Connected := connected_delete_pair_of_left_side_path_and_other_component (G := G) hall_connected (u := a) (v := b) (c := c0) (d := d0) hc0d0 hnear_c0 hfar_c0 hq_c0 hother_d hnearu hqv hqfar hnfar hreach exact ⟨far.1, other.1, a, hfaru.symm, hotheru.symm, hfar_other, hnot_adj, hconn_pair⟩ · obtain ⟨other, hother_c, hotheru⟩ := hc0.1 have hd0c0 : d0 ≠ c0 := hc0d0.symm have hnear_d0 : near ∈ d0.supp := by simpa [hc_eq] using hnear_c have hfar_d0 : far ∈ d0.supp := by simpa [hc_eq] using hfar_c have hq_d0 : q ∈ d0.supp := by simpa [hc_eq] using hq_c have hfar_other_sub : far ≠ other := by intro h exact hd0c0 (SimpleGraph.ConnectedComponent.eq_of_common_vertex (by simpa [h] using hfar_d0) hother_c) have hfar_other : far.1 ≠ other.1 := by intro h exact hfar_other_sub (Subtype.ext h) have hfar_comp : H.connectedComponentMk far = d0 := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hfar_d0 have hother_comp : H.connectedComponentMk other = c0 := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hother_c have hcomp_ne : H.connectedComponentMk far ≠ H.connectedComponentMk other := by intro h exact hd0c0 (by rw [← hfar_comp, ← hother_comp, h]) have hnot_adj : ¬ G.Adj far.1 other.1 := by intro hadj have hHadj : H.Adj far other := hadj exact hcomp_ne (SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hHadj) have hconn_pair : (G.induce {z | z ≠ far.1 ∧ z ≠ other.1}).Connected := connected_delete_pair_of_left_side_path_and_other_component (G := G) hall_connected (u := a) (v := b) (c := d0) (d := c0) hd0c0 hnear_d0 hfar_d0 hq_d0 hother_c hnearu hqv hqfar hnfar hreach exact ⟨far.1, other.1, a, hfaru.symm, hotheru.symm, hfar_other, hnot_adj, hconn_pair⟩ lemma exists_nonseparating_pair_of_adj_pair_cut_not_connected {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (huv : u ≠ v) (huv_adj : G.Adj u v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ (x y w : V) (_hwx : G.Adj w x) (_hwy : G.Adj w y), x ≠ y ∧ ¬ G.Adj x y ∧ (G.induce {z | z ≠ x ∧ z ≠ y}).Connected := by obtain ⟨c, d, hcd, _hc, _hd⟩ := exists_pair_deleted_components_touch_both_of_pair_delete_not_connected (G := G) hmindeg hall_connected huv hnot_conn exact exists_nonseparating_pair_of_adj_pair_deleted_components (G := G) hall_connected huv huv_adj hcd theorem nonseparatingPairDeletionTwoComponent_of_nonadjacent : NonseparatingPairDeletionTwoComponentNonadjacentStatement → NonseparatingPairDeletionTwoComponentStatement := by intro hnonadj V _ _ G _ hconn hne_top hmindeg hall_connected a b hab hnot_conn htwo by_cases hab_adj : G.Adj a b · exact exists_nonseparating_pair_of_adj_pair_cut_not_connected (G := G) hmindeg hall_connected hab hab_adj hnot_conn · exact hnonadj V G hconn hne_top hmindeg hall_connected a b hab hab_adj hnot_conn htwo theorem nonseparatingPairDeletionTwoComponent : NonseparatingPairDeletionTwoComponentStatement := nonseparatingPairDeletionTwoComponent_of_nonadjacent nonseparatingPairDeletionTwoComponentNonadjacent lemma exists_pair_deleted_components_touch_both_with_edges_of_pair_delete_not_connected {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (huv : u ≠ v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ c d : (G.induce {x | x ≠ u ∧ x ≠ v}).ConnectedComponent, c ≠ d ∧ ((∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 u) ∧ ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ G.Adj x.1 v) ∧ ((∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ d.supp ∧ G.Adj x.1 u) ∧ ∃ x : {x // x ≠ u ∧ x ≠ v}, x ∈ d.supp ∧ G.Adj x.1 v) ∧ (∃ x y : {x // x ≠ u ∧ x ≠ v}, x ∈ c.supp ∧ y ∈ c.supp ∧ G.Adj x.1 y.1) ∧ (∃ x y : {x // x ≠ u ∧ x ≠ v}, x ∈ d.supp ∧ y ∈ d.supp ∧ G.Adj x.1 y.1) := by obtain ⟨c, d, hcd, hc, hd⟩ := exists_pair_deleted_components_touch_both_of_pair_delete_not_connected (G := G) hmindeg hall_connected huv hnot_conn exact ⟨c, d, hcd, hc, hd, exists_adj_mem_deleted_pair_component_of_three_le_degree (G := G) hmindeg c, exists_adj_mem_deleted_pair_component_of_three_le_degree (G := G) hmindeg d⟩ lemma exists_nonadjacent_neighbors_left_of_pair_cut_not_connected {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (huv : u ≠ v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ x y : {x // x ≠ u ∧ x ≠ v}, G.Adj u x.1 ∧ G.Adj u y.1 ∧ x.1 ≠ y.1 ∧ ¬ G.Adj x.1 y.1 ∧ (G.induce {z | z ≠ u ∧ z ≠ v}).connectedComponentMk x ≠ (G.induce {z | z ≠ u ∧ z ≠ v}).connectedComponentMk y := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨c, d, hcd, hc, hd⟩ := exists_pair_deleted_components_touch_both_of_pair_delete_not_connected (G := G) hmindeg hall_connected huv hnot_conn obtain ⟨x, hxc, hxu⟩ := hc.1 obtain ⟨y, hyd, hyu⟩ := hd.1 have hcx : H.connectedComponentMk x = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hxc have hdy : H.connectedComponentMk y = d := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hyd have hcomp_ne : H.connectedComponentMk x ≠ H.connectedComponentMk y := by intro hcomp exact hcd (by rw [← hcx, ← hdy, hcomp]) have hxy : x.1 ≠ y.1 := by intro hxy exact hcomp_ne (by rw [Subtype.ext hxy]) have hnot_adj : ¬ G.Adj x.1 y.1 := by intro hxy_adj have hH_adj : H.Adj x y := hxy_adj exact hcomp_ne (SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hH_adj) refine ⟨x, y, hxu.symm, hyu.symm, hxy, hnot_adj, ?_⟩ simpa [H] using hcomp_ne lemma exists_nonadjacent_neighbors_right_of_pair_cut_not_connected {G : SimpleGraph V} [DecidableRel G.Adj] (hmindeg : ∀ x : V, 3 ≤ G.degree x) (hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected) {u v : V} (huv : u ≠ v) (hnot_conn : ¬ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ x y : {x // x ≠ u ∧ x ≠ v}, G.Adj v x.1 ∧ G.Adj v y.1 ∧ x.1 ≠ y.1 ∧ ¬ G.Adj x.1 y.1 ∧ (G.induce {z | z ≠ u ∧ z ≠ v}).connectedComponentMk x ≠ (G.induce {z | z ≠ u ∧ z ≠ v}).connectedComponentMk y := by classical let H : SimpleGraph {x // x ≠ u ∧ x ≠ v} := G.induce {x | x ≠ u ∧ x ≠ v} obtain ⟨c, d, hcd, hc, hd⟩ := exists_pair_deleted_components_touch_both_of_pair_delete_not_connected (G := G) hmindeg hall_connected huv hnot_conn obtain ⟨x, hxc, hxv⟩ := hc.2 obtain ⟨y, hyd, hyv⟩ := hd.2 have hcx : H.connectedComponentMk x = c := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hxc have hdy : H.connectedComponentMk y = d := by simpa [H, SimpleGraph.ConnectedComponent.mem_supp_iff] using hyd have hcomp_ne : H.connectedComponentMk x ≠ H.connectedComponentMk y := by intro hcomp exact hcd (by rw [← hcx, ← hdy, hcomp]) have hxy : x.1 ≠ y.1 := by intro hxy exact hcomp_ne (by rw [Subtype.ext hxy]) have hnot_adj : ¬ G.Adj x.1 y.1 := by intro hxy_adj have hH_adj : H.Adj x y := hxy_adj exact hcomp_ne (SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hH_adj) refine ⟨x, y, hxv.symm, hyv.symm, hxy, hnot_adj, ?_⟩ simpa [H] using hcomp_ne lemma exists_two_le_degree_of_path_length_two_le {G : SimpleGraph V} [DecidableRel G.Adj] {u v : V} {p : G.Walk u v} (hp : p.IsPath) (hlen : 2 ≤ p.length) : ∃ x : V, 2 ≤ G.degree x := by refine ⟨p.snd, two_le_degree_of_adj_of_adj_ne (G := G) (x := p.snd) (u := u) (w := p.getVert 2) (p.adj_snd ?_).symm ?_ ?_⟩ · rw [SimpleGraph.Walk.nil_iff_length_eq] omega · simpa using p.adj_getVert_succ (i := 1) (by omega) · intro h have h02 : p.getVert 0 = p.getVert 2 := by simp [h] have hidx : 0 = 2 := hp.getVert_injOn (by simp) (by simp [hlen]) h02 omega lemma exists_two_le_degree_of_connected_not_adj {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) {u v : V} (huv : u ≠ v) (hnadj : ¬ G.Adj u v) : ∃ x : V, 2 ≤ G.degree x := by obtain ⟨p, hp⟩ := hconn.exists_isPath u v have hlen0 : p.length ≠ 0 := by intro hlen exact huv (SimpleGraph.Walk.eq_of_length_eq_zero (p := p) hlen) have hlen1 : p.length ≠ 1 := by intro hlen exact hnadj (SimpleGraph.Walk.adj_of_length_eq_one (p := p) hlen) exact exists_two_le_degree_of_path_length_two_le (G := G) hp (by omega) omit [Fintype V] [DecidableEq V] in lemma exists_nonadjacent_neighbors_of_connected_ne_top {G : SimpleGraph V} (hconn : G.Connected) (hne_top : G ≠ ⊤) : ∃ (w u v : V), G.Adj w u ∧ G.Adj w v ∧ u ≠ v ∧ ¬ G.Adj u v := by obtain ⟨u, v, huv, hnadj⟩ := SimpleGraph.ne_top_iff_exists_not_adj.mp hne_top obtain ⟨p, hp⟩ := (hconn u v).exists_walk_length_eq_dist obtain ⟨x, a, b, hxa, hab, hxb, hne⟩ := SimpleGraph.Walk.exists_adj_adj_not_adj_ne hp ((hconn u v).one_lt_dist_of_ne_of_not_adj huv hnadj) exact ⟨a, x, b, hxa.symm, hab, hne, hxb⟩ omit [Fintype V] [DecidableEq V] in lemma exists_nonseparating_pair_of_forall_pair_deletion_connected {G : SimpleGraph V} (hconn : G.Connected) (hne_top : G ≠ ⊤) (hpair_connected : ∀ u v : V, u ≠ v → (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ (u v w : V) (_hwu : G.Adj w u) (_hwv : G.Adj w v), u ≠ v ∧ ¬ G.Adj u v ∧ (G.induce {x | x ≠ u ∧ x ≠ v}).Connected := by obtain ⟨w, u, v, hwu, hwv, huv, hnadj⟩ := exists_nonadjacent_neighbors_of_connected_ne_top (G := G) hconn hne_top exact ⟨u, v, w, hwu, hwv, huv, hnadj, hpair_connected u v huv⟩ theorem nonseparatingPairDeletionPath_of_twoCut : NonseparatingPairDeletionTwoCutStatement → NonseparatingPairDeletionPathStatement := by intro htwocut V _ _ G _ hconn hne_top hmindeg hall_connected by_cases hpair_connected : ∀ u v : V, u ≠ v → (G.induce {x | x ≠ u ∧ x ≠ v}).Connected · exact exists_nonseparating_pair_of_forall_pair_deletion_connected (G := G) hconn hne_top hpair_connected · push Not at hpair_connected obtain ⟨a, b, hab, hnot_conn⟩ := hpair_connected exact htwocut V G hconn hne_top hmindeg hall_connected ⟨a, b, hab, hnot_conn⟩ theorem nonseparatingPairDeletionPath_of_twoComponent : NonseparatingPairDeletionTwoComponentStatement → NonseparatingPairDeletionPathStatement := fun htwo => nonseparatingPairDeletionPath_of_twoCut (nonseparatingPairDeletionTwoCut_of_twoComponent htwo) theorem nonseparatingPairDeletionPath : NonseparatingPairDeletionPathStatement := nonseparatingPairDeletionPath_of_twoComponent nonseparatingPairDeletionTwoComponent lemma two_le_maxDegree_of_connected_ne_top {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) (hne_top : G ≠ ⊤) : 2 ≤ G.maxDegree := by obtain ⟨u, v, huv, hnadj⟩ := SimpleGraph.ne_top_iff_exists_not_adj.mp hne_top obtain ⟨x, hx⟩ := exists_two_le_degree_of_connected_not_adj (G := G) hconn huv hnadj exact hx.trans (G.degree_le_maxDegree x) lemma colorable_maxDegree_of_isAcyclic {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) (hne_top : G ≠ ⊤) (hacyc : G.IsAcyclic) : G.Colorable G.maxDegree := hacyc.colorable_two.mono (two_le_maxDegree_of_connected_ne_top (G := G) hconn hne_top) theorem brooksTheorem_of_nonAcyclic : BrooksNonAcyclicStatement → BrooksTheoremStatement := by intro hcore V _ _ G _ hconn hne_top hnot_odd by_cases hacyc : G.IsAcyclic · exact colorable_maxDegree_of_isAcyclic (G := G) hconn hne_top hacyc · exact hcore V G hconn hne_top hnot_odd hacyc theorem brooksNonAcyclic_of_degreeSplit : BrooksDegreeTwoStatement → BrooksDegreeAtLeastThreeStatement → BrooksNonAcyclicStatement := by intro htwo hthree V _ _ G _ hconn hne_top hnot_odd hnot_acyc have hdeg2 : 2 ≤ G.maxDegree := two_le_maxDegree_of_connected_ne_top (G := G) hconn hne_top obtain hEq | hLt := Nat.eq_or_lt_of_le hdeg2 · exact htwo V G hconn hne_top hnot_odd hnot_acyc hEq.symm · exact hthree V G hconn hne_top hnot_odd hnot_acyc (by omega) theorem brooksTheorem_of_degreeSplit : BrooksDegreeTwoStatement → BrooksDegreeAtLeastThreeStatement → BrooksTheoremStatement := fun htwo hthree => brooksTheorem_of_nonAcyclic (brooksNonAcyclic_of_degreeSplit htwo hthree) omit [Fintype V] [DecidableEq V] in lemma nontrivial_of_ne_top {G : SimpleGraph V} (hne_top : G ≠ ⊤) : Nontrivial V := by obtain ⟨u, v, huv, _⟩ := SimpleGraph.ne_top_iff_exists_not_adj.mp hne_top exact ⟨⟨u, v, huv⟩⟩ omit [DecidableEq V] in lemma degree_pos_of_connected_ne_top {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) (hne_top : G ≠ ⊤) (v : V) : 0 < G.degree v := by letI : Nontrivial V := nontrivial_of_ne_top (G := G) hne_top exact hconn.preconnected.degree_pos_of_nontrivial v omit [DecidableEq V] in lemma isCycles_of_forall_degree_eq_two {G : SimpleGraph V} [DecidableRel G.Adj] (hdeg : ∀ v : V, G.degree v = 2) : G.IsCycles := by intro v _hv rw [Set.ncard_eq_toFinset_card'] change (G.neighborFinset v).card = 2 exact hdeg v omit [DecidableEq V] in lemma degree_eq_two_of_isCycles_connected_ne_top {G : SimpleGraph V} [DecidableRel G.Adj] (hcycles : G.IsCycles) (hconn : G.Connected) (hne_top : G ≠ ⊤) (v : V) : G.degree v = 2 := by have hneighbor : (G.neighborSet v).Nonempty := by rw [← G.degree_pos_iff_nonempty] exact degree_pos_of_connected_ne_top (G := G) hconn hne_top v have hcard := hcycles hneighbor rw [Set.ncard_eq_toFinset_card'] at hcard change (G.neighborFinset v).card = 2 at hcard exact hcard omit [Fintype V] [DecidableEq V] in lemma connectedComponentMk_supp_eq_univ_of_connected {G : SimpleGraph V} (hconn : G.Connected) (v : V) : (G.connectedComponentMk v).supp = Set.univ := by ext w simp [SimpleGraph.ConnectedComponent.eq, hconn w v] lemma exists_spanning_cycle_of_isCycles_connected_ne_top {G : SimpleGraph V} [DecidableRel G.Adj] (hcycles : G.IsCycles) (hconn : G.Connected) (hne_top : G ≠ ⊤) : ∃ (v : V) (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = Set.univ := by obtain ⟨u, w, huw, hnadj⟩ := SimpleGraph.ne_top_iff_exists_not_adj.mp hne_top obtain ⟨v, hvdeg⟩ := exists_two_le_degree_of_connected_not_adj (G := G) hconn huw hnadj have hneighbor : (G.neighborSet v).Nonempty := by rw [← G.degree_pos_iff_nonempty] omega obtain ⟨p, hpcycle, hpverts⟩ := hcycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp (c := G.connectedComponentMk v) (v := v) (by simp) hneighbor exact ⟨v, p, hpcycle, by rw [hpverts, connectedComponentMk_supp_eq_univ_of_connected hconn v]⟩ omit [DecidableEq V] in lemma cycle_neighborSet_eq_of_maxDegree_le_two {G : SimpleGraph V} [DecidableRel G.Adj] {u x : V} {p : G.Walk u u} (hp : p.IsCycle) (hx : x ∈ p.support) (hmax : G.maxDegree ≤ 2) : p.toSubgraph.neighborSet x = G.neighborSet x := by refine Set.eq_of_subset_of_ncard_le (p.toSubgraph.neighborSet_subset x) ?_ have hGcard : (G.neighborSet x).ncard ≤ 2 := by rw [Set.ncard_eq_toFinset_card'] change (G.neighborFinset x).card ≤ 2 exact (G.degree_le_maxDegree x).trans hmax rw [hp.ncard_neighborSet_toSubgraph_eq_two hx] exact hGcard omit [DecidableEq V] in lemma not_adj_cycle_outside_of_maxDegree_le_two {G : SimpleGraph V} [DecidableRel G.Adj] {u x y : V} {p : G.Walk u u} (hp : p.IsCycle) (hx : x ∈ p.support) (hy : y ∉ p.support) (hmax : G.maxDegree ≤ 2) : ¬ G.Adj x y := by intro hxy have hsets := cycle_neighborSet_eq_of_maxDegree_le_two (G := G) hp hx hmax have hy_cycle : y ∈ p.toSubgraph.verts := by exact p.toSubgraph.neighborSet_subset_verts x (by simpa [hsets] using hxy) exact hy (p.mem_verts_toSubgraph.mp hy_cycle) omit [Fintype V] [DecidableEq V] in lemma exists_cycle_of_not_isAcyclic {G : SimpleGraph V} (hnot_acyc : ¬ G.IsAcyclic) : ∃ (v : V) (p : G.Walk v v), p.IsCycle := by classical by_contra hnone exact hnot_acyc (by intro v p hp exact hnone ⟨v, p, hp⟩) omit [DecidableEq V] in lemma exists_spanning_cycle_of_connected_not_acyclic_maxDegree_le_two {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) (hnot_acyc : ¬ G.IsAcyclic) (hmax : G.maxDegree ≤ 2) : ∃ (v : V) (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = Set.univ := by obtain ⟨v, p, hp⟩ := exists_cycle_of_not_isAcyclic (G := G) hnot_acyc refine ⟨v, p, hp, ?_⟩ rw [Set.eq_univ_iff_forall] intro y by_contra hy obtain ⟨q⟩ := hconn v y obtain ⟨d, _hd, hdin, hdout⟩ := q.exists_boundary_dart p.toSubgraph.verts p.start_mem_verts_toSubgraph hy have hdfst : d.fst ∈ p.support := p.mem_verts_toSubgraph.mp hdin have hdsnd : d.snd ∉ p.support := by intro hs exact hdout (p.mem_verts_toSubgraph.mpr hs) exact not_adj_cycle_outside_of_maxDegree_le_two (G := G) hp hdfst hdsnd hmax d.adj omit [DecidableEq V] in lemma eq_cycle_spanningCoe_of_spanning_cycle_maxDegree_le_two {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} {p : G.Walk v v} (hp : p.IsCycle) (hspan : p.toSubgraph.verts = Set.univ) (hmax : G.maxDegree ≤ 2) : G = p.toSubgraph.spanningCoe := by ext x y constructor · intro hxy have hxverts : x ∈ p.toSubgraph.verts := by rw [hspan] simp have hx : x ∈ p.support := p.mem_verts_toSubgraph.mp hxverts have hsets := cycle_neighborSet_eq_of_maxDegree_le_two (G := G) hp hx hmax change y ∈ p.toSubgraph.neighborSet x rw [hsets] exact hxy · intro hxy exact p.toSubgraph.adj_sub hxy omit [Fintype V] in lemma isHamiltonianCycle_of_spanning_isCycle {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) (hspan : p.toSubgraph.verts = Set.univ) : p.IsHamiltonianCycle := by rw [SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one] refine ⟨hp, ?_⟩ intro x have hx_support : x ∈ p.support := by rw [← p.mem_verts_toSubgraph, hspan] simp have hx_tail : x ∈ p.support.tail := by by_cases hxv : x = v · subst x exact p.end_mem_tail_support hp.not_nil · have hx_tail_walk : x ∈ p.tail.support := by rw [← p.cons_support_tail hp.not_nil] at hx_support exact (List.mem_cons.mp hx_support).resolve_left hxv rwa [← p.support_tail_of_not_nil hp.not_nil] exact List.count_eq_one_of_mem hp.support_nodup hx_tail lemma length_eq_card_of_spanning_cycle {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) (hspan : p.toSubgraph.verts = Set.univ) : p.length = Fintype.card V := (isHamiltonianCycle_of_spanning_isCycle (G := G) hp hspan).length_eq noncomputable def cycleTailEquivOfSpanning {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) (hspan : p.toSubgraph.verts = Set.univ) : Fin p.length ≃ V := by let hham := isHamiltonianCycle_of_spanning_isCycle (G := G) hp hspan have hlen : p.tail.support.length = p.length := by rw [SimpleGraph.Walk.length_support] exact SimpleGraph.Walk.length_tail_add_one hp.not_nil exact (finCongr hlen.symm).trans hham.isHamiltonian_tail.getVertEquiv omit [Fintype V] in lemma cycleTailEquivOfSpanning_apply_tail {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) (hspan : p.toSubgraph.verts = Set.univ) (i : Fin p.length) : cycleTailEquivOfSpanning (G := G) hp hspan i = p.tail.getVert i := by simp [cycleTailEquivOfSpanning] omit [Fintype V] in lemma cycleTailEquivOfSpanning_apply_getVert {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) (hspan : p.toSubgraph.verts = Set.univ) (i : Fin p.length) : cycleTailEquivOfSpanning (G := G) hp hspan i = p.getVert (i + 1) := by simp [cycleTailEquivOfSpanning] theorem brooksDegreeTwo_of_spanningCycleColoring : BrooksSpanningCycleColoringStatement → BrooksDegreeTwoStatement := by intro hcycle V _ _ G _ hconn hne_top hnot_odd hnot_acyc hmax have hmax_le_two : G.maxDegree ≤ 2 := by omega exact hcycle V G hne_top hnot_odd (exists_spanning_cycle_of_connected_not_acyclic_maxDegree_le_two (G := G) hconn hnot_acyc hmax_le_two) hmax theorem brooksTheorem_of_spanningCycleColoring_and_degreeAtLeastThree : BrooksSpanningCycleColoringStatement → BrooksDegreeAtLeastThreeStatement → BrooksTheoremStatement := fun hcycle hthree => brooksTheorem_of_degreeSplit (brooksDegreeTwo_of_spanningCycleColoring hcycle) hthree lemma cycleGraph_adj_iff_eq_add_or_sub {n : ℕ} [NeZero n] (hn : 2 ≤ n) {i j : Fin n} : (SimpleGraph.cycleGraph n).Adj i j ↔ j = i + 1 ∨ j = i - 1 := by rw [SimpleGraph.cycleGraph_adj'] constructor · intro h rcases h with h | h · right have hfin : i - j = 1 := by apply Fin.ext simpa [Nat.mod_eq_of_lt (by omega : 1 < n)] using h rw [sub_eq_iff_eq_add'] at hfin rw [hfin] simp · left have hfin : j - i = 1 := by apply Fin.ext simpa [Nat.mod_eq_of_lt (by omega : 1 < n)] using h rw [sub_eq_iff_eq_add'] at hfin rw [hfin] · intro h rcases h with rfl | rfl · right simp [Nat.mod_eq_of_lt (by omega : 1 < n)] · left simp [Nat.mod_eq_of_lt (by omega : 1 < n)] private lemma fin_val_add_one_of_last {n : ℕ} [NeZero n] (hn : 2 ≤ n) {i : Fin n} (hlast : i.val + 1 = n) : (i + 1).val = 0 := by rw [Fin.val_add] simp [Nat.mod_eq_of_lt (by omega : 1 < n), hlast] private lemma fin_val_add_one_of_not_last {n : ℕ} [NeZero n] {i : Fin n} (hnotlast : i.val + 1 ≠ n) : (i + 1).val = i.val + 1 := Fin.val_add_one_of_lt' (by omega) private lemma fin_val_sub_one_add_one_of_ne_zero {n : ℕ} [NeZero n] {i : Fin n} (hi0 : i ≠ 0) : (i - 1).val + 1 = i.val := by have hprev : (i - 1).val = i.val - 1 := Fin.val_sub_one_of_ne_zero hi0 have hpos : 0 < i.val := by rw [Fin.val_pos_iff, Fin.pos_iff_ne_zero'] exact hi0 omega private lemma fin_val_zero_sub_one_add_one {n : ℕ} [NeZero n] (hn : 2 ≤ n) : (((0 : Fin n) - 1).val + 1 = n) := by rw [sub_eq_add_neg, zero_add] rw [Fin.val_neg'] simp [Nat.mod_eq_of_lt (by omega : 1 < n)] omega omit [Fintype V] in lemma cycleTailEquivOfSpanning_neighborSet_toSubgraph {G : SimpleGraph V} {v : V} {p : G.Walk v v} [NeZero p.length] (hp : p.IsCycle) (hspan : p.toSubgraph.verts = Set.univ) (i : Fin p.length) : p.toSubgraph.neighborSet (cycleTailEquivOfSpanning (G := G) hp hspan i) = {cycleTailEquivOfSpanning (G := G) hp hspan (i - 1), cycleTailEquivOfSpanning (G := G) hp hspan (i + 1)} := by have hlen2 : 2 ≤ p.length := by have hlen3 := hp.three_le_length omega by_cases hlast : i.val + 1 = p.length · have hi_start : cycleTailEquivOfSpanning (G := G) hp hspan i = v := by rw [cycleTailEquivOfSpanning_apply_getVert (G := G) hp hspan] rw [hlast, p.getVert_length] have hi0 : i ≠ 0 := by intro hi subst i simp at hlast omega have hprev : (i - 1).val + 1 = p.length - 1 := by have hprev_i := fin_val_sub_one_add_one_of_ne_zero hi0 omega have hnext : (i + 1).val = 0 := fin_val_add_one_of_last hlen2 hlast rw [hi_start, hp.neighborSet_toSubgraph_endpoint] ext y simp [cycleTailEquivOfSpanning_apply_getVert, SimpleGraph.Walk.penultimate, hprev, hnext] tauto · have hinternal := hp.neighborSet_toSubgraph_internal (i := i.val + 1) (by omega) (by omega) rw [cycleTailEquivOfSpanning_apply_getVert (G := G) hp hspan, hinternal] have hnext : (i + 1).val = i.val + 1 := fin_val_add_one_of_not_last hlast ext y by_cases hi0 : i = 0 · subst i have hprev_zero : (((0 : Fin p.length) - 1).val + 1 = p.length) := fin_val_zero_sub_one_add_one hlen2 have hprev_neg : ((-1 : Fin p.length).val + 1 = p.length) := by simpa [sub_eq_add_neg] using hprev_zero have hone_mod : 1 % p.length = 1 := Nat.mod_eq_of_lt (by omega : 1 < p.length) simp [cycleTailEquivOfSpanning_apply_getVert, hprev_neg, hone_mod, SimpleGraph.Walk.getVert_length] · have hprev : (i - 1).val + 1 = i.val := fin_val_sub_one_add_one_of_ne_zero hi0 simp [cycleTailEquivOfSpanning_apply_getVert, hnext, hprev] omit [Fintype V] in noncomputable def cycleTailGraphIso {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) (hspan : p.toSubgraph.verts = Set.univ) : p.toSubgraph.spanningCoe ≃g SimpleGraph.cycleGraph p.length := by have hlen3 : 3 ≤ p.length := hp.three_le_length haveI : NeZero p.length := ⟨by omega⟩ let e := cycleTailEquivOfSpanning (G := G) hp hspan exact { e.symm with map_rel_iff' := by intro x y have hx : x = e (e.symm x) := (e.apply_symm_apply x).symm have hy : y = e (e.symm y) := (e.apply_symm_apply y).symm rw [hx, hy] change (SimpleGraph.cycleGraph p.length).Adj (e.symm (e (e.symm x))) (e.symm (e (e.symm y))) ↔ e (e.symm y) ∈ p.toSubgraph.neighborSet (e (e.symm x)) simp only [Equiv.symm_apply_apply] rw [cycleGraph_adj_iff_eq_add_or_sub (by omega : 2 ≤ p.length), cycleTailEquivOfSpanning_neighborSet_toSubgraph (G := G) hp hspan] simp only [Set.mem_insert_iff, Set.mem_singleton_iff] change e.symm y = e.symm x + 1 ∨ e.symm y = e.symm x - 1 ↔ e (e.symm y) = e (e.symm x - 1) ∨ e (e.symm y) = e (e.symm x + 1) constructor · intro h rcases h with h | h · right rw [h] · left rw [h] · intro h rcases h with h | h · right exact e.injective h · left exact e.injective h } theorem brooksSpanningCycleIso : BrooksSpanningCycleIsoStatement := by intro V _ _ G _ hcycle hmax obtain ⟨v, p, hp, hspan⟩ := hcycle refine ⟨p.length, hp.three_le_length, ?_⟩ have hmax_le_two : G.maxDegree ≤ 2 := by omega have hG := eq_cycle_spanningCoe_of_spanning_cycle_maxDegree_le_two (G := G) hp hspan hmax_le_two simpa [hG] using (show Nonempty (p.toSubgraph.spanningCoe ≃g SimpleGraph.cycleGraph p.length) from ⟨cycleTailGraphIso (G := G) hp hspan⟩) omit [Fintype V] [DecidableEq V] in lemma colorable_two_of_even_cycleGraph_iso {G : SimpleGraph V} {n : ℕ} (heven : Even n) (hiso : Nonempty (G ≃g SimpleGraph.cycleGraph n)) : G.Colorable 2 := by obtain ⟨e⟩ := hiso have hcycle : (SimpleGraph.cycleGraph n).Colorable 2 := by simpa using (SimpleGraph.cycleGraph.bicoloring_of_even n heven).colorable exact SimpleGraph.Colorable.of_hom e.toHom hcycle omit [Fintype V] [DecidableEq V] in lemma isOddCycleGraph_of_odd_cycleGraph_iso {G : SimpleGraph V} {n : ℕ} (hodd : Odd n) (hthree : 3 ≤ n) (hiso : Nonempty (G ≃g SimpleGraph.cycleGraph n)) : IsOddCycleGraph G := ⟨n, hodd, hthree, hiso⟩ theorem brooksSpanningCycleColoring_of_spanningCycleIso : BrooksSpanningCycleIsoStatement → BrooksSpanningCycleColoringStatement := by intro hiso V _ _ G _ _hne_top hnot_odd hcycle hmax obtain ⟨n, hthree, hGiso⟩ := hiso V G hcycle hmax have hcolor_two : G.Colorable 2 := by by_cases heven : Even n · exact colorable_two_of_even_cycleGraph_iso (G := G) heven hGiso · exact False.elim (hnot_odd (isOddCycleGraph_of_odd_cycleGraph_iso (G := G) (Nat.not_even_iff_odd.mp heven) hthree hGiso)) simpa [hmax] using hcolor_two theorem brooksTheorem_of_spanningCycleIso_and_degreeAtLeastThree : BrooksSpanningCycleIsoStatement → BrooksDegreeAtLeastThreeStatement → BrooksTheoremStatement := fun hiso hthree => brooksTheorem_of_spanningCycleColoring_and_degreeAtLeastThree (brooksSpanningCycleColoring_of_spanningCycleIso hiso) hthree theorem brooksSpanningCycleColoring : BrooksSpanningCycleColoringStatement := brooksSpanningCycleColoring_of_spanningCycleIso brooksSpanningCycleIso theorem brooksDegreeTwo : BrooksDegreeTwoStatement := brooksDegreeTwo_of_spanningCycleColoring brooksSpanningCycleColoring theorem brooksTheorem_of_degreeAtLeastThree : BrooksDegreeAtLeastThreeStatement → BrooksTheoremStatement := brooksTheorem_of_spanningCycleIso_and_degreeAtLeastThree brooksSpanningCycleIso theorem brooksHighDegreeNonregular_of_deleteColoring : BrooksHighDegreeDeleteColoringStatement → BrooksHighDegreeNonregularStatement := by intro hdel V _ _ G _ hconn hne_top hnot_odd hnot_acyclic hthree hlow obtain ⟨v, hv⟩ := hlow exact colorable_of_induce_compl_singleton_colorable_of_degree_lt (G := G) v (hdel V G hconn hne_top hnot_odd hnot_acyclic hthree v hv) hv theorem brooksHighDegreeDeleteColoring_of_componentColoring : BrooksHighDegreeDeleteComponentColoringStatement → BrooksHighDegreeDeleteColoringStatement := by intro hcomp V _ _ G _ hconn hne_top hnot_odd hnot_acyclic hthree v hv exact SimpleGraph.colorable_iff_forall_connectedComponents.mpr (hcomp V G hconn hne_top hnot_odd hnot_acyclic hthree v hv) lemma colorable_deleted_component {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) (v : V) (c : (G.induce {w | w ≠ v}).ConnectedComponent) : c.toSimpleGraph.Colorable G.maxDegree := by classical haveI : DecidablePred (fun x : {w // w ≠ v} => x ∈ c) := fun _ => Classical.propDecidable _ haveI : Fintype c := Subtype.fintype (fun x : {w // w ≠ v} => x ∈ c) haveI : DecidableRel c.toSimpleGraph.Adj := fun _ _ => Classical.propDecidable _ exact colorable_of_forall_finset_exists_low_degree (G := c.toSimpleGraph) (k := G.maxDegree) (exists_low_degree_in_deleted_component_induce (G := G) hconn v c) omit [Fintype V] [DecidableEq V] in lemma exists_coloring_eq_of_forall_component_colorable_of_ne_component {G : SimpleGraph V} {k : ℕ} {a b : V} (hcomp : ∀ c : G.ConnectedComponent, c.toSimpleGraph.Colorable k) (hcomp_ne : G.connectedComponentMk a ≠ G.connectedComponentMk b) : ∃ C : G.Coloring (Fin k), C a = C b := by classical let ca : G.ConnectedComponent := G.connectedComponentMk a let cb : G.ConnectedComponent := G.connectedComponentMk b let Ca : ca.toSimpleGraph.Coloring (Fin k) := (hcomp ca).some let target : Fin k := Ca ⟨a, SimpleGraph.ConnectedComponent.connectedComponentMk_mem⟩ let componentColoring : (c : G.ConnectedComponent) → c.toSimpleGraph.Coloring (Fin k) := fun c => if hc : c = cb then let Cc : c.toSimpleGraph.Coloring (Fin k) := (hcomp c).some let bc : c := ⟨b, by simpa [cb, hc] using (SimpleGraph.ConnectedComponent.connectedComponentMk_mem (G := G) (v := b))⟩ (c.toSimpleGraph.recolorOfEquiv (Equiv.swap (Cc bc) target)) Cc else (hcomp c).some refine ⟨G.homOfConnectedComponents componentColoring, ?_⟩ have hca : componentColoring ca = Ca := by dsimp [componentColoring, ca, cb, Ca] split_ifs with h · exact False.elim (hcomp_ne h) · rfl have ha : (G.homOfConnectedComponents componentColoring) a = target := by change componentColoring (G.connectedComponentMk a) ⟨a, SimpleGraph.ConnectedComponent.connectedComponentMk_mem⟩ = target simpa [ca, target] using congrFun (congrArg DFunLike.coe hca) ⟨a, SimpleGraph.ConnectedComponent.connectedComponentMk_mem⟩ have hb : (G.homOfConnectedComponents componentColoring) b = target := by change componentColoring (G.connectedComponentMk b) ⟨b, SimpleGraph.ConnectedComponent.connectedComponentMk_mem⟩ = target simp [componentColoring, cb, target] exact ha.trans hb.symm lemma exists_deleted_vertex_coloring_eq_of_ne_component {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) {u v w : V} (hu : u ≠ w) (hv : v ≠ w) (hcomp_ne : (G.induce {x | x ≠ w}).connectedComponentMk ⟨u, hu⟩ ≠ (G.induce {x | x ≠ w}).connectedComponentMk ⟨v, hv⟩) : ∃ C : (G.induce {x | x ≠ w}).Coloring (Fin G.maxDegree), C ⟨u, hu⟩ = C ⟨v, hv⟩ := exists_coloring_eq_of_forall_component_colorable_of_ne_component (G := G.induce {x | x ≠ w}) (k := G.maxDegree) (fun c => colorable_deleted_component (G := G) hconn w c) hcomp_ne lemma colorable_of_delete_vertex_neighbors_in_different_components {G : SimpleGraph V} [DecidableRel G.Adj] (hconn : G.Connected) {u v w : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (huv : u ≠ v) (hcomp_ne : (G.induce {x | x ≠ w}).connectedComponentMk ⟨u, (G.ne_of_adj hwu).symm⟩ ≠ (G.induce {x | x ≠ w}).connectedComponentMk ⟨v, (G.ne_of_adj hwv).symm⟩) : G.Colorable G.maxDegree := colorable_of_delete_vertex_coloring_eq_on_neighbors (G := G) hwu hwv huv (exists_deleted_vertex_coloring_eq_of_ne_component (G := G) hconn (G.ne_of_adj hwu).symm (G.ne_of_adj hwv).symm hcomp_ne) (G.degree_le_maxDegree w) lemma exists_deleted_vertex_coloring_eq_of_connected_compl_pair {G : SimpleGraph V} [DecidableRel G.Adj] (hregular : ∀ x : V, G.degree x = G.maxDegree) {u v w z : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (hwz : G.Adj w z) (hzu : z ≠ u) (hzv : z ≠ v) (hnadj : ¬ G.Adj u v) (hconn_pair : ((G.induce {x | x ≠ w}).induce {x : {x // x ≠ w} | x ≠ ⟨u, (G.ne_of_adj hwu).symm⟩ ∧ x ≠ ⟨v, (G.ne_of_adj hwv).symm⟩}).Connected) : ∃ C : (G.induce {x | x ≠ w}).Coloring (Fin G.maxDegree), C ⟨u, (G.ne_of_adj hwu).symm⟩ = C ⟨v, (G.ne_of_adj hwv).symm⟩ := by classical let H : SimpleGraph {x // x ≠ w} := G.induce {x | x ≠ w} let uH : {x // x ≠ w} := ⟨u, (G.ne_of_adj hwu).symm⟩ let vH : {x // x ≠ w} := ⟨v, (G.ne_of_adj hwv).symm⟩ let zH : {x // x ≠ w} := ⟨z, (G.ne_of_adj hwz).symm⟩ have hk : 0 < G.maxDegree := by have hdeg_pos : 0 < G.degree w := by rw [← G.card_neighborFinset_eq_degree] exact Finset.card_pos.mpr ⟨u, by rw [G.mem_neighborFinset]; exact hwu⟩ rwa [hregular w] at hdeg_pos have hnadjH : ¬ H.Adj uH vH := by intro huvH exact hnadj huvH have hdeg_le_H : ∀ x : {x // x ≠ w}, H.degree x ≤ G.maxDegree := by intro x exact (degree_induce_le (G := G) (s := {x | x ≠ w}) x).trans (G.degree_le_maxDegree x.1) have hzdegH : H.degree zH < G.maxDegree := by have hlt : H.degree zH < G.degree z := degree_induce_lt_of_adj_notMem (G := G) (s := {x | x ≠ w}) (x := z) (y := w) (by exact zH.2) (by simp) hwz.symm simpa [H, zH, hregular z] using hlt have hlow : ∀ s : Finset {x // x ≠ w}, uH ∈ s → vH ∈ s → (∃ x ∈ s, x ≠ uH ∧ x ≠ vH) → ∃ x : {y // y ∈ s}, x.1 ≠ uH ∧ x.1 ≠ vH ∧ (H.induce ((s : Finset {x // x ≠ w}) : Set {x // x ≠ w})).degree x < G.maxDegree := exists_low_degree_outside_pair_of_connected_compl_pair (G := H) (k := G.maxDegree) (u := uH) (v := vH) (z := zH) (by simpa [H, uH, vH] using hconn_pair) hdeg_le_H (by intro h; exact hzu (congrArg Subtype.val h)) (by intro h; exact hzv (congrArg Subtype.val h)) hzdegH obtain ⟨C, hCuv⟩ := exists_coloring_eq_induce_finset_of_forall_exists_low_degree_except_pair (G := H) (k := G.maxDegree) (u := uH) (v := vH) hk hnadjH hlow Finset.univ (by simp) (by simp) refine ⟨SimpleGraph.Coloring.mk (G := H) (fun x => C ⟨x, by simp⟩) ?_, ?_⟩ · intro x y hxy exact C.valid hxy · simpa [H, uH, vH] using hCuv lemma colorable_of_delete_vertex_neighbors_connected_compl_pair {G : SimpleGraph V} [DecidableRel G.Adj] (hregular : ∀ x : V, G.degree x = G.maxDegree) {u v w z : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (hwz : G.Adj w z) (huv : u ≠ v) (hzu : z ≠ u) (hzv : z ≠ v) (hnadj : ¬ G.Adj u v) (hconn_pair : ((G.induce {x | x ≠ w}).induce {x : {x // x ≠ w} | x ≠ ⟨u, (G.ne_of_adj hwu).symm⟩ ∧ x ≠ ⟨v, (G.ne_of_adj hwv).symm⟩}).Connected) : G.Colorable G.maxDegree := colorable_of_delete_vertex_coloring_eq_on_neighbors (G := G) hwu hwv huv (exists_deleted_vertex_coloring_eq_of_connected_compl_pair (G := G) hregular hwu hwv hwz hzu hzv hnadj hconn_pair) (by rw [hregular w]) lemma exists_deleted_vertex_coloring_eq_of_connected_delete_pair {G : SimpleGraph V} [DecidableRel G.Adj] (hregular : ∀ x : V, G.degree x = G.maxDegree) {u v w z : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (hwz : G.Adj w z) (hzu : z ≠ u) (hzv : z ≠ v) (hnadj : ¬ G.Adj u v) (hconn_pair : (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : ∃ C : (G.induce {x | x ≠ w}).Coloring (Fin G.maxDegree), C ⟨u, (G.ne_of_adj hwu).symm⟩ = C ⟨v, (G.ne_of_adj hwv).symm⟩ := by classical let H : SimpleGraph {x // x ≠ w} := G.induce {x | x ≠ w} let uH : {x // x ≠ w} := ⟨u, (G.ne_of_adj hwu).symm⟩ let vH : {x // x ≠ w} := ⟨v, (G.ne_of_adj hwv).symm⟩ have hk : 0 < G.maxDegree := by have hdeg_pos : 0 < G.degree w := by rw [← G.card_neighborFinset_eq_degree] exact Finset.card_pos.mpr ⟨u, by rw [G.mem_neighborFinset]; exact hwu⟩ rwa [hregular w] at hdeg_pos have hnadjH : ¬ H.Adj uH vH := by intro huvH exact hnadj huvH have hlow : ∀ s : Finset {x // x ≠ w}, uH ∈ s → vH ∈ s → (∃ x ∈ s, x ≠ uH ∧ x ≠ vH) → ∃ x : {y // y ∈ s}, x.1 ≠ uH ∧ x.1 ≠ vH ∧ (H.induce ((s : Finset {x // x ≠ w}) : Set {x // x ≠ w})).degree x < G.maxDegree := by simpa [H, uH, vH] using exists_low_degree_outside_pair_of_connected_delete_pair (G := G) (k := G.maxDegree) (u := u) (v := v) (w := w) (z := z) hwu hwv hwz hconn_pair (fun x => G.degree_le_maxDegree x) hzu hzv obtain ⟨C, hCuv⟩ := exists_coloring_eq_induce_finset_of_forall_exists_low_degree_except_pair (G := H) (k := G.maxDegree) (u := uH) (v := vH) hk hnadjH hlow Finset.univ (by simp) (by simp) refine ⟨SimpleGraph.Coloring.mk (G := H) (fun x => C ⟨x, by simp⟩) ?_, ?_⟩ · intro x y hxy exact C.valid hxy · simpa [H, uH, vH] using hCuv lemma colorable_of_delete_vertex_neighbors_connected_delete_pair {G : SimpleGraph V} [DecidableRel G.Adj] (hregular : ∀ x : V, G.degree x = G.maxDegree) {u v w z : V} (hwu : G.Adj w u) (hwv : G.Adj w v) (hwz : G.Adj w z) (huv : u ≠ v) (hzu : z ≠ u) (hzv : z ≠ v) (hnadj : ¬ G.Adj u v) (hconn_pair : (G.induce {x | x ≠ u ∧ x ≠ v}).Connected) : G.Colorable G.maxDegree := colorable_of_delete_vertex_coloring_eq_on_neighbors (G := G) hwu hwv huv (exists_deleted_vertex_coloring_eq_of_connected_delete_pair (G := G) hregular hwu hwv hwz hzu hzv hnadj hconn_pair) (by rw [hregular w]) theorem brooksHighDegreeDeleteComponentColoring : BrooksHighDegreeDeleteComponentColoringStatement := by intro V _ _ G _ hconn _hne_top _hnot_odd _hnot_acyclic _hthree v _hv c exact colorable_deleted_component (G := G) hconn v c theorem brooksDegreeAtLeastThree_of_highDegreeSplit : BrooksHighDegreeNonregularStatement → BrooksHighDegreeRegularStatement → BrooksDegreeAtLeastThreeStatement := by intro hnon hreg V _ _ G _ hconn hne_top hnot_odd hnot_acyclic hthree by_cases hregular : ∀ v : V, G.degree v = G.maxDegree · exact hreg V G hconn hne_top hnot_odd hnot_acyclic hthree hregular · push Not at hregular obtain ⟨v, hv⟩ := hregular have hlt : G.degree v < G.maxDegree := lt_of_le_of_ne (G.degree_le_maxDegree v) hv exact hnon V G hconn hne_top hnot_odd hnot_acyclic hthree ⟨v, hlt⟩ theorem brooksTheorem_of_highDegreeSplit : BrooksHighDegreeNonregularStatement → BrooksHighDegreeRegularStatement → BrooksTheoremStatement := fun hnon hreg => brooksTheorem_of_degreeAtLeastThree (brooksDegreeAtLeastThree_of_highDegreeSplit hnon hreg) theorem brooksDegreeAtLeastThree_of_deleteColoring_and_regular : BrooksHighDegreeDeleteColoringStatement → BrooksHighDegreeRegularStatement → BrooksDegreeAtLeastThreeStatement := fun hdel hreg => brooksDegreeAtLeastThree_of_highDegreeSplit (brooksHighDegreeNonregular_of_deleteColoring hdel) hreg theorem brooksTheorem_of_deleteColoring_and_highDegreeRegular : BrooksHighDegreeDeleteColoringStatement → BrooksHighDegreeRegularStatement → BrooksTheoremStatement := fun hdel hreg => brooksTheorem_of_degreeAtLeastThree (brooksDegreeAtLeastThree_of_deleteColoring_and_regular hdel hreg) theorem brooksTheorem_of_deleteComponentColoring_and_highDegreeRegular : BrooksHighDegreeDeleteComponentColoringStatement → BrooksHighDegreeRegularStatement → BrooksTheoremStatement := fun hcomp hreg => brooksTheorem_of_deleteColoring_and_highDegreeRegular (brooksHighDegreeDeleteColoring_of_componentColoring hcomp) hreg theorem brooksDegreeAtLeastThree_of_highDegreeRegular : BrooksHighDegreeRegularStatement → BrooksDegreeAtLeastThreeStatement := fun hreg => brooksDegreeAtLeastThree_of_deleteColoring_and_regular (brooksHighDegreeDeleteColoring_of_componentColoring brooksHighDegreeDeleteComponentColoring) hreg theorem brooksTheorem_of_highDegreeRegular : BrooksHighDegreeRegularStatement → BrooksTheoremStatement := fun hreg => brooksTheorem_of_deleteComponentColoring_and_highDegreeRegular brooksHighDegreeDeleteComponentColoring hreg theorem brooksHighDegreeRegular_of_pairColoring : BrooksHighDegreeRegularPairColoringStatement → BrooksHighDegreeRegularStatement := by intro hpair V _ _ G _ hconn hne_top hnot_odd hnot_acyclic hthree hregular obtain ⟨u, v, w, hwu, hwv, huv, hcolor⟩ := hpair V G hconn hne_top hnot_odd hnot_acyclic hthree hregular exact colorable_of_delete_vertex_coloring_eq_on_neighbors (G := G) hwu hwv huv hcolor (by rw [hregular w]) theorem brooksDegreeAtLeastThree_of_regularPairColoring : BrooksHighDegreeRegularPairColoringStatement → BrooksDegreeAtLeastThreeStatement := fun hpair => brooksDegreeAtLeastThree_of_highDegreeRegular (brooksHighDegreeRegular_of_pairColoring hpair) theorem brooksTheorem_of_regularPairColoring : BrooksHighDegreeRegularPairColoringStatement → BrooksTheoremStatement := fun hpair => brooksTheorem_of_highDegreeRegular (brooksHighDegreeRegular_of_pairColoring hpair) theorem brooksHighDegreeRegularPairColoring_of_pairDeletion : BrooksHighDegreeRegularPairDeletionStatement → BrooksHighDegreeRegularPairColoringStatement := by intro hpairdel V _ _ G _ hconn hne_top hnot_odd hnot_acyclic hthree hregular by_cases hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected · obtain ⟨u, v, w, hwu, hwv, huv, hnadj, hconn_pair⟩ := hpairdel V G hconn hne_top hnot_odd hnot_acyclic hthree hregular hall_connected refine ⟨u, v, w, hwu, hwv, huv, ?_⟩ have hthree_w : 3 ≤ G.degree w := by rwa [hregular w] obtain ⟨z, hwz, hzu, hzv⟩ := exists_neighbor_ne_pair_of_three_le_degree (G := G) (w := w) (u := u) (v := v) hthree_w exact exists_deleted_vertex_coloring_eq_of_connected_delete_pair (G := G) hregular hwu hwv hwz hzu hzv hnadj hconn_pair · push Not at hall_connected obtain ⟨w, hnot_conn⟩ := hall_connected have hdegree_pos : 0 < G.degree w := by rw [hregular w] omega obtain ⟨x, hwx⟩ := (G.degree_pos_iff_exists_adj w).mp hdegree_pos obtain ⟨u, v, hwu, hwv, huv, _hnadj, hcomp_ne⟩ := exists_separated_neighbors_of_delete_not_connected (G := G) hconn hwx hnot_conn exact ⟨u, v, w, hwu, hwv, huv, exists_deleted_vertex_coloring_eq_of_ne_component (G := G) hconn (G.ne_of_adj hwu).symm (G.ne_of_adj hwv).symm hcomp_ne⟩ theorem brooksHighDegreeRegular_of_pairDeletion : BrooksHighDegreeRegularPairDeletionStatement → BrooksHighDegreeRegularStatement := fun hpairdel => brooksHighDegreeRegular_of_pairColoring (brooksHighDegreeRegularPairColoring_of_pairDeletion hpairdel) theorem brooksDegreeAtLeastThree_of_pairDeletion : BrooksHighDegreeRegularPairDeletionStatement → BrooksDegreeAtLeastThreeStatement := fun hpairdel => brooksDegreeAtLeastThree_of_regularPairColoring (brooksHighDegreeRegularPairColoring_of_pairDeletion hpairdel) theorem brooksTheorem_of_pairDeletion : BrooksHighDegreeRegularPairDeletionStatement → BrooksTheoremStatement := fun hpairdel => brooksTheorem_of_regularPairColoring (brooksHighDegreeRegularPairColoring_of_pairDeletion hpairdel) theorem brooksHighDegreeRegularPairDeletion_of_nonseparatingPairDeletion : NonseparatingPairDeletionPathStatement → BrooksHighDegreeRegularPairDeletionStatement := by intro hpath V _ _ G _ hconn hne_top _hnot_odd _hnot_acyclic hthree hregular hall_connected exact hpath V G hconn hne_top (fun x => by rw [hregular x]; exact hthree) hall_connected theorem brooksHighDegreeRegularPairColoring_of_nonseparatingPairDeletion : NonseparatingPairDeletionPathStatement → BrooksHighDegreeRegularPairColoringStatement := fun hpath => brooksHighDegreeRegularPairColoring_of_pairDeletion (brooksHighDegreeRegularPairDeletion_of_nonseparatingPairDeletion hpath) theorem brooksHighDegreeRegular_of_nonseparatingPairDeletion : NonseparatingPairDeletionPathStatement → BrooksHighDegreeRegularStatement := fun hpath => brooksHighDegreeRegular_of_pairDeletion (brooksHighDegreeRegularPairDeletion_of_nonseparatingPairDeletion hpath) theorem brooksDegreeAtLeastThree_of_nonseparatingPairDeletion : NonseparatingPairDeletionPathStatement → BrooksDegreeAtLeastThreeStatement := fun hpath => brooksDegreeAtLeastThree_of_pairDeletion (brooksHighDegreeRegularPairDeletion_of_nonseparatingPairDeletion hpath) theorem brooksTheorem_of_nonseparatingPairDeletion : NonseparatingPairDeletionPathStatement → BrooksTheoremStatement := fun hpath => brooksTheorem_of_pairDeletion (brooksHighDegreeRegularPairDeletion_of_nonseparatingPairDeletion hpath) theorem brooksHighDegreeRegularPairColoring_of_structural : BrooksHighDegreeRegularStructuralStatement → BrooksHighDegreeRegularPairColoringStatement := by intro hstruct V _ _ G _ hconn hne_top hnot_odd hnot_acyclic hthree hregular obtain ⟨u, v, w, hwu, hwv, huv, hnadj, hcase⟩ := hstruct V G hconn hne_top hnot_odd hnot_acyclic hthree hregular refine ⟨u, v, w, hwu, hwv, huv, ?_⟩ rcases hcase with hcomp_ne | hconn_pair · exact exists_deleted_vertex_coloring_eq_of_ne_component (G := G) hconn (G.ne_of_adj hwu).symm (G.ne_of_adj hwv).symm hcomp_ne · obtain ⟨z, hwz, hzu, hzv, hconn_pair⟩ := hconn_pair exact exists_deleted_vertex_coloring_eq_of_connected_compl_pair (G := G) hregular hwu hwv hwz hzu hzv hnadj hconn_pair theorem brooksHighDegreeRegular_of_structural : BrooksHighDegreeRegularStructuralStatement → BrooksHighDegreeRegularStatement := fun hstruct => brooksHighDegreeRegular_of_pairColoring (brooksHighDegreeRegularPairColoring_of_structural hstruct) theorem brooksDegreeAtLeastThree_of_regularStructural : BrooksHighDegreeRegularStructuralStatement → BrooksDegreeAtLeastThreeStatement := fun hstruct => brooksDegreeAtLeastThree_of_regularPairColoring (brooksHighDegreeRegularPairColoring_of_structural hstruct) theorem brooksTheorem_of_regularStructural : BrooksHighDegreeRegularStructuralStatement → BrooksTheoremStatement := fun hstruct => brooksTheorem_of_regularPairColoring (brooksHighDegreeRegularPairColoring_of_structural hstruct) theorem brooksHighDegreeRegularStructural_of_connectivity : BrooksHighDegreeRegularConnectivityStatement → BrooksHighDegreeRegularStructuralStatement := by intro hconnect V _ _ G _ hconn hne_top hnot_odd hnot_acyclic hthree hregular obtain ⟨u, v, w, hwu, hwv, huv, hnadj, hcase⟩ := hconnect V G hconn hne_top hnot_odd hnot_acyclic hthree hregular refine ⟨u, v, w, hwu, hwv, huv, hnadj, ?_⟩ rcases hcase with hcomp_ne | hconn_pair · exact Or.inl hcomp_ne · refine Or.inr ?_ have hthree_w : 3 ≤ G.degree w := by rwa [hregular w] obtain ⟨z, hwz, hzu, hzv⟩ := exists_neighbor_ne_pair_of_three_le_degree (G := G) (w := w) (u := u) (v := v) hthree_w exact ⟨z, hwz, hzu, hzv, hconn_pair⟩ theorem brooksHighDegreeRegularPairColoring_of_connectivity : BrooksHighDegreeRegularConnectivityStatement → BrooksHighDegreeRegularPairColoringStatement := fun hconnect => brooksHighDegreeRegularPairColoring_of_structural (brooksHighDegreeRegularStructural_of_connectivity hconnect) theorem brooksHighDegreeRegular_of_connectivity : BrooksHighDegreeRegularConnectivityStatement → BrooksHighDegreeRegularStatement := fun hconnect => brooksHighDegreeRegular_of_structural (brooksHighDegreeRegularStructural_of_connectivity hconnect) theorem brooksDegreeAtLeastThree_of_regularConnectivity : BrooksHighDegreeRegularConnectivityStatement → BrooksDegreeAtLeastThreeStatement := fun hconnect => brooksDegreeAtLeastThree_of_regularStructural (brooksHighDegreeRegularStructural_of_connectivity hconnect) theorem brooksTheorem_of_regularConnectivity : BrooksHighDegreeRegularConnectivityStatement → BrooksTheoremStatement := fun hconnect => brooksTheorem_of_regularStructural (brooksHighDegreeRegularStructural_of_connectivity hconnect) theorem brooksHighDegreeRegularConnectivity_of_twoConnectedSelection : BrooksHighDegreeRegularTwoConnectedSelectionStatement → BrooksHighDegreeRegularConnectivityStatement := by intro hselect V _ _ G _ hconn hne_top hnot_odd hnot_acyclic hthree hregular by_cases hall_connected : ∀ w : V, (G.induce {x | x ≠ w}).Connected · obtain ⟨u, v, w, hwu, hwv, huv, hnadj, hconn_pair⟩ := hselect V G hconn hne_top hnot_odd hnot_acyclic hthree hregular hall_connected exact ⟨u, v, w, hwu, hwv, huv, hnadj, Or.inr hconn_pair⟩ · push Not at hall_connected obtain ⟨w, hnot_conn⟩ := hall_connected have hdegree_pos : 0 < G.degree w := by rw [hregular w] omega obtain ⟨x, hwx⟩ := (G.degree_pos_iff_exists_adj w).mp hdegree_pos obtain ⟨u, v, hwu, hwv, huv, hnadj, hcomp_ne⟩ := exists_separated_neighbors_of_delete_not_connected (G := G) hconn hwx hnot_conn exact ⟨u, v, w, hwu, hwv, huv, hnadj, Or.inl hcomp_ne⟩ theorem brooksHighDegreeRegularStructural_of_twoConnectedSelection : BrooksHighDegreeRegularTwoConnectedSelectionStatement → BrooksHighDegreeRegularStructuralStatement := fun hselect => brooksHighDegreeRegularStructural_of_connectivity (brooksHighDegreeRegularConnectivity_of_twoConnectedSelection hselect) theorem brooksHighDegreeRegularPairColoring_of_twoConnectedSelection : BrooksHighDegreeRegularTwoConnectedSelectionStatement → BrooksHighDegreeRegularPairColoringStatement := fun hselect => brooksHighDegreeRegularPairColoring_of_connectivity (brooksHighDegreeRegularConnectivity_of_twoConnectedSelection hselect) theorem brooksHighDegreeRegular_of_twoConnectedSelection : BrooksHighDegreeRegularTwoConnectedSelectionStatement → BrooksHighDegreeRegularStatement := fun hselect => brooksHighDegreeRegular_of_connectivity (brooksHighDegreeRegularConnectivity_of_twoConnectedSelection hselect) theorem brooksDegreeAtLeastThree_of_regularTwoConnectedSelection : BrooksHighDegreeRegularTwoConnectedSelectionStatement → BrooksDegreeAtLeastThreeStatement := fun hselect => brooksDegreeAtLeastThree_of_regularConnectivity (brooksHighDegreeRegularConnectivity_of_twoConnectedSelection hselect) theorem brooksTheorem_of_regularTwoConnectedSelection : BrooksHighDegreeRegularTwoConnectedSelectionStatement → BrooksTheoremStatement := fun hselect => brooksTheorem_of_regularConnectivity (brooksHighDegreeRegularConnectivity_of_twoConnectedSelection hselect) theorem brooksHighDegreeRegularTwoConnectedSelection_of_nonseparatingPath : NonseparatingLengthTwoPathStatement → BrooksHighDegreeRegularTwoConnectedSelectionStatement := by intro hpath V _ _ G _ hconn hne_top _hnot_odd _hnot_acyclic _hthree _hregular hall_connected exact hpath V G hconn hne_top hall_connected theorem brooksHighDegreeRegularConnectivity_of_nonseparatingPath : NonseparatingLengthTwoPathStatement → BrooksHighDegreeRegularConnectivityStatement := fun hpath => brooksHighDegreeRegularConnectivity_of_twoConnectedSelection (brooksHighDegreeRegularTwoConnectedSelection_of_nonseparatingPath hpath) theorem brooksHighDegreeRegular_of_nonseparatingPath : NonseparatingLengthTwoPathStatement → BrooksHighDegreeRegularStatement := fun hpath => brooksHighDegreeRegular_of_twoConnectedSelection (brooksHighDegreeRegularTwoConnectedSelection_of_nonseparatingPath hpath) theorem brooksDegreeAtLeastThree_of_nonseparatingPath : NonseparatingLengthTwoPathStatement → BrooksDegreeAtLeastThreeStatement := fun hpath => brooksDegreeAtLeastThree_of_regularTwoConnectedSelection (brooksHighDegreeRegularTwoConnectedSelection_of_nonseparatingPath hpath) theorem brooksTheorem_of_nonseparatingPath : NonseparatingLengthTwoPathStatement → BrooksTheoremStatement := fun hpath => brooksTheorem_of_regularTwoConnectedSelection (brooksHighDegreeRegularTwoConnectedSelection_of_nonseparatingPath hpath) theorem brooksTheorem : BrooksTheoremStatement := brooksTheorem_of_nonseparatingPairDeletion nonseparatingPairDeletionPath end AtlasKnownTheorems.BrooksTheorem