import Mathlib.Combinatorics.SimpleGraph.Basic import Mathlib.Combinatorics.SimpleGraph.Finite import Mathlib.Combinatorics.SimpleGraph.Coloring import Mathlib.Combinatorics.SimpleGraph.Subgraph import Mathlib.Combinatorics.SimpleGraph.Path import Mathlib.Combinatorics.SimpleGraph.Walk import Mathlib.Combinatorics.SimpleGraph.Maps import Mathlib.Order.Disjoint import Mathlib.Data.List.Basic import Mathlib.Data.List.Lemmas import Mathlib.Data.Fintype.Basic import Mathlib.Data.Fintype.Sets import Mathlib.Data.Set.Basic import Mathlib.Tactic.Linarith open SimpleGraph List Walk Set.Notation open Classical variable {α : Type} {V : Type} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] namespace List abbrev toSet (l : List α) := { x | x ∈ l } lemma toSet_nil : ([] : List α).toSet = ∅ := by simp_all only [toSet, not_mem_nil, Set.setOf_false] noncomputable def extend_coloring (S : Set V) (S_coloring : Coloring (G.induce S) α) (v : V) (c : α) (h : c ∉ S_coloring '' (S ↓∩ G.neighborSet v)) : Coloring (G.induce (S ∪ {v})) α := by simp at h apply Coloring.mk case color => intro ⟨x, mem⟩ by_cases hx : x ∈ S · exact S_coloring ⟨x, hx⟩ · exact c case valid => rintro ⟨x₁, mem_x₁⟩ ⟨x₂, mem_x₂⟩ intro adj by_cases hx₁ : x₁ ∈ S <;> by_cases hx₂ : x₂ ∈ S -- 4 cases according to whether x₁ and/or x₂ are in S or not · simp [hx₁, hx₂] exact S_coloring.valid adj · simp [hx₁, hx₂] replace hx₂ : x₂ = v := mem_x₂.resolve_left hx₂ simp [hx₂] at adj exact h x₁ (G.adj_symm adj) hx₁ · simp [hx₁, hx₂] replace hx₁ : x₁ = v := mem_x₁.resolve_left hx₁ simp [hx₁] at adj -- TODO the following 2 lines are kind of cumbersome intro wrong exact (h x₂ adj hx₂) (Eq.symm wrong) · intro a simp_all only [comap_adj, Function.Embedding.coe_subtype] simp_all only [Set.union_singleton, Set.mem_insert_iff, or_false, SimpleGraph.irrefl] lemma preimage_val_card {A B : Set V} : (A ↓∩ B).toFinset.card = (A ∩ B).toFinset.card := by apply Finset.card_bij' case i => exact fun a _ => ↑a case j => intro a h simp only [Set.toFinset_inter, Finset.mem_inter, Set.mem_toFinset] at h exact ⟨a, h.left⟩ case hi => intro a ha simp_all only [not_false_eq_true, true_and, Set.mem_toFinset, Set.mem_preimage, Set.toFinset_inter, Finset.mem_inter, Subtype.coe_prop, and_self] case hj => intro a ha simp_all only [not_false_eq_true, true_and, Set.mem_toFinset, Set.mem_preimage] simp_all only [Set.toFinset_inter, Finset.mem_inter, Set.mem_toFinset] case left_inv => intro a ha simp_all only [not_false_eq_true, true_and, Subtype.coe_eta] case right_inv => intro a ha simp_all only [not_false_eq_true, true_and] theorem color_path (k : ℕ) (maxDeg_le_k : G.maxDegree ≤ k) {u v : V} (P : G.Path u v) (S : Set V) (P_outside_S : ∀ x ∈ P.val.support, x ∉ S) (S_colorable : Colorable (G.induce S) k) : Colorable (G.induce (S ∪ P.val.support.tail.toSet)) k := by classical let ⟨W, W_is_path⟩ := P cases W with | nil => simp rw [List.toSet_nil, Set.union_empty] exact S_colorable | @cons u w v adj W' => simp at * let P' : G.Path w v := ⟨W', IsPath.of_cons W_is_path⟩ have P'_colorable := color_path k maxDeg_le_k P' S (P_outside_S.right) S_colorable let P'_coloring := P'_colorable.some let N := G.neighborSet w -- set of vertices already colored by P'_coloring let C := S ∪ W'.support.tail.toSet have u_not_in_W' : u ∉ W'.support := ((Walk.cons_isPath_iff adj W').mp W_is_path).right have u_not_in_W'_tail : u ∉ W'.support.tail := by intro wrong have u_in_W' := List.Mem.tail w wrong rw [←(Walk.support_eq_cons W')] at u_in_W' contradiction have hu : u ∈ (N \ C) := by simp [N, C] exact ⟨G.adj_symm adj, P_outside_S.left, u_not_in_W'_tail⟩ have card_fact : (C ↓∩ N).toFinset.card = (C ∩ N).toFinset.card := -- TODO the below gives a timeout error -- preimage_val_card sorry have unused_color : ∃ c : Fin k, c ∉ P'_coloring '' (C ↓∩ N) := by suffices (P'_coloring '' (C ↓∩ N)).toFinset.card < (Set.univ : Set (Fin k)).toFinset.card from by have ⟨c, hc⟩ := Finset.exists_mem_not_mem_of_card_lt_card this simp only [Set.mem_toFinset] at hc exact ⟨c, hc.right⟩ simp only [Set.toFinset_image, Set.toFinset_univ, Finset.card_univ, Fintype.card_fin] suffices (C ↓∩ N).toFinset.card < k from calc (Finset.image (⇑P'_coloring) (C ↓∩ N).toFinset).card ≤ (C ↓∩ N).toFinset.card := Finset.card_image_le _ < k := this have ineq1 : (C ↓∩ N).toFinset.card + (N \ C).toFinset.card ≤ k := calc (C ↓∩ N).toFinset.card + (N \ C).toFinset.card = (N ∩ C).toFinset.card + (N \ C).toFinset.card := by simp only [card_fact, Set.inter_comm] _ = N.toFinset.card := by simp only [Set.toFinset_inter, Set.toFinset_diff, Finset.card_inter_add_card_sdiff] _ ≤ G.maxDegree := G.degree_le_maxDegree w _ ≤ k := maxDeg_le_k have ineq2 : 1 ≤ (N \ C).toFinset.card := by simp only [Finset.one_le_card, Set.toFinset_nonempty] exact ⟨u, hu⟩ linarith let ⟨c, hc⟩ := unused_color have extended_coloring := extend_coloring G (S ∪ W'.support.tail.toSet) P'_coloring w c hc have fact : (W'.support.tail.toSet ∪ {w} : Set V) = W'.support.toSet := by simp [List.toSet, Set.union_def, Or.comm, Walk.mem_support_iff] rw [Set.union_assoc, fact] at extended_coloring exact Nonempty.intro extended_coloring -- lemma trivial_graph_colorable {k : ℕ} (h : Fintype.card V = 0) : Colorable G k := by -- simp [Fintype.card_eq_zero_iff, IsEmpty] at h -- apply Nonempty.intro -- apply Coloring.mk -- case color => exact isEmptyElim -- case valid => -- intro v -- exact isEmptyElim v namespace SimpleGraph theorem maxDegree_mono (G' : Subgraph G) : G'.maxDegree ≤ G.maxDegree := by apply maxDegree_le_of_forall_degree_le intro v calc G'.degree v theorem brooks' (k : ℕ) (k_ge_3 : k ≥ 3) (maxDeg_le_k : G.maxDegree ≤ k) (no_max_clique : CliqueFree G (k + 1)) : Colorable G k := by induction hn : Fintype.card V using Nat.strong_induction_on generalizing V G case h n ih _ => by_cases h : n ≤ k · have n_colorable := G.colorable_of_fintype rw [hn] at n_colorable exact Colorable.mono h n_colorable · by_cases k_reg : G.IsRegularOfDegree k case neg => simp [IsRegularOfDegree] at k_reg have ⟨x, hx⟩ := k_reg let S : Set V := Set.univ \ {x} let G' := G.induce S have S_maxDeg_le_k : G'.maxDegree ≤ k := G. case pos => sorry