feat(Combinatorics): a clique has size at most the chromatic number (leanprover-community#32654)

There already exists a version of this lemma for cliques given by a set, but it's impractical to provide an explicit clique on an explicit graph as a set, rather than an indexed family, especially because computing the size of the set would then involve proving that it is the range of an injective function, even though being a clique already implies being injective!

Application: google-deepmind/formal-conjectures#1369

Also rename `coloringOfIsEmpty` and `colorable_of_isEmpty` to leverage anonymous dot notation, and make more arguments implicit.

From FormalConjectures

Author: YaelDillies

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -199,6 +199,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 symm_adj (f : ι → V) : Std.Symm 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 <| hf.mono fun _ _ ↦ C.valid
+
 /-- Construct a term of `SimpleGraph.Coloring` using a function that
 assigns vertices to colors and a proof that it is as proper coloring.
 
@@ -129,17 +133,17 @@ 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))
 
 /-- The coloring of an empty graph. -/
-def coloringOfIsEmpty [IsEmpty V] : G.Coloring α :=
-  Coloring.mk isEmptyElim fun {v} => isEmptyElim v
+def Coloring.ofIsEmpty [IsEmpty V] : G.Coloring α := .mk isEmptyElim fun {v} => isEmptyElim v
+
+theorem Colorable.of_isEmpty [IsEmpty V] (n : ℕ) : G.Colorable n := ⟨.ofIsEmpty⟩
 
-theorem colorable_of_isEmpty [IsEmpty V] (n : ℕ) : G.Colorable n :=
-  ⟨G.coloringOfIsEmpty⟩
+@[deprecated (since := "2026-01-03")] alias coloringOfIsEmpty := Coloring.ofIsEmpty
+@[deprecated (since := "2026-01-03")] alias colorableOfIsEmpty := Colorable.of_isEmpty
 
 theorem isEmpty_of_colorable_zero (h : G.Colorable 0) : IsEmpty V := by
   constructor
@@ -149,39 +153,57 @@ theorem isEmpty_of_colorable_zero (h : G.Colorable 0) : IsEmpty V := by
 
 @[simp]
 lemma colorable_zero_iff : G.Colorable 0 ↔ IsEmpty V :=
-  ⟨G.isEmpty_of_colorable_zero, fun _ ↦ G.colorable_of_isEmpty 0⟩
+  ⟨isEmpty_of_colorable_zero, fun _ ↦ .of_isEmpty 0⟩
 
 /-- 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) :
-    (G.map f).Colorable n := by
+theorem Colorable.map (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 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_iInf {G : SimpleGraph V} :
-    G.chromaticNumber = ⨅ n : {m | G.Colorable m}, (n : ℕ∞) := by
+variable (G) in
+lemma chromaticNumber_eq_biInf : G.chromaticNumber = ⨅ n ∈ setOf G.Colorable, (n : ℕ∞) := rfl
+
+variable (G) in
+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) :
+lemma Colorable.chromaticNumber_eq_sInf (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 +216,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 +232,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⟩
 
@@ -342,8 +367,7 @@ theorem colorable_of_chromaticNumber_ne_top (h : G.chromaticNumber ≠ ⊤) :
   exact colorable_chromaticNumber hn
 
 theorem chromaticNumber_eq_zero_of_isEmpty [IsEmpty V] : G.chromaticNumber = 0 := by
-  rw [← nonpos_iff_eq_zero, ← Nat.cast_zero, chromaticNumber_le_iff_colorable]
-  apply colorable_of_isEmpty
+  rw [← nonpos_iff_eq_zero, ← Nat.cast_zero, chromaticNumber_le_iff_colorable]; exact .of_isEmpty _
 
 @[deprecated (since := "2025-09-15")]
 alias chromaticNumber_eq_zero_of_isempty := chromaticNumber_eq_zero_of_isEmpty
@@ -502,31 +526,16 @@ theorem CompleteBipartiteGraph.chromaticNumber {V W : Type*} [Nonempty V] [Nonem
 
 /-! ### Cliques -/
 
+theorem IsClique.card_le_of_colorable {s : Finset V} (h : G.IsClique s) (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
+    (C : G.Coloring α) : s.card ≤ Fintype.card α := 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