From 2a6b1403af27c1f3a3c00940219491abdee85388 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Wed, 28 May 2025 16:08:26 +0200
Subject: case 1 done

---
 Brooks.lean | 504 ++++++++++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 422 insertions(+), 82 deletions(-)

(limited to 'Brooks.lean')

diff --git a/Brooks.lean b/Brooks.lean
index 669ecc7..1619387 100644
--- a/Brooks.lean
+++ b/Brooks.lean
@@ -20,41 +20,120 @@ open Classical
 variable
   {α : Type}
   {V : Type} [Fintype V]
-  (G : SimpleGraph V) [DecidableRel G.Adj]
+  {G : SimpleGraph V}
+
+-- API for partial colorings
+
+namespace SimpleGraph.Coloring
+
+  structure Extension {S : Set V} (C : (G.induce S).Coloring α) (T : Set V) where
+    subset : S ⊆ T
+    coloring : (G.induce T).Coloring α
+    compatible : @Set.restrict₂ V (fun _ => α) S T subset coloring = C
+
+  def trivial_extension {S : Set V} (C : (G.induce S).Coloring α) : Extension C S := by
+    apply Extension.mk
+    case subset => exact subset_refl S
+    case coloring => exact C
+    case compatible =>
+      ext x
+      simp only [Set.restrict₂, Subtype.coe_eta]
+
+  def extension_trans
+    {S T U : Set V}
+    (C : (G.induce S).Coloring α)
+    (E : Extension C T)
+    (F : Extension E.coloring U)
+    : Extension C U := by
+    apply Extension.mk
+    case subset => exact subset_trans E.subset F.subset
+    case coloring => exact F.coloring
+    case compatible => simp only [←(Set.restrict₂_comp_restrict₂ E.subset F.subset), Function.comp_apply, F.compatible, E.compatible]
+
+end SimpleGraph.Coloring
+
+namespace SimpleGraph.Path
+
+  def split [dec_eq : DecidableEq V] {u v : V} (p : G.Path u v) (z : V) (hz : z ∈ p.val.support)
+    : Σ p₁ : G.Path u z, Σ' p₂ : G.Path z v, p.val = p₁.val.append p₂.val := by
+    replace ⟨p, hp⟩ := p
+    cases dec_eq z u with
+    | isTrue h =>
+      rw [h]
+      use Path.nil, ⟨p, hp⟩
+      simp only [nil_coe, Walk.nil_append]
+    | isFalse h =>
+      cases p with
+      | nil =>
+        simp only [support_nil, mem_cons, not_mem_nil, or_false] at hz
+        contradiction
+      | @cons u w v adj tl =>
+        simp only [support_cons, mem_cons, h, false_or] at hz
+        obtain ⟨⟨tl₁, htl₁⟩, ⟨tl₂, htl₂⟩, happ⟩ := split ⟨tl, IsPath.of_cons hp⟩ z hz
+        simp only at happ
+        simp only [happ, cons_isPath_iff, mem_support_append_iff, not_or] at hp
+        let p₁ := Walk.cons adj tl₁
+        have hp₁ : IsPath p₁ := IsPath.cons htl₁ hp.right.left
+        use ⟨p₁, hp₁⟩, ⟨tl₂, htl₂⟩
+        simp only [Walk.cons_append, p₁, happ]
+
+end SimpleGraph.Path
 
 noncomputable def extend_coloring
-  (S : Set V) (S_coloring : Coloring (G.induce S) α)
+  (S : Set V) (C : Coloring (G.induce S) α)
   (v : V) (c : α)
