feat(Combinatorics): a clique has size at most the chromatic number

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -195,6 +195,8 @@ theorem adj_congr_of_sym2 {u v w x : V} (h : s(u, v) = s(w, x)) : G.Adj u v ↔
   · rw [hl.1, hl.2]
   · rw [hr.1, hr.2, adj_comm]
 
+instance isSymm_adj (f : ι → V) : IsSymm ι fun i j ↦ G.Adj (f i) (f j) where symm _ _ := .symm
+
 section Order
 
 /-- The relation that one `SimpleGraph` is a subgraph of another.

Mathlib/Combinatorics/SimpleGraph/Coloring.lean

@@ -74,11 +74,15 @@ This is also known as a proper coloring.
 abbrev Coloring (α : Type v) := G →g completeGraph α
 
 variable {G}
-variable {α β : Type*} (C : G.Coloring α)
+variable {ι α β : Type*} (C : G.Coloring α)
 
 theorem Coloring.valid {v w : V} (h : G.Adj v w) : C v ≠ C w :=
   C.map_rel h
 
+lemma Coloring.injective_comp_of_pairwise_adj (C : G.Coloring α) (f : ι → V)
+    (hf : Pairwise fun i j ↦ G.Adj (f i) (f j)) : (C ∘ f).Injective :=
+  Function.injective_iff_pairwise_ne.2 fun _i _j hij ↦ C.valid <| hf hij
+
 /-- Construct a term of `SimpleGraph.Coloring` using a function that
 assigns vertices to colors and a proof that it is as proper coloring.
 
@@ -129,11 +133,11 @@ instance [DecidableEq α] {c : α} :
     DecidablePred (· ∈ C.colorClass c) :=
   inferInstanceAs <| DecidablePred (· ∈ { v | C v = c })
 
-variable (G)
-
+variable (G) in
 /-- Whether a graph can be colored by at most `n` colors. -/
 def Colorable (n : ℕ) : Prop := Nonempty (G.Coloring (Fin n))
 
+variable (G) in
 /-- The coloring of an empty graph. -/
 def coloringOfIsEmpty [IsEmpty V] : G.Coloring α :=
   Coloring.mk isEmptyElim fun {v} => isEmptyElim v
@@ -153,35 +157,52 @@ lemma colorable_zero_iff : G.Colorable 0 ↔ IsEmpty V :=
 
 /-- If `G` is `n`-colorable, then mapping the vertices of `G` produces an `n`-colorable simple
 graph. -/
-theorem Colorable.map {β : Type*} (f : V ↪ β) [NeZero n] {G : SimpleGraph V} (hc : G.Colorable n) :
+theorem Colorable.map {β : Type*} (f : V ↪ β) [NeZero n] (hc : G.Colorable n) :
     (G.map f).Colorable n := by
   obtain ⟨C⟩ := hc
   use extend f C (const β default)
   intro a b ⟨_, _, hadj, ha, hb⟩
   rw [← ha, f.injective.extend_apply, ← hb, f.injective.extend_apply]
   exact C.valid hadj
 
+lemma Colorable.card_le_of_pairwise_adj (hG : G.Colorable n) (f : ι → V)
+    (hf : Pairwise fun i j ↦ G.Adj (f i) (f j)) : Nat.card ι ≤ n := by
+  obtain ⟨C⟩ := hG
+  simpa using Nat.card_le_card_of_injective _ (C.injective_comp_of_pairwise_adj f hf)
+
+variable (G) in
 /-- The "tautological" coloring of a graph, using the vertices of the graph as colors. -/
 def selfColoring : G.Coloring V := Coloring.mk id fun {_ _} => G.ne_of_adj
 
+variable (G) in
 /-- The chromatic number of a graph is the minimal number of colors needed to color it.
 This is `⊤` (infinity) iff `G` isn't colorable with finitely many colors.
 
 If `G` is colorable, then `ENat.toNat G.chromaticNumber` is the `ℕ`-valued chromatic number. -/
 noncomputable def chromaticNumber : ℕ∞ := ⨅ n ∈ setOf G.Colorable, (n : ℕ∞)
 
-lemma chromaticNumber_eq_biInf {G : SimpleGraph V} :
-    G.chromaticNumber = ⨅ n ∈ setOf G.Colorable, (n : ℕ∞) := rfl
+lemma le_chromaticNumber_iff_colorable : n ≤ G.chromaticNumber ↔ ∀ m, G.Colorable m → n ≤ m := by
+  simp [chromaticNumber]
+
+lemma le_chromaticNumber_iff_coloring :
+    n ≤ G.chromaticNumber ↔ ∀ m, G.Coloring (Fin m) → n ≤ m := by
+  simp [le_chromaticNumber_iff_colorable, Colorable]
 
-lemma chromaticNumber_eq_iInf {G : SimpleGraph V} :
-    G.chromaticNumber = ⨅ n : {m | G.Colorable m}, (n : ℕ∞) := by
+lemma le_chromaticNumber_of_pairwise_adj (hn : n ≤ Nat.card ι) (f : ι → V)
+    (hf : Pairwise fun i j ↦ G.Adj (f i) (f j)) : n ≤ G.chromaticNumber :=
+  le_chromaticNumber_iff_colorable.2 fun _m hm ↦ hn.trans <| hm.card_le_of_pairwise_adj f hf
+
+lemma chromaticNumber_eq_biInf : G.chromaticNumber = ⨅ n ∈ setOf G.Colorable, (n : ℕ∞) := rfl
+
+lemma chromaticNumber_eq_iInf : G.chromaticNumber = ⨅ n : {m | G.Colorable m}, (n : ℕ∞) := by
   rw [chromaticNumber, iInf_subtype]
 
 lemma Colorable.chromaticNumber_eq_sInf {G : SimpleGraph V} {n} (h : G.Colorable n) :
     G.chromaticNumber = sInf {n' : ℕ | G.Colorable n'} := by
   rw [ENat.coe_sInf, chromaticNumber]
   exact ⟨_, h⟩
 
