path: root/Brooks.lean

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.Card
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}

-- 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) (C : Coloring (G.induce S) α)
  (v : V) (c : α)
  (h : c ∉ C '' (S ↓∩ G.neighborSet v))
  : Coloring.Extension C (S ∪ {v})
  := by
    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'
  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]

noncomputable def extend_coloring_of_lt_colored_neighbors
  {k : ℕ}
  (S : Set V) (C : Coloring (G.induce S) (Fin k))
  (v : V) (h : (G.neighborSet v ∩ S).toFinset.card < k)
  : Coloring.Extension C (S ∪ {v}) := by
  let N := G.neighborSet v

  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

  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 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

  exact extend_coloring_of_image_card S C v h

noncomputable def extend_coloring_of_degree_lt
  {k : ℕ}
  (S : Set V) (C : Coloring (G.induce S) (Fin k))
  (v : V) (h : G.degree v < k)
  : 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
      simp only [Set.subset_toFinset, Finset.coe_inter, Set.coe_toFinset, Set.inter_subset_left]
    _ = G.degree v := by simp only [Set.toFinset_card, G.card_neighborSet_eq_degree]
    _ < k := h

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_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 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 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 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 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
      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 \ T) := by
      simp [N, T]
      exact ⟨G.adj_symm adj, P_outside_S.left, u_not_in_W'_tail⟩

    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 \ T).toFinset.card := by
        simp only [Finset.one_le_card, Set.toFinset_nonempty]
        exact ⟨u, hu⟩
      linarith

    have extended_coloring := by
      apply extend_coloring_of_lt_colored_neighbors T T_ext.coloring w
      -- TODO without "convert" this gives a timeout error
      convert h

    have fact : (W'.support.tail.toFinset ∪ {w} : Set V) = W'.support.toFinset := by
      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 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]
  apply maxDegree_le_of_forall_degree_le
  intro v
  rw [Subgraph.coe_degree]
  calc
    ((⊤ : G.Subgraph).induce S).degree v ≤ G.degree v := Subgraph.degree_le ((⊤ : G.Subgraph).induce S) v
    _ ≤ 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 (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

  case zero =>
    have fact : P.support.toFinset = Finset.univ := by
      apply Finset.eq_univ_of_card
      rw [isPath_def] at hP
      rw [←(List.toFinset_card_of_nodup hP)] at hn
      apply Nat.le_antisymm
      · exact Finset.card_le_univ P.support.toFinset
      · omega
    use u, Walk.nil
    simp only [Walk.nil_append, fact, Finset.coe_univ, Finset.subset_univ, and_true]
    assumption

  case succ n ih =>
    by_cases hu : G.neighborFinset u ⊆ P.support.toFinset
    case pos =>
      use u, Walk.nil
      simp only [Walk.nil_append]
      exact ⟨hP, hu⟩
    case neg =>
      simp [Finset.subset_iff] at hu
      have ⟨x, e, hx⟩ := hu
      replace e : G.Adj x u := G.adj_symm e
      let P' := Walk.cons e P
      have hP' : IsPath P' := IsPath.cons hP hx
      have hn' : Fintype.card V - P'.support.length = n := by
        simp only [P', Walk.support_cons, List.length_cons]
        omega
      have ⟨w, Q', hQ'⟩ := ih P' hP' hn'
      let Q := Walk.concat Q' e
      use w, Q
      simp only [Q, Walk.concat_append]
      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 hnk : n ≤ k
    · have n_colorable := G.colorable_of_fintype
      rw [hn] at 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

        -- 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 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 := Ne.lt_of_le hx (Nat.le_trans (G.degree_le_maxDegree x) maxDeg_le_k)

        -- 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) (Nonempty.intro G_colorable)

      -- Assume G is k-regular.
      case pos =>
        -- Pick any vertex v.
        have V_nonempty : Nonempty V := by
          apply Fintype.card_pos_iff.mp
          omega
        let v := V_nonempty.some

        -- Since G does not contain a clique on k+1 vertices, there exist
        -- two neighbours x, y of v that are not adjacent in G.
        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
            case card_eq =>
              simp only [Set.union_singleton, Set.toFinset_insert, Set.mem_toFinset,
                mem_neighborSet, SimpleGraph.irrefl, not_false_eq_true,
                Finset.card_insert_of_not_mem, Set.toFinset_card, Fintype.card_ofFinset,
                Nat.add_left_inj]
              have fact : ({x | G.Adj v x} : Finset V) = G.neighborFinset v := by
                ext a
                simp only [Finset.mem_filter, Finset.mem_univ, true_and, mem_neighborFinset]
              simp only [fact, card_neighborFinset_eq_degree]
              exact k_reg v
            case isClique =>
              intro x hx y hy x_ne_y
              simp at hx hy
              cases' hx with x_eq_v hx <;> cases' hy with y_eq_v hy
              · rw [x_eq_v, y_eq_v] at x_ne_y
                contradiction
              · rw [←x_eq_v] at hy
                assumption
              · rw [←y_eq_v] at hx
                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)

        case neg => sorry