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