+variable (G) in
 /-- Given an embedding, there is an induced embedding of colorings. -/
 def recolorOfEmbedding {α β : Type*} (f : α ↪ β) : G.Coloring α ↪ G.Coloring β where
   toFun C := (Embedding.completeGraph f).toHom.comp C
@@ -194,9 +215,11 @@ def recolorOfEmbedding {α β : Type*} (f : α ↪ β) : G.Coloring α ↪ G.Col
     rw [h]
     rfl
 
+variable (G) in
 @[simp] lemma coe_recolorOfEmbedding (f : α ↪ β) :
     ⇑(G.recolorOfEmbedding f) = (Embedding.completeGraph f).toHom.comp := rfl
 
+variable (G) in
 /-- Given an equivalence, there is an induced equivalence between colorings. -/
 def recolorOfEquiv {α β : Type*} (f : α ≃ β) : G.Coloring α ≃ G.Coloring β where
   toFun := G.recolorOfEmbedding f.toEmbedding
@@ -208,21 +231,22 @@ def recolorOfEquiv {α β : Type*} (f : α ≃ β) : G.Coloring α ≃ G.Colorin
     ext v
     apply Equiv.apply_symm_apply
 
+variable (G) in
 @[simp] lemma coe_recolorOfEquiv (f : α ≃ β) :
     ⇑(G.recolorOfEquiv f) = (Embedding.completeGraph f).toHom.comp := rfl
 
+variable (G) in
 /-- There is a noncomputable embedding of `α`-colorings to `β`-colorings if
 `β` has at least as large a cardinality as `α`. -/
 noncomputable def recolorOfCardLE {α β : Type*} [Fintype α] [Fintype β]
     (hn : Fintype.card α ≤ Fintype.card β) : G.Coloring α ↪ G.Coloring β :=
   G.recolorOfEmbedding <| (Function.Embedding.nonempty_of_card_le hn).some
 
+variable (G) in
 @[simp] lemma coe_recolorOfCardLE [Fintype α] [Fintype β] (hαβ : card α ≤ card β) :
     ⇑(G.recolorOfCardLE hαβ) =
       (Embedding.completeGraph (Embedding.nonempty_of_card_le hαβ).some).toHom.comp := rfl
 
-variable {G}
-
 theorem Colorable.mono {n m : ℕ} (h : n ≤ m) (hc : G.Colorable n) : G.Colorable m :=
   ⟨G.recolorOfCardLE (by simp [h]) hc.some⟩
 
@@ -502,31 +526,17 @@ theorem CompleteBipartiteGraph.chromaticNumber {V W : Type*} [Nonempty V] [Nonem
 
 /-! ### Cliques -/
 
+theorem IsClique.card_le_of_colorable {s : Finset V} (h : G.IsClique s) {n : ℕ}
+    (hc : G.Colorable n) : s.card ≤ n := by
+  simpa using hc.card_le_of_pairwise_adj (Subtype.val : s → V) <| by simpa [Pairwise] using h
 
 theorem IsClique.card_le_of_coloring {s : Finset V} (h : G.IsClique s) [Fintype α]
     (C : G.Coloring α) : s.card ≤ Fintype.card α := by
-  rw [isClique_iff_induce_eq] at h
-  have f : G.induce ↑s ↪g G := Embedding.comap (Function.Embedding.subtype fun x => x ∈ ↑s) G
-  rw [h] at f
-  convert Fintype.card_le_of_injective _ (C.comp f.toHom).injective_of_top_hom using 1
-  simp
-
-theorem IsClique.card_le_of_colorable {s : Finset V} (h : G.IsClique s) {n : ℕ}
-    (hc : G.Colorable n) : s.card ≤ n := by
-  convert h.card_le_of_coloring hc.some
-  simp
+  simpa using h.card_le_of_colorable C.colorable
 
 theorem IsClique.card_le_chromaticNumber {s : Finset V} (h : G.IsClique s) :
-    s.card ≤ G.chromaticNumber := by
-  obtain (hc | hc) := eq_or_ne G.chromaticNumber ⊤
-  · rw [hc]
-    exact le_top
-  · have hc' := hc
-    rw [chromaticNumber_ne_top_iff_exists] at hc'
-    obtain ⟨n, c⟩ := hc'
-    rw [← ENat.coe_toNat_eq_self] at hc
-    rw [← hc, Nat.cast_le]
-    exact h.card_le_of_colorable (colorable_chromaticNumber c)
+    s.card ≤ G.chromaticNumber :=
+  le_chromaticNumber_of_pairwise_adj (by simp) (Subtype.val : s → V) <| by simpa [Pairwise] using h
 
 protected theorem Colorable.cliqueFree {n m : ℕ} (hc : G.Colorable n) (hm : n < m) :
     G.CliqueFree m := by