-  (h : c ∉ S_coloring '' (S ↓∩ G.neighborSet v))
-  : Coloring (G.induce (S ∪ {v})) α
+  (h : c ∉ C '' (S ↓∩ G.neighborSet v))
+  : Coloring.Extension C (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]
+    apply Coloring.Extension.mk
+    case subset => exact Set.subset_union_left
+    case coloring =>
+      apply Coloring.mk
+      case color =>
+        intro ⟨x, _⟩
+        by_cases hx : x ∈ S
+        · exact C ⟨x, hx⟩
+        · exact c
+      case valid =>
+        simp only [Set.mem_image, Set.mem_preimage, mem_neighborSet, Subtype.exists,
+          exists_and_left, not_exists, not_and] at h
+        rintro ⟨x, hx⟩ ⟨y, hy⟩ adj
+        by_cases hxS : x ∈ S <;> by_cases hyS : y ∈ S
+        · simp only [hxS, hyS]
+          exact C.valid adj
+        · simp only [hxS, hyS]
+          replace hyS : y = v := hy.resolve_left hyS
+          simp only [hyS, comap_adj, Function.Embedding.subtype_apply] at adj
+          exact h x (G.adj_symm adj) hxS
+        · simp only [hxS, hyS]
+          replace hxS : x = v := hx.resolve_left hxS
+          simp only [hxS] at adj
+          intro wrong
+          exact h y adj hyS (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]
+
+    case compatible =>
+      ext ⟨x, hx⟩
+      simp only [Coloring.mk, Set.restrict₂_def, RelHom.instFunLike]
+      simp only [hx, ↓reduceDIte, RelHom.coe_fn_toFun]
+
+noncomputable def extend_coloring_of_image_card
+  {k : ℕ}
+  (S : Set V) (C : Coloring (G.induce S) (Fin k))
+  (v : V) (h : (C '' (S ↓∩ G.neighborSet v)).toFinset.card < k)
+  : Coloring.Extension C (S ∪ {v}) := by
+  let N := G.neighborSet v
+
+  have unused_color : ∃ c : Fin k, c ∉ C '' (S ↓∩ N) := by
+    suffices (C '' (S ↓∩ 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_univ, Finset.card_univ, Fintype.card_fin]
+    exact h
+  exact extend_coloring S C v (Exists.choose unused_color) (Exists.choose_spec unused_color)
 
 lemma preimage_val_card (A B : Set V) : (A ↓∩ B).toFinset.card = (A ∩ B).toFinset.card := by
   apply Finset.card_bij'
@@ -78,12 +157,11 @@ lemma preimage_val_card (A B : Set V) : (A ↓∩ B).toFinset.card = (A ∩ B).t
     intro a ha
     simp_all only [not_false_eq_true, true_and]
 
-lemma extend_coloring'
+noncomputable def extend_coloring_of_lt_colored_neighbors
   {k : ℕ}
-  (S : Set V) (S_colorable : Colorable (G.induce S) k)
+  (S : Set V) (C : Coloring (G.induce S) (Fin k))
   (v : V) (h : (G.neighborSet v ∩ S).toFinset.card < k)
-  : Colorable (G.induce (S ∪ {v})) k := by
-  have S_coloring := S_colorable.some
+  : Coloring.Extension C (S ∪ {v}) := by
   let N := G.neighborSet v
 
   have card_fact : (S ↓∩ N).toFinset.card = (S ∩ N).toFinset.card := by
@@ -91,28 +169,23 @@ lemma extend_coloring'
     have foo := preimage_val_card S N
     convert foo
 
-  have unused_color : ∃ c : Fin k, c ∉ S_coloring '' (S ↓∩ N) := by
-    suffices (S_coloring '' (S ↓∩ 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⟩
+  replace h : (C '' (S ↓∩ G.neighborSet v)).toFinset.card < k := by
     simp only [Set.toFinset_image, Set.toFinset_univ, Finset.card_univ, Fintype.card_fin]
     calc
-      (Finset.image (⇑S_coloring) (S ↓∩ N).toFinset).card ≤ (S ↓∩ N).toFinset.card := Finset.card_image_le
+      (Finset.image C (S ↓∩ N).toFinset).card ≤ (S ↓∩ N).toFinset.card := Finset.card_image_le
       _ = (S ∩ N).toFinset.card := card_fact
       _ = (N ∩ S).toFinset.card := by simp only [Set.inter_comm]
       _ < k := h
-  have ⟨c, hc⟩ := unused_color
-  exact Nonempty.intro (extend_coloring G S S_coloring v c hc)
 
-lemma extend_coloring''
+  exact extend_coloring_of_image_card S C v h
+
+noncomputable def extend_coloring_of_degree_lt
   {k : ℕ}
-  (S : Set V) (S_colorable : Colorable (G.induce S) k)
+  (S : Set V) (C : Coloring (G.induce S) (Fin k))
   (v : V) (h : G.degree v < k)
-  : Colorable (G.induce (S ∪ {v})) k := by
-  apply extend_coloring'
-  · assumption
-  · calc
+  : Coloring.Extension C (S ∪ {v}) := by
+  apply extend_coloring_of_lt_colored_neighbors
+  calc
     (G.neighborSet v ∩ S).toFinset.card ≤ (G.neighborSet v).toFinset.card := by
       simp only [Set.toFinset_inter]
       apply Finset.card_le_card
@@ -120,28 +193,63 @@ lemma extend_coloring''
     _ = G.degree v := by simp only [Set.toFinset_card, G.card_neighborSet_eq_degree]
     _ < k := h
 
-theorem color_path
+noncomputable def extend_coloring_of_two_neighbors_eq_color
+  {k : ℕ}
+  (S : Set V) (C : Coloring (G.induce S) (Fin k))
+  (v : V) (hv : G.degree v ≤ k)
+  (x y : S) (hx : G.Adj v x) (hy : G.Adj v y) (x_ne_y : x ≠ y)
+  (hC : C x = C y)
+  : Coloring.Extension C (S ∪ {v}) := by
+  let N := G.neighborSet v
+  apply extend_coloring_of_image_card
+  simp only [Set.toFinset_image, Set.toFinset_univ, Finset.card_univ, Fintype.card_fin]
+
+  have card_fact : (S ↓∩ N).toFinset.card = (S ∩ N).toFinset.card := by
+    -- without "convert" this gives a timeout error
+    have foo := preimage_val_card S N
+    convert foo
+
+  have S_inter_N_card_le_k : (S ↓∩ N).toFinset.card ≤ k := calc
+    (S ↓∩ N).toFinset.card = (S ∩ N).toFinset.card := card_fact
+    _ ≤ N.toFinset.card := Finset.card_le_card (Set.toFinset_subset_toFinset.mpr Set.inter_subset_right)
+    _ ≤ k := hv
+
+  apply Ne.lt_of_le
+  · intro hk
+    have k_le_S_inter_N_card : k ≤ (S ↓∩ N).toFinset.card := calc
+      k = (Finset.image C (S ↓∩ N).toFinset).card := hk.symm
+      _ ≤ (S ↓∩ N).toFinset.card := Finset.card_image_le
+    have k_eq_S_inter_N_card := Nat.le_antisymm k_le_S_inter_N_card S_inter_N_card_le_k
+    simp only [k_eq_S_inter_N_card] at hk
+    have C_inj_on_S_inter_N := Finset.card_image_iff.mp hk
+    simp only [Set.coe_toFinset] at C_inj_on_S_inter_N
+    have x_eq_y := C_inj_on_S_inter_N hx hy hC
+    contradiction
+  · calc
+      (Finset.image C (S ↓∩ N).toFinset).card ≤ (S ↓∩ N).toFinset.card := Finset.card_image_le
+      _ ≤ k := S_inter_N_card_le_k
+
+noncomputable def 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.toFinset)) k := by
-  classical
+    (S_coloring : Coloring (G.induce S) (Fin k))
+    : Coloring.Extension S_coloring (S ∪ P.val.support.tail.toFinset) := by
   let ⟨W, W_is_path⟩ := P
   cases W with
   | nil =>
-    simp
-    rw [Finset.coe_empty, Set.union_empty]
-    exact S_colorable
+    simp only [support_nil, List.tail_cons, toFinset_nil, Finset.coe_empty, Set.union_empty]
+    exact Coloring.trivial_extension S_coloring
   | @cons u w v adj W' =>
-    simp at *
+    simp only [support_cons, mem_cons, forall_eq_or_imp] at P_outside_S
+
     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
+    have T_ext := color_path k maxDeg_le_k P' S (P_outside_S.right) S_coloring
 
     let N := G.neighborSet w
     -- set of vertices already colored by P'_coloring
-    let C := S ∪ W'.support.tail.toFinset
+    let T := S ∪ W'.support.tail.toFinset
 
     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
@@ -149,22 +257,22 @@ theorem color_path
       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]
