English
In any IsFiveWheelLike structure, w2 is not in s.
Русский
В любой структуре IsFiveWheelLike w2 не принадлежит s.
LaTeX
$$$$ w_2 \\notin s. $$$$
Lean4
/-- Any graph containing an `IsFiveWheelLike r k` structure is not `(r + 1)`-colorable.
-/
theorem not_colorable_succ : ¬G.Colorable (r + 1) := by
intro ⟨C⟩
have h := C.surjOn_of_card_le_isClique hw.isNClique_fst_left.1 (by simp [hw.isNClique_fst_left.2])
have :=
C.surjOn_of_card_le_isClique hw.isNClique_snd_right.1
(by simp [hw.isNClique_snd_right.2])
-- Since `C` is an `r + 1`-coloring and `insert w₁ s` is an `r + 1`-clique, it contains a vertex
-- `x` which shares its colour with `v`
obtain ⟨x, hx, hcx⟩ := h (a := C v) trivial
obtain ⟨y, hy, hcy⟩ := this (a := C v) trivial
rw [coe_insert] at *
-- However since `insert v s` and `insert v t` are cliques, we must have `x = w₁` and `y = w₂`.
cases hx with
| inl hx =>
cases hy with
| inl hy =>
-- But this is a contradiction since `w₁` and `w₂` are adjacent.
subst_vars; exact C.valid hw.isPathGraph3Compl.adj (hcy ▸ hcx)
| inr hy =>
apply (C.valid _ hcy.symm).elim
exact hw.isNClique_right.1 (by simp) (by simp [hy]) fun h ↦ hw.notMem_right (h ▸ hy)
| inr hx =>
apply (C.valid _ hcx.symm).elim
exact hw.isNClique_left.1 (by simp) (by simp [hx]) fun h ↦ hw.notMem_left (h ▸ hx)
