feat: vertex replacement (#6808)

`cliqueFree_of_replaceVertex_cliqueFree` is still quite long.

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -1239,6 +1239,43 @@ theorem DeleteFar.mono (h : G.DeleteFar p r₂) (hr : r₁ ≤ r₂) : G.DeleteF
 
 end DeleteFar
 
+/-! ## Vertex replacement -/
+
+
+section ReplaceVertex
+
+variable [DecidableEq V] (s t : V)
+
+/-- The graph formed by forgetting `t`'s neighbours and instead giving it those of `s`. The `s-t`
+edge is removed if present. -/
+abbrev replaceVertex : SimpleGraph V where
+  Adj v w := if v = t then if w = t then False else G.Adj s w
+                      else if w = t then G.Adj v s else G.Adj v w
+  symm v w := by dsimp only; split_ifs <;> simp [adj_comm]
+
+/-- There is never an `s-t` edge in `G.replaceVertex s t`. -/
+theorem not_adj_replaceVertex_same : ¬(G.replaceVertex s t).Adj s t := by simp
+
+@[simp]
+theorem replaceVertex_self : G.replaceVertex s s = G := by
+  ext; dsimp only; split_ifs <;> simp_all [adj_comm]
+
+/-- Except possibly for `t`, the neighbours of `s` in `G.replaceVertex s t` are its neighbours in
+`G`. -/
+lemma adj_replaceVertex_iff_of_ne_left {w : V} (hw : w ≠ t) :
+    (G.replaceVertex s t).Adj s w ↔ G.Adj s w := by simp [hw]
+
+/-- Except possibly for itself, the neighbours of `t` in `G.replaceVertex s t` are the neighbours of
+`s` in `G`. -/
+lemma adj_replaceVertex_iff_of_ne_right {w : V} (hw : w ≠ t) :
+    (G.replaceVertex s t).Adj t w ↔ G.Adj s w := by simp [hw]
+
+/-- Adjacency in `G.replaceVertex s t` which does not involve `t` is the same as that of `G`. -/
+lemma adj_replaceVertex_iff_of_ne {v w : V} (hv : v ≠ t) (hw : w ≠ t) :
+    (G.replaceVertex s t).Adj v w ↔ G.Adj v w := by simp [hv, hw]
+
+end ReplaceVertex
+
 /-! ## Map and comap -/
 
 

Mathlib/Combinatorics/SimpleGraph/Clique.lean

@@ -237,6 +237,43 @@ theorem cliqueFree_completeMultipartiteGraph {ι : Type*} [Fintype ι] (V : ι 
   rw [← top_adj, ← f.map_adj_iff, comap_Adj, top_adj] at hn
   exact absurd he hn
 
+/-- Clique-freeness is preserved by `replaceVertex`. -/
+theorem cliqueFree_of_replaceVertex_cliqueFree [DecidableEq α] (s t : α) (h : G.CliqueFree n) :
+    (G.replaceVertex s t).CliqueFree n := by
+  contrapose h
+  obtain ⟨⟨f, hi⟩, ha⟩ := topEmbeddingOfNotCliqueFree h
+  simp only [Function.Embedding.coeFn_mk, top_adj, ne_eq] at ha
+  rw [not_cliqueFree_iff]
+  by_cases mt : t ∈ Set.range f
+  · obtain ⟨x, hx⟩ := mt
+    by_cases ms : s ∈ Set.range f
+    · obtain ⟨y, hy⟩ := ms
+      by_cases hst : s = t
+      · simp_all [not_cliqueFree_iff]
+      · replace ha := @ha x y; simp_all
+    · use ⟨fun v => if v = x then s else f v, ?_⟩
+      swap
+      · intro a b
+        dsimp only
+        split_ifs
+        · simp_all
+        · intro; simp_all
+        · intro; simp_all
+        · apply hi
+      intro a b
+      simp only [Function.Embedding.coeFn_mk, top_adj, ne_eq]
+      split_ifs with h1 h2 h2
+      · simp_all
+      · have := (@ha b x).mpr h2
+        split_ifs at this; subst h1; tauto
+      · have := (@ha a x).mpr h1
+        split_ifs at this; subst h2; tauto
+      · rw [← @ha a b]
+        have := (@hi a x).mt h1
+        have := (@hi b x).mt h2
+        simp_all
+  · use ⟨f, hi⟩; simp_all
+
 end CliqueFree
 
 /-! ### Set of cliques -/