+    have hu : u ∈ (N \ T) := by
+      simp [N, T]
       exact ⟨G.adj_symm adj, P_outside_S.left, u_not_in_W'_tail⟩
 
-    have h : (N ∩ C).toFinset.card < k := by
-      have ineq1 : (N ∩ C).toFinset.card + (N \ C).toFinset.card ≤ k := calc
+    have h : (N ∩ T).toFinset.card < k := by
+      have ineq1 : (N ∩ T).toFinset.card + (N \ T).toFinset.card ≤ k := calc
         _ = 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
+      have ineq2 : 1 ≤ (N \ T).toFinset.card := by
         simp only [Finset.one_le_card, Set.toFinset_nonempty]
         exact ⟨u, hu⟩
       linarith
 
     have extended_coloring := by
-      apply extend_coloring' G C P'_colorable w
+      apply extend_coloring_of_lt_colored_neighbors T T_ext.coloring w
       -- TODO without "convert" this gives a timeout error
       convert h
 
@@ -172,7 +280,7 @@ theorem color_path
       simp only [coe_toFinset, Set.union_def, Set.mem_setOf_eq, Set.mem_singleton_iff, Or.comm, mem_support_iff]
 
     rw [Set.union_assoc, fact] at extended_coloring
-    exact extended_coloring
+    exact Coloring.extension_trans S_coloring T_ext extended_coloring
 
 lemma induce_maxDegree_mono (S : Set V) : (G.induce S).maxDegree ≤ G.maxDegree := by
   simp only [G.induce_eq_coe_induce_top S]
@@ -184,7 +292,7 @@ lemma induce_maxDegree_mono (S : Set V) : (G.induce S).maxDegree ≤ G.maxDegree
     _ ≤ G.maxDegree := G.degree_le_maxDegree v
 
 noncomputable def extend_path_maximally {u v : V} (P : G.Path u v)
-  : ∃ w : V, ∃ Q : G.Walk w u, IsPath (Walk.append Q P.1) ∧ G.neighborFinset w ⊆ (Walk.append Q P.1).support.toFinset := by
+  : ∃ w : V, ∃ Q : G.Walk w u, IsPath (Q.append P.1) ∧ G.neighborFinset w ⊆ (Q.append P.1).support.toFinset := by
   replace ⟨P, hP⟩ := P
   induction hn : Fintype.card V - P.support.length generalizing u P
 
@@ -222,46 +330,44 @@ noncomputable def extend_path_maximally {u v : V} (P : G.Path u v)
       simp only [P'] at hQ'
       assumption
 
-
 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
+  case h n ih _ =>
+    by_cases hnk : n ≤ k
     · have n_colorable := G.colorable_of_fintype
       rw [hn] at n_colorable
-      exact Colorable.mono h n_colorable
+      exact Colorable.mono hnk n_colorable
     · by_cases k_reg : G.IsRegularOfDegree k
       -- Assume G is not k-regular.
       case neg =>
         simp [IsRegularOfDegree] at k_reg
+        -- x is a vertex of degree strictly less than k
         have ⟨x, hx⟩ := k_reg
         let S : Set V := Set.univ \ {x}
         let G' := G.induce S
 
-        -- Apply induction
-        have S_maxDeg_le_k : G'.maxDegree ≤ k := sorry -- induce_maxDegree_mono G S
+        -- Color every vertex except x by induction
+        have S_maxDeg_le_k : G'.maxDegree ≤ k := sorry -- Nat.le_trans (induce_maxDegree_mono S) maxDeg_le_k
         have S_no_max_clique : G'.CliqueFree (k + 1) := CliqueFree.comap (Embedding.induce S) no_max_clique
         have S_card : Fintype.card (↑S) = n - 1 := by
           simp only [S, ←Set.toFinset_card, Set.toFinset_diff, Set.toFinset_univ, Set.toFinset_singleton]
           have fact := Finset.card_inter_add_card_sdiff Finset.univ {x}
           simp [hn] at fact
           omega
-        have fact : n - 1 < n := by omega
-        have S_colorable : (G.induce S).Colorable k := ih (n - 1) fact (G.induce S) S_maxDeg_le_k S_no_max_clique S_card
+        have S_colorable : (G.induce S).Colorable k := ih (n - 1) (by omega) S_maxDeg_le_k S_no_max_clique S_card
 
-        replace hx : G.degree x < k := by
-          have hx' : G.degree x ≤ k := Nat.le_trans (G.degree_le_maxDegree x) maxDeg_le_k
-          omega
+        replace hx : G.degree x < k := Ne.lt_of_le hx (Nat.le_trans (G.degree_le_maxDegree x) maxDeg_le_k)
 
-        have G_colorable := extend_coloring'' G S S_colorable x hx
+        -- We can also color x since it has degree < k
+        have ⟨_, G_colorable, _⟩ := extend_coloring_of_degree_lt S S_colorable.some x hx
         have fact : S ∪ {x} = Set.univ := by simp only [Set.union_singleton,
           Set.insert_diff_singleton, Set.mem_univ, Set.insert_eq_of_mem, S]
         rw [fact] at G_colorable
-        exact Colorable.of_embedding (G.induceUnivIso.symm.toEmbedding) G_colorable
+        exact Colorable.of_embedding (G.induceUnivIso.symm.toEmbedding) (Nonempty.intro G_colorable)
 
       -- Assume G is k-regular.
       case pos =>
@@ -276,6 +382,7 @@ theorem brooks'
         have claim : ∃ x y : V, x ≠ y ∧ G.Adj v x ∧ G.Adj v y ∧ ¬G.Adj x y := by
           by_contra wrong
           apply no_max_clique
+          -- If not, v and its neighbors would form a clique on k+1 vertices.
           case t => exact (G.neighborSet v ∪ {v}).toFinset
           case a =>
             apply IsNClique.mk
@@ -301,6 +408,239 @@ theorem brooks'
                 exact G.adj_symm hx
               · simp at wrong
                 exact wrong x y x_ne_y hx hy
+        have ⟨x, y, x_ne_y, v_adj_x, v_adj_y, x_nadj_y⟩ := claim
+
+        -- P is the path x → v → y
+        let P : G.Walk x y := Walk.cons (G.adj_symm v_adj_x) (Walk.cons v_adj_y nil)
+        have hP : IsPath P := by
+          apply IsPath.cons
+          · simp only [cons_isPath_iff, isPath_iff_eq_nil, support_nil, mem_cons, not_mem_nil,
+            or_false, true_and]
+            by_contra v_eq_y
+            rw [v_eq_y] at v_adj_y
+            exact G.irrefl v_adj_y
+          · simp only [support_cons, support_nil, mem_cons, not_mem_nil, or_false, not_or]
+            apply And.intro
+            · by_contra x_eq_v
+              rw [x_eq_v] at v_adj_x
+              exact G.irrefl v_adj_x
+            · assumption
+
+        -- Extend P maximally to the front by a path Q from w to x
+        have ⟨w, Q, hQP, hw⟩ := extend_path_maximally ⟨P, hP⟩
+        have hQ : IsPath Q := IsPath.of_append_left hQP
+        simp only [isPath_def, Walk.support_append, List.nodup_append] at hQP
+        replace hQP := hQP.right.right
+        simp only at hw
+
+        by_cases h : (Q.append P).support.toFinset = Finset.univ
+
+        -- Case 1: Q.append P visits every vertex of G
+        case pos =>
+          -- Since G is k-regular with k ≥ 3, v has another neighbor z not equal to x or y
+          have existsThirdNeighbor : (G.neighborFinset v \ {x, y}).Nonempty := by
+            apply Finset.card_pos.mp
+            calc
+              (G.neighborFinset v \ {x, y}).card ≥ (G.neighborFinset v).card - Finset.card {x, y} := Finset.le_card_sdiff {x, y} (G.neighborFinset v)
+              _ = k - Finset.card {x, y} := by simp only [card_neighborFinset_eq_degree, k_reg v]
+              _ > 0 := by
+                have fact : Finset.card {x, y} ≤ 2 := Finset.card_le_two
+                omega -- recall that k ≥ 3
+          have ⟨z, hz⟩ := existsThirdNeighbor
+          simp only [Finset.mem_sdiff, mem_neighborFinset, Finset.mem_insert, Finset.mem_singleton,
+            not_or] at hz
+          have ⟨v_adj_z, z_ne_x, z_ne_y⟩ := hz
+
+          -- By definition z is not on P
+          have z_not_on_P : z ∉ P.support := by
+            simp only [P, support_cons, support_nil, mem_cons, z_ne_x, z_ne_y, not_mem_nil, or_self,
+              or_false, false_or]
+            by_contra z_eq_v
+            simp only [z_eq_v, SimpleGraph.irrefl] at v_adj_z
+
+          -- By assumption, z must lie on Q then
+          have z_on_Q : z ∈ Q.support := by
+            have obv : z ∈ Finset.univ := Finset.mem_univ z
+            simp only [←h, mem_toFinset, mem_support_append_iff, z_not_on_P, or_false] at obv
+            assumption
+
+          -- Split the path Q at z
+          obtain ⟨⟨Q₁, hQ₁⟩, ⟨Q₂, hQ₂⟩, happ⟩ := Path.split ⟨Q, hQ⟩ z z_on_Q
+          simp only at happ
+
+          -- Start by giving x and y the same color
+          let C₁ : Coloring (G.induce {x, y}) (Fin k) := by
+            apply Coloring.mk
+            case color =>
+              exact fun _ => Fin.mk 0 (by omega)
+            case valid =>
+              rintro ⟨a, ha⟩ ⟨b, hb⟩ adj _
+              by_cases hab : a = b
+              · simp only [hab] at adj
+                exact G.irrefl adj
+              · simp at ha hb adj
+                cases ha with
+                | inl a_eq_x =>
+                  rw [a_eq_x, Eq.comm] at hab
+                  have b_eq_y := Or.resolve_left hb hab
+                  rw [a_eq_x, b_eq_y] at adj
+                  contradiction
+                | inr a_eq_y =>
+                  rw [a_eq_y, Eq.comm] at hab
+                  have b_eq_x := Or.resolve_right hb hab
+                  rw [a_eq_y, b_eq_x, G.adj_comm] at adj
+                  contradiction
+
+          -- u is the vertex on Q next to x
+          let u := Q₂.penultimate
+          have u_adj_x : G.Adj u x := Walk.adj_penultimate (Walk.not_nil_of_ne z_ne_x)
+
+          -- We will color the paths R₁ and R₂
+          let R₁ : G.Walk z u := Q₂.dropLast
+          let R₂ : G.Walk v w := Walk.cons v_adj_z Q₁.reverse
+
+          have v_not_on_Q : v ∉ Q.support := by
+            have v_on_P_tail : v ∈ P.support.tail := by simp [P]
+            exact List.disjoint_symm hQP v_on_P_tail
+          have v_not_on_Q₁_rev : v ∉ Q₁.reverse.support := by
+            simp [happ] at v_not_on_Q
+            simp only [Walk.support_reverse, List.mem_reverse]
+            exact v_not_on_Q.1
+          have v_not_on_Q₂ : v ∉ Q₂.support := by
+            simp [happ] at v_not_on_Q
+            exact v_not_on_Q.2
+
+          have hR₁ : IsPath R₁ := by
+            have obv : R₁.concat u_adj_x = Q₂ := by simp only [concat_dropLast, R₁]
+            simp [←obv, Walk.concat_eq_append] at hQ₂
+            exact IsPath.of_append_left hQ₂
+          have hR₂ : IsPath R₂ := IsPath.cons ((isPath_reverse_iff Q₁).mpr hQ₁) v_not_on_Q₁_rev
+
+          have R₁_support : Q₂.support = R₁.support.concat x := by
+            rw [←(Walk.support_concat R₁ u_adj_x)]
+            simp only [concat_dropLast, R₁]
+
+          have x_not_on_R₁ : x ∉ R₁.support := by
+            simp [isPath_def, R₁_support] at hQ₂
+            simpa using List.disjoint_of_nodup_append hQ₂
+
+          have Q₁_disj_Q₂_tail : Q₁.support.Disjoint Q₂.support.tail := by
+            simp [isPath_def, happ, Walk.support_append] at hQ
+            exact List.disjoint_of_nodup_append hQ
+
+          have x_not_on_Q₁ : x ∉ Q₁.support := by
+            have Q₂_not_nil : ¬Q₂.Nil := Walk.not_nil_of_ne z_ne_x
+            exact Q₁_disj_Q₂_tail.symm (Walk.end_mem_tail_support Q₂_not_nil)
+
+          have y_not_on_Q : y ∉ Q.support := by
+            have y_on_P_tail : y ∈ P.support.tail := by simp [P]
+            exact List.disjoint_symm hQP y_on_P_tail
+
+          simp only [happ, mem_support_append_iff, not_or] at y_not_on_Q
+          have ⟨y_not_on_Q₁, y_not_on_Q₂⟩ := y_not_on_Q
+
+          have y_not_on_R₁ : y ∉ R₁.support := by
+            simp only [R₁_support, List.concat_eq_append, mem_append, mem_cons, not_mem_nil,
+              or_false, not_or] at y_not_on_Q₂
+            exact y_not_on_Q₂.left
+
+          have v_not_on_R₁ : v ∉ R₁.support := by
+            simp only [R₁_support, List.concat_eq_append, mem_append, mem_cons, not_mem_nil,
+              or_false, not_or] at v_not_on_Q₂
+            exact v_not_on_Q₂.left
+
+          have xy_not_on_R₁ : ∀ t ∈ R₁.support, t ∉ ({x, y} : Set V) := by
+            intro t ht
+            simp only [Set.mem_insert_iff, Set.mem_singleton_iff, not_or]
+            apply And.intro
+            · intro hx
+              rw [hx] at ht
+              contradiction
+            · intro hy
+              rw [hy] at ht
+              contradiction
+
+          -- Color the path R₁.
+          let C₂ := color_path k maxDeg_le_k ⟨R₁, hR₁⟩ {x, y} xy_not_on_R₁ C₁
+          simp only at C₂
+
+          have R₂_not_colored_by_C₂ : ∀ t ∈ R₂.support, t ∉ (({x, y} : Set V) ∪ R₁.support.tail.toFinset) := by
+            intro t ht
+            simp only [support_cons, support_reverse, mem_cons, mem_reverse, R₂] at ht
+
+            simp only [coe_toFinset, Set.mem_union, Set.mem_insert_iff, Set.mem_singleton_iff,
+              Set.mem_setOf_eq, not_or]
+
+            cases ht with
+            | inl t_eq_v =>
+              rw [t_eq_v]
+              use ⟨G.ne_of_adj v_adj_x, G.ne_of_adj v_adj_y⟩
+              intro hv
+              exact v_not_on_R₁ (List.mem_of_mem_tail hv)
+            | inr t_on_Q₁ =>
+              constructor
+              · constructor
+                · intro hx
+                  rw [hx] at t_on_Q₁
+                  contradiction
+                · intro hy
+                  rw [hy] at t_on_Q₁
+                  contradiction
+              · intro ht
+                have t_not_on_Q₂_tail := Q₁_disj_Q₂_tail t_on_Q₁
+                simp only [R₁_support, List.concat_eq_append, ne_eq, support_ne_nil,
+                  not_false_eq_true, tail_append_of_ne_nil, mem_append, mem_cons, not_mem_nil,
+                  or_false, imp_false, not_or] at t_not_on_Q₂_tail
+                exact t_not_on_Q₂_tail.left ht
+
+          -- Now color the path R₂.
+          let C₃ := color_path k maxDeg_le_k ⟨R₂, hR₂⟩ ({x, y} ∪ R₁.support.tail.toFinset) R₂_not_colored_by_C₂ C₂.coloring
+          replace C₃ := Coloring.extension_trans C₁ C₂ C₃
+          simp only at C₃
+
+          -- C₃ colors the set S, which contains every vertex of G except v.
+          -- We can also color v because v has two neighbors of the same color
+          -- (namely x and y).
+          let S : Set V := {x, y} ∪ R₁.support.tail.toFinset ∪ R₂.support.tail.toFinset
+          have x_in_xy : x ∈ ({x, y} : Set V) := by simp only [Set.mem_insert_iff, Set.mem_singleton_iff, true_or]
+          have y_in_xy : y ∈ ({x, y} : Set V) := by simp only [Set.mem_insert_iff, Set.mem_singleton_iff, or_true]
+          have x_in_S : x ∈ S := by simp only [S, x_in_xy, Set.mem_union, true_or]
+          have y_in_S : y ∈ S := by simp only [S, y_in_xy, Set.mem_union, true_or]
+          have x_ne_y : (⟨x, x_in_S⟩ : S) ≠ ⟨y, y_in_S⟩ := by
+            intro wrong
+            simp only [Subtype.mk.injEq] at wrong
+            contradiction
+          have x_y_same_color : C₃.coloring ⟨x, x_in_S⟩ = C₃.coloring ⟨y, y_in_S⟩ := by
+            calc
+              C₃.coloring ⟨x, x_in_S⟩ = C₁ ⟨x, x_in_xy⟩ := by simp only [←C₃.compatible, Set.restrict₂]
+              _ = C₁ ⟨y, y_in_xy⟩ := rfl
+              _ = C₃.coloring ⟨y, y_in_S⟩ := by simp only [←C₃.compatible, Set.restrict₂]
+
+          have deg_v_le_k := Nat.le_trans (G.degree_le_maxDegree v) maxDeg_le_k
+          let C₄ := extend_coloring_of_two_neighbors_eq_color S C₃.coloring v deg_v_le_k ⟨x, x_in_S⟩ ⟨y, y_in_S⟩ v_adj_x v_adj_y x_ne_y x_y_same_color
+
+          -- Now we just need to check that the union of all these paths is indeed all of V.
+          have C₄_colors_G : S ∪ {v} = Set.univ := by
+            rw [Set.union_comm]
+            apply Set.toFinset_inj.mp
+            simp only [S, Set.toFinset_univ, Set.toFinset_union, Finset.toFinset_coe, Set.toFinset_singleton, Set.toFinset_insert]
+            simp only [Finset.insert_union, support_cons, support_reverse, List.tail_cons,
+              toFinset_reverse, Finset.union_assoc, Finset.union_insert, R₂]
+            simp only [happ, support_append, R₁_support, List.concat_eq_append, ne_eq,
+              support_ne_nil, not_false_eq_true, tail_append_of_ne_nil, support_cons, support_nil,
+              List.tail_cons, List.append_assoc, List.cons_append, List.nil_append, toFinset_append,
+              toFinset_cons, toFinset_nil, insert_emptyc_eq, Finset.union_insert, P] at h
+            rw [←h]
+            congr
+            rw [←Finset.insert_eq]
+            congr 1
+            rw [←Finset.union_assoc, Finset.union_comm]
+            conv =>
+              lhs
+              arg 2
+              rw [Finset.union_comm]
+
+          rw [C₄_colors_G] at C₄
+          exact Colorable.of_embedding G.induceUnivIso.symm.toEmbedding (Nonempty.intro C₄.coloring)
 
-        have ⟨x, y, x_ne_y, hx, hy, x_nadj_y⟩ := claim
-        sorry
+        case neg => sorry
-- 
cgit v1.2.3

