From 865e2c2f9af4f78e8ea6114c3019e1df0e075c11 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 22 Apr 2026 06:55:57 +0300
Subject: [PATCH 01/13] feat(Combinatorics/SimpleGraph/Coloring/Greedy): greedy
 coloring

---
 .../SimpleGraph/Coloring/Greedy.lean          | 285 ++++++++++++++++++
 .../SimpleGraph/Coloring/VertexColoring.lean  |  40 +++
 Mathlib/Combinatorics/SimpleGraph/Finite.lean |  21 +-
 3 files changed, 344 insertions(+), 2 deletions(-)
 create mode 100644 Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
new file mode 100644
index 00000000000000..029777e484814c
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -0,0 +1,285 @@
+/-
+Copyright (c) 2026 Snir Broshi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Snir Broshi
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
+public import Mathlib.Data.Set.Card
+public import Mathlib.SetTheory.Ordinal.Arithmetic
+
+/-!
+# Greedy Coloring
+-/
+
+@[expose] public section Dependencies
+
+set_option warn.sorry false
+set_option linter.style.longLine false
+
+-- #35619
+theorem SimpleGraph.isClique_top {α : Type*} (s : Set α) : (⊤ : SimpleGraph α).IsClique s := sorry
+-- #35619
+theorem SimpleGraph.isClique_univ_iff {V : Type*} (G : SimpleGraph V) : G.IsClique .univ ↔ G = ⊤ := sorry
+-- #35622
+theorem Function.Injective.isWellOrder_onFun {α β : Type*} (r : β → β → Prop) {f : α → β} (hf : f.Injective) [IsWellOrder β r] : IsWellOrder α (r.onFun f) := sorry
+-- #35628
+theorem SimpleGraph.Embedding.image_neighborSet {V V' : Type*} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G ↪g G'} (v : V) : f '' G.neighborSet v = G'.neighborSet (f v) ∩ Set.range f := sorry
+-- #36626
+theorem IsLowerSet.eqOn_id_of_injOn_of_forall_not_lt {α : Type*} {r : α → α → Prop} [IsWellOrder α r] {s : Set α} (hs : @IsLowerSet α ⟨r⟩ s) {f : α → α} (hf : s.InjOn f) (h : ∀ x ∈ s, ¬r x (f x)) : s.EqOn f id := sorry
+-- #36626
+theorem IsWellOrder.eq_id_of_injective_of_forall_not_lt {α : Type*} {r : α → α → Prop} [IsWellOrder α r] {f : α → α} (hf : f.Injective) (h : ∀ x, ¬r x (f x)) : f = id := sorry
+
+end Dependencies
+
+public section
+
+namespace SimpleGraph
+
+open Cardinal Ordinal
+
+variable {V : Type*} (G : SimpleGraph V) (r : V → V → Prop) [IsWellOrder V r]
+
+/-- A greedy coloring of the graph where the vertices are greedily colored in the order specified
+by the given well-order. The colors are the vertices of the graph, ordered by the same
+well-order. -/
+noncomputable def greedyColoring : G.Coloring V :=
+  let f v ih :=
+    -- The set of possible colors is the complement of the set of colors that are already taken by
+    -- neighbors of `v` that were already colored
+    let s := {(ih u hu).val | (u : V) (hu : r u v) (_ : G.Adj u v)}ᶜ
+    -- This set is not empty since `v` itself is always a possible color
+    have : v ∈ s := fun ⟨u, hu, _, heq⟩ ↦ heq ▸ (ih u hu).prop <| hu
+    -- Color `v` with the minimum possible color, ordered by the well-order
+    ⟨IsWellFounded.wf.min s ⟨v, this⟩, IsWellFounded.wf.not_lt_min s this⟩
+  let toFun v :=
+    -- Recurse to color each vertex, ordered by the well-order
+    IsWellFounded.fix (motive := ({ c // ¬r · c })) r f v |>.val
+  { toFun := toFun
+    map_rel' {u v} hadj heq := by
+      -- As `r` is trichotomous and `u ≠ v` because they are adjacent in the graph, wlog `r u v`
+      wlog hr : r u v
+      · exact hadj.ne <| Std.Trichotomous.trichotomous u v hr <| this G r hadj.symm heq.symm
+      -- Therefore the color of `u` was considered when choosing a color for `v`
+      let sv := {toFun u | (u : V) (hu : r u v) (_ : G.Adj u v)}
+      have : toFun u ∈ sv := ⟨u, hr, hadj, rfl⟩
+      -- Since the color of `v` was chosen to be the minimum of the complement of `sv`,
+      -- it can't be in `sv`, so surely the colors of `u` and `v` cannot be the same
+      refine absurd this <| heq ▸ ?_
+      unfold toFun
+      rw [IsWellFounded.fix_eq]
+      refine IsWellFounded.wf.min_mem svᶜ ⟨v, fun ⟨w, hw, _, heq'⟩ ↦ absurd hw ?_⟩
+      rw [← heq']
+      exact IsWellFounded.fix r f w |>.prop }
+
+variable {G} in
+/-- Given a coloring of a graph, consider the mapped graph `G.map f` which can be thought of as
+taking the original graph `G` and considering every color class (independent set) as a single
+vertex. This greedily colors this graph by the given order on colors, which produces a new coloring
+of the original graph. -/
+noncomputable def Coloring.recolorGreedily {α : Type*} (r : α → α → Prop) [IsWellOrder α r]
+    (f : G.Coloring α) : G.Coloring α :=
+  G.map f |>.greedyColoring r |>.comp f.homMap
+
+/-- The color assigned to a vertex `v` by greedy coloring is not greater than `v` -/
+theorem not_lt_greedyColoring (v : V) : ¬r v (G.greedyColoring r v) := by
+  grind [greedyColoring, RelHom.coeFn_mk]
+
+/-- The set of colors that `v` could not use when `G` was greedily colored in the order specified
+by the given well-order -/
+def greedyColorsBefore (v : V) : Set V :=
+  {G.greedyColoring r u | (u) (_ : r u v) (_ : G.Adj u v)}
+
+variable {G r} in
+theorem greedyColoring_mem_greedyColorsBefore {u v : V} (hr : r u v) (hadj : G.Adj u v) :
+    G.greedyColoring r u ∈ G.greedyColorsBefore r v :=
+  ⟨u, hr, hadj, rfl⟩
+
+theorem lt_of_mem_greedyColorsBefore {u v : V} (h : u ∈ G.greedyColorsBefore r v) : r u v := by
+  obtain ⟨w, hr, _, rfl⟩ := h
+  exact trans_trichotomous_left (G.not_lt_greedyColoring r w) hr
+
+/-- Greedy coloring cannot get stuck since it is always possible for a vertex to be its own color -/
+theorem notMem_greedyColorsBefore_self (v : V) : v ∉ G.greedyColorsBefore r v :=
+  fun ⟨u, hu, _, heq⟩ ↦ heq ▸ G.not_lt_greedyColoring r u <| hu
+
+theorem greedyColorsBefore_subset_image_neighborSet (v : V) :
+    G.greedyColorsBefore r v ⊆ G.greedyColoring r '' G.neighborSet v :=
+  fun _u ⟨w, _, hwv, hu⟩ ↦ ⟨w, hwv.symm, hu⟩
+
+/-- Greedy coloring assigns the smallest available color -/
+theorem greedyColoring_eq_min (v : V) :
+    G.greedyColoring r v = IsWellFounded.wf.min (r := r) (G.greedyColorsBefore r v)ᶜ
+      ⟨v, G.notMem_greedyColorsBefore_self r v⟩ := by
+  rw [greedyColoring, RelHom.coeFn_mk, IsWellFounded.fix_eq]
+  rfl
+
+theorem greedyColoring_notMem_greedyColorsBefore (v : V) :
+    G.greedyColoring r v ∉ G.greedyColorsBefore r v := by
+  rw [greedyColoring_eq_min, ← Set.mem_compl_iff]
+  apply WellFounded.min_mem
+
+variable {G r} in
+theorem mem_greedyColorsBefore_of_lt_greedyColoring {u v : V} (h : r u (G.greedyColoring r v)) :
+    u ∈ G.greedyColorsBefore r v := by
+  rw [greedyColoring_eq_min] at h
+  exact WellFounded.mem_of_lt_min_compl h
+
+variable {G r} in
+theorem greedyColoring_eq_iff_subset_and_notMem {v c : V} :
+    G.greedyColoring r v = c ↔
+      {u | r u c} ⊆ G.greedyColorsBefore r v ∧ c ∉ G.greedyColorsBefore r v := by
+  refine ⟨(· ▸ ⟨?_, ?_⟩), fun ⟨hsub, hmem⟩ ↦ ?_⟩
+  · exact fun _ ↦ mem_greedyColorsBefore_of_lt_greedyColoring
+  · exact G.greedyColoring_notMem_greedyColorsBefore r v
+  · rw [greedyColoring_eq_min]
+    exact WellFounded.min_eq_of_forall_not_lt _ hmem <| Set.compl_subset_compl.mpr hsub
+
+variable {G r} in
+theorem greedyColoring_eq_of_greedyColorsBefore_eq {v c : V}
+    (h : G.greedyColorsBefore r v = {u | r u c}) : G.greedyColoring r v = c := by
+  rw [greedyColoring_eq_iff_subset_and_notMem, h]
+  exact ⟨Set.Subset.rfl, irrefl c⟩
+
+variable {G r} in
+theorem greedyColoring_eq_self_tfae {v : V} :
+    [G.greedyColoring r v = v, G.greedyColorsBefore r v = {u | r u v},
+      {u | r u v} ⊆ G.greedyColorsBefore r v].TFAE := by
+  tfae_have 1 → 3 := fun h u ↦ by
+    nth_rw 1 [← h]
+    exact mem_greedyColorsBefore_of_lt_greedyColoring
+  tfae_have 2 → 1 := greedyColoring_eq_of_greedyColorsBefore_eq
+  tfae_have 3 → 2 := antisymm fun _ ↦ G.lt_of_mem_greedyColorsBefore r
+  tfae_finish
+
+theorem isLowerSet_range_greedyColoring : @IsLowerSet V ⟨r⟩ <| Set.range <| G.greedyColoring r := by
+  rintro _ u hle ⟨v, rfl⟩
+  rcases mem_greedyColorsBefore_of_lt_greedyColoring hle with ⟨u, _, _, rfl⟩
+  exact Set.mem_range_self u
+
+theorem mk_greedyColorsBefore_le_coe_degree (v : V) [Fintype <| G.neighborSet v] :
+    #(G.greedyColorsBefore r v) ≤ G.degree v := by
+  rw [← G.card_neighborFinset_eq_degree, G.neighborFinset_def, ← Set.ncard_eq_toFinset_card',
+    Set.cast_ncard <| Set.toFinite _]
+  grw [← mk_image_le (f := G.greedyColoring r) (s := G.neighborSet v)]
+  exact mk_le_mk_of_subset <| G.greedyColorsBefore_subset_image_neighborSet r v
+
+theorem encard_greedyColorsBefore_le_coe_degree (v : V) [Fintype <| G.neighborSet v] :
+    (G.greedyColorsBefore r v).encard ≤ G.degree v := by
+  grw [G.greedyColorsBefore_subset_image_neighborSet r v, Set.encard_image_le]
+  rw [← card_neighborFinset_eq_degree, neighborFinset_def, Set.encard_eq_coe_toFinset_card]
+
+theorem ncard_greedyColorsBefore_le_degree (v : V) [Fintype <| G.neighborSet v] :
+    (G.greedyColorsBefore r v).ncard ≤ G.degree v := by
+  grw [← Nat.cast_le (α := ℕ∞), ← G.encard_greedyColorsBefore_le_coe_degree r v]
+  apply Set.ncard_le_encard
+
+variable {G r} in
+theorem greedyColoring_isClique_tfae {s : Set V} (hs : @IsLowerSet V ⟨r⟩ s) :
+    [s.InjOn (G.greedyColoring r), s.EqOn (G.greedyColoring r) id, G.IsClique s].TFAE := by
+  tfae_have 2 → 3 := fun h u hu v hv hne ↦ by
+    wlog huv : r u v
+    · refine this hs h v hv u hu hne.symm ?_ |>.symm
+      exact hne.imp_symm <| Std.Trichotomous.trichotomous u v huv
+    obtain ⟨u, hr, hadj, rfl⟩ := mem_greedyColorsBefore_of_lt_greedyColoring (h hv ▸ id_def v ▸ huv)
+    rwa [h <| hs hr hv]
+  tfae_have 3 → 2 := fun h v hv ↦ by
+    induction v using IsWellFounded.induction r with | ind v ih
+    rw [id_eq, greedyColoring_eq_self_tfae.out 0 2 rfl]
+    refine fun u huv ↦ ⟨u, huv, h (hs huv hv) hv (irrefl v <| · ▸ huv), ?_⟩
+    rw [ih u huv <| hs huv hv, id_eq]
+  tfae_have 1 → 2 :=
+    fun h ↦ hs.eqOn_id_of_injOn_of_forall_not_lt h fun v _ ↦ G.not_lt_greedyColoring r v
+  tfae_have 2 → 1 := fun h ↦ s.injOn_id.congr h.symm
+  tfae_finish
+
+variable {G r} in
+theorem greedyColoring_eq_id_tfae :
+    [Function.Injective (G.greedyColoring r), ↑(G.greedyColoring r) = id, G = ⊤].TFAE := by
+  rw [← Set.eqOn_univ, ← Set.injOn_univ, ← isClique_univ_iff]
+  exact greedyColoring_isClique_tfae <| @isLowerSet_univ V ⟨r⟩
+
+@[simp]
+theorem greedyColoring_top_eq_id : greedyColoring ⊤ r = .id :=
+  RelHom.ext <| congrFun <| greedyColoring_eq_id_tfae.out 2 1 |>.mp rfl
+
+theorem card_typein_greedyColoring_le_mk_greedyColorsBefore (v : V) :
+    (typein r <| G.greedyColoring r v).card ≤ #(G.greedyColorsBefore r v) := by
+  rw [greedyColoring_eq_min]
+  apply card_typein_min_le_mk
+
+theorem typein_greedyColoring_le_coe_degree (v : V) [Fintype <| G.neighborSet v] :
+    typein r (G.greedyColoring r v) ≤ G.degree v := by
+  grw [← card_le_nat, card_typein_greedyColoring_le_mk_greedyColorsBefore,
+    mk_greedyColorsBefore_le_coe_degree]
+
+theorem not_lt_enum_ord_greedyColorsBefore (v : V) (h : G.greedyColorsBefore r v |>.Finite) :
+    ¬r (enum r ⟨#(G.greedyColorsBefore r v) |>.ord,
+      ord_mk_lt_type r h ⟨v, G.notMem_greedyColorsBefore_self r v⟩⟩) (G.greedyColoring r v) := by
+  rw [greedyColoring_eq_min]
+  exact not_lt_enum_ord_mk_min_compl r h _
+
+theorem not_lt_enum_degree_greedyColoring (v : V) [Fintype <| G.neighborSet v] :
+    ¬r (enum r ⟨G.degree v, by
+      rw [Set.mem_Iio, ← card_neighborFinset_eq_degree, ← ord_nat, ← Cardinal.mk_coe_finset]
+      exact ord_mk_lt_type r (Finset.finite_toSet _) ⟨v, G.notMem_neighborFinset_self v⟩
+    ⟩) (G.greedyColoring r v) := by
+  grw [← typein_le_typein, typein_enum, typein_greedyColoring_le_coe_degree]
+
+variable {G} in
+/-- A graph is `α`-colorable iff there exists a well-ordering of its vertices such that
+greedy coloring uses at most `|α|` colors -/
+theorem nonempty_coloring_iff_exists_isWellOrder {α : Type*} :
+    Nonempty (G.Coloring α) ↔ ∃ (r : V → V → Prop) (_ : IsWellOrder V r),
+      Nonempty (Set.range (G.greedyColoring r) ↪ α) := by
+  refine ⟨fun ⟨C⟩ ↦ ?_,
+    fun ⟨r, _, ⟨f⟩⟩ ↦ ⟨Embedding.completeGraph f |>.toHom.comp <| G.greedyColoring r |>.attach⟩⟩
+  -- Take arbitrary well-orders on `α` and `V`, then order the vertices first by their color,
+  -- and then by themselves to break ties (i.e. use the lexicographic order).
+  let r := Prod.Lex WellOrderingRel WellOrderingRel |>.onFun fun v ↦ (C v, v)
+  have : IsWellOrder V r := Function.Injective.isWellOrder_onFun _ fun _ _ h ↦ congr(($h).snd)
+  -- For every color `v` assigned in the greedy coloring, let `f v` be the first vertex that was
+  -- greedy-colored by the color `v`, with respect to the order `r`.
+  let f : Set.range (G.greedyColoring r) → V := (IsWellFounded.wf.min (r := r) _ <| ·.prop)
+  -- We claim that `C ∘ f` is injective.
+  refine ⟨r, this, C ∘ f, fun u v heq ↦ Subtype.ext ?_⟩
+  -- WLOG `r u v` since `r` is trichotomous.
+  wlog hr : r u v
+  · grind [Std.Trichotomous.trichotomous (r := r)]
+  -- Since `f v` got the greedy-color `v`,
+  have : G.greedyColoring r (f v) = v := WellFounded.min_mem _ _ v.prop
+  -- and `u` precedes `v`, there must exist a `w` before `f v` with color `u` and `G.Adj w (f v)`.
+  have ⟨w, hrw, hadj, hw⟩ := mem_greedyColorsBefore_of_lt_greedyColoring <| this ▸ hr
+  -- Since `f u` is the first vertex with color `u`, we get `f u ≤ w < f v` (using `r`).
+  have hnrw : ¬r w (f u) := WellFounded.not_lt_min _ _ <| by exact hw
+  -- Due to the lexicographic order and `C (f u) = C (f v)`, we get `C w = C (f v)`.
+  -- But since `G.Adj w (f v)` and `C` is a valid coloring, this is a contradiction.
+  exact absurd (by grind) <| C.map_adj hadj
+
+theorem coe_greedyColoringOfEmbedding_le_degree {n : ℕ} (f : V ↪ Fin n) (v : V)
+    [Fintype <| G.neighborSet v] :
+    (G.coloringOfEmbedding f).recolorGreedily LT.lt v ≤ G.degree v := by
+  classical
+  grw [← G.degree_map f, ← Nat.cast_le (α := Ordinal),
+    ← typein_greedyColoring_le_coe_degree _ LT.lt, typein_lt_fin]
+  rfl
+
+/-- A coloring of a graph `G` using at most `G.maxDegree + 1` colors,
+constructed by greedy coloring in an arbitrary order -/
+noncomputable def coloringMaxDegreeAddOne [Fintype V] [DecidableRel G.Adj] :
+    G.Coloring <| Fin <| G.maxDegree + 1 :=
+  .castLT (G.coloringOfEmbedding (Fintype.equivFin V).toEmbedding |>.recolorGreedily LT.lt)
+    fun v ↦ by
+      grw [coe_greedyColoringOfEmbedding_le_degree, degree_le_maxDegree]
+      apply Nat.lt_add_one
+
+theorem colorable_maxDegree_add_one [Fintype V] [DecidableRel G.Adj] :
+    G.Colorable <| G.maxDegree + 1 :=
+  ⟨G.coloringMaxDegreeAddOne⟩
+
+theorem chromaticNumber_le_maxDegree_add_one [Fintype V] [DecidableRel G.Adj] :
+    G.chromaticNumber ≤ G.maxDegree + 1 :=
+  G.colorable_maxDegree_add_one.chromaticNumber_le
+
+end SimpleGraph
diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean
index 99df79691738ff..ea5885898ca8ed 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean
@@ -57,6 +57,17 @@ the colors.
   * develop API for partial colorings, likely as colorings of subgraphs (`H.coe.Coloring α`)
 -/
 
+@[expose] public section Dependencies
+
+set_option warn.sorry false
+set_option linter.style.longLine false
+set_option linter.missingDocs false
+
+/-- #35628 -/
+@[simps] def SimpleGraph.Hom.map {V W : Type*} (f : V → W) (G : SimpleGraph V) (h : ∀ {u v}, G.Adj u v → f u ≠ f v) : G →g G.map f := ⟨f, sorry⟩
+
+end Dependencies
+
 @[expose] public section
 
 assert_not_exists Field
@@ -284,6 +295,35 @@ theorem Colorable.of_hom {V' : Type*} {G' : SimpleGraph V'} (f : G →g G') {n :
     (h : G'.Colorable n) : G.Colorable n :=
   ⟨(h.toColoring (by simp)).comp f⟩
 
+/-- Given an `ℕ`-coloring where only colors below `n` are used, convert it to an `n`-coloring -/
+@[simps!]
+def Coloring.natToFin {n : ℕ} (C : G.Coloring ℕ) (h : ∀ v, C v < n) : G.Coloring <| Fin n :=
+  .mk (fun v ↦ ⟨C v, h v⟩) <| by grind [C.valid]
+
+/-- Given a `k`-coloring where only colors below `n` are used, convert it to an `n`-coloring -/
+@[simps!]
+def Coloring.castLT {k n : ℕ} (C : G.Coloring <| Fin k) (h : ∀ v, C v < n) : G.Coloring <| Fin n :=
+  .mk (fun v ↦ C v |>.castLT <| h v) <| by grind [Fin.castLT, C.valid]
+
+/-- Given an `α`-coloring `C`, convert it to a coloring where the only available colors are from the
+range of `C`, possibly producing a coloring with fewer colors -/
+@[simps!]
+def Coloring.attach (C : G.Coloring α) : G.Coloring <| Set.range C :=
+  .mk (Set.rangeFactorization C) <| by grind [Set.rangeFactorization, C.valid]
+
+variable (G) in
+/-- Color a graph using an embedding of its vertices to colors -/
+@[simps!]
+def coloringOfEmbedding {α : Type*} (f : V ↪ α) : G.Coloring α :=
+  G.recolorOfEmbedding f G.selfColoring
+
+/-- A coloring of a graph `G` is a homomorphism from it to the mapped graph.
+This is `Hom.map` spelled using colorings. The mapped graph `G.map f` can be thought of as taking
+the original graph `G` and considering every color class (independent set) as a single vertex. -/
+@[simps!]
+def Coloring.homMap {α : Type*} (f : G.Coloring α) : G →g G.map f :=
+  .map f G f.map_adj
+
 theorem colorable_iff_exists_bdd_nat_coloring (n : ℕ) :
     G.Colorable n ↔ ∃ C : G.Coloring ℕ, ∀ v, C v < n := by
   constructor
diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
index 0bd2fc936d8797..2201a272fdc19f 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Combinatorics.SimpleGraph.Maps
 public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Set.Card
 public import Mathlib.Data.Sym.Card
 
 /-!
@@ -40,6 +41,16 @@ or `card_verts`.
   is locally finite, too.
 -/
 
+@[expose] public section Dependencies
+
+set_option warn.sorry false
+set_option linter.style.longLine false
+
+-- #35628
+theorem SimpleGraph.neighborSet_map {V W : Type*} (G : SimpleGraph V) (v : V) (f : V ↪ W) : (G.map f).neighborSet (f v) = f '' G.neighborSet v := sorry
+
+end Dependencies
+
 @[expose] public section
 
 
@@ -392,7 +403,7 @@ theorem exists_minimal_degree_vertex [DecidableRel G.Adj] [Nonempty V] :
     ∃ v, G.minDegree = G.degree v := by
   obtain ⟨t, ht : _ = _⟩ := min_of_nonempty (univ_nonempty.image fun v => G.degree v)
   obtain ⟨v, _, rfl⟩ := mem_image.mp (mem_of_min ht)
-  exact ⟨v, by simp [minDegree, ht]⟩
+  exact ⟨v, by simp [minDegree, ht, -ENat.some_eq_coe]⟩
 
 /-- The minimum degree in the graph is at most the degree of any particular vertex. -/
 theorem minDegree_le_degree [DecidableRel G.Adj] (v : V) : G.minDegree ≤ G.degree v := by
@@ -493,7 +504,7 @@ lemma minDegree_le_maxDegree [DecidableRel G.Adj] : G.minDegree ≤ G.maxDegree
 
 theorem IsRegularOfDegree.minDegree_eq [Nonempty V] [DecidableRel G.Adj] {d : ℕ}
     (h : G.IsRegularOfDegree d) : G.minDegree = d := by
-  simp [minDegree, h.degree_eq, Finset.image_const]
+  simp [minDegree, h.degree_eq, Finset.image_const, -ENat.some_eq_coe]
 
 @[simp]
 lemma minDegree_bot_eq_zero : (⊥ : SimpleGraph V).minDegree = 0 :=
@@ -679,6 +690,12 @@ theorem card_edgeFinset_map (f : V ↪ W) (G : SimpleGraph V) [DecidableRel G.Ad
   rw [edgeFinset_map]
   exact G.edgeFinset.card_map f.sym2Map
 
+theorem degree_map {V W : Type*} (G : SimpleGraph V) (f : V ↪ W) (v : V)
+    [Fintype <| G.neighborSet v] [Fintype <| G.map f |>.neighborSet <| f v] :
+    (G.map f).degree (f v) = G.degree v := by
+  simp_rw [← card_neighborSet_eq_degree, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
+    ← Set.ncard_image_of_injective _ f.injective, neighborSet_map]
+
 end Map
 
 end SimpleGraph

From 4671689383778879d20fdfec267ce5a5ffde4cc2 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 22 Apr 2026 07:12:19 +0300
Subject: [PATCH 02/13] `mk_all`

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 4c2d2eba135003..2ae52cc4dbd831 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3519,6 +3519,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Circulant
 public import Mathlib.Combinatorics.SimpleGraph.Clique
 public import Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
 public import Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
+public import Mathlib.Combinatorics.SimpleGraph.Coloring.Greedy
 public import Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
 public import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

From 7b08e5ec209820a25c79c964f8d0c1ef840bdd71 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 22 Apr 2026 07:12:43 +0300
Subject: [PATCH 03/13] remove import

---
 Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
index 029777e484814c..c56ce64451a508 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -6,7 +6,6 @@ Authors: Snir Broshi
 module
 
 public import Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
-public import Mathlib.Data.Set.Card
 public import Mathlib.SetTheory.Ordinal.Arithmetic
 
 /-!

From b08e65444345d8c386fe252a9d8628892cec77c3 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 23 Apr 2026 19:43:09 +0300
Subject: [PATCH 04/13] extract `Coloring.homMap` to separate PR

---
 .../SimpleGraph/Coloring/Greedy.lean           |  2 ++
 .../SimpleGraph/Coloring/VertexColoring.lean   | 18 ------------------
 2 files changed, 2 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
index c56ce64451a508..cb283c88f037c7 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -29,6 +29,8 @@ theorem SimpleGraph.Embedding.image_neighborSet {V V' : Type*} {G : SimpleGraph
 theorem IsLowerSet.eqOn_id_of_injOn_of_forall_not_lt {α : Type*} {r : α → α → Prop} [IsWellOrder α r] {s : Set α} (hs : @IsLowerSet α ⟨r⟩ s) {f : α → α} (hf : s.InjOn f) (h : ∀ x ∈ s, ¬r x (f x)) : s.EqOn f id := sorry
 -- #36626
 theorem IsWellOrder.eq_id_of_injective_of_forall_not_lt {α : Type*} {r : α → α → Prop} [IsWellOrder α r] {f : α → α} (hf : f.Injective) (h : ∀ x, ¬r x (f x)) : f = id := sorry
+/-- #38422 -/
+@[simps] def SimpleGraph.Coloring.homMap {V α : Type*} {G : SimpleGraph V} (f : G.Coloring α) : G →g G.map f := ⟨f, sorry⟩
 
 end Dependencies
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean
index ea5885898ca8ed..c082b80229c8c1 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean
@@ -57,17 +57,6 @@ the colors.
   * develop API for partial colorings, likely as colorings of subgraphs (`H.coe.Coloring α`)
 -/
 
-@[expose] public section Dependencies
-
-set_option warn.sorry false
-set_option linter.style.longLine false
-set_option linter.missingDocs false
-
-/-- #35628 -/
-@[simps] def SimpleGraph.Hom.map {V W : Type*} (f : V → W) (G : SimpleGraph V) (h : ∀ {u v}, G.Adj u v → f u ≠ f v) : G →g G.map f := ⟨f, sorry⟩
-
-end Dependencies
-
 @[expose] public section
 
 assert_not_exists Field
@@ -317,13 +306,6 @@ variable (G) in
 def coloringOfEmbedding {α : Type*} (f : V ↪ α) : G.Coloring α :=
   G.recolorOfEmbedding f G.selfColoring
 
-/-- A coloring of a graph `G` is a homomorphism from it to the mapped graph.
-This is `Hom.map` spelled using colorings. The mapped graph `G.map f` can be thought of as taking
-the original graph `G` and considering every color class (independent set) as a single vertex. -/
-@[simps!]
-def Coloring.homMap {α : Type*} (f : G.Coloring α) : G →g G.map f :=
-  .map f G f.map_adj
-
 theorem colorable_iff_exists_bdd_nat_coloring (n : ℕ) :
     G.Colorable n ↔ ∃ C : G.Coloring ℕ, ∀ v, C v < n := by
   constructor

From 636a46b88de43e7bfced00d68377a385f70294ed Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 29 Apr 2026 06:52:11 +0300
Subject: [PATCH 05/13] update dependencies

---
 Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean |  6 +-----
 Mathlib/Combinatorics/SimpleGraph/Finite.lean          | 10 ----------
 2 files changed, 1 insertion(+), 15 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
index cb283c88f037c7..05578196376072 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -21,10 +21,6 @@ set_option linter.style.longLine false
 theorem SimpleGraph.isClique_top {α : Type*} (s : Set α) : (⊤ : SimpleGraph α).IsClique s := sorry
 -- #35619
 theorem SimpleGraph.isClique_univ_iff {V : Type*} (G : SimpleGraph V) : G.IsClique .univ ↔ G = ⊤ := sorry
--- #35622
-theorem Function.Injective.isWellOrder_onFun {α β : Type*} (r : β → β → Prop) {f : α → β} (hf : f.Injective) [IsWellOrder β r] : IsWellOrder α (r.onFun f) := sorry
--- #35628
-theorem SimpleGraph.Embedding.image_neighborSet {V V' : Type*} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G ↪g G'} (v : V) : f '' G.neighborSet v = G'.neighborSet (f v) ∩ Set.range f := sorry
 -- #36626
 theorem IsLowerSet.eqOn_id_of_injOn_of_forall_not_lt {α : Type*} {r : α → α → Prop} [IsWellOrder α r] {s : Set α} (hs : @IsLowerSet α ⟨r⟩ s) {f : α → α} (hf : s.InjOn f) (h : ∀ x ∈ s, ¬r x (f x)) : s.EqOn f id := sorry
 -- #36626
@@ -239,7 +235,7 @@ theorem nonempty_coloring_iff_exists_isWellOrder {α : Type*} :
   -- Take arbitrary well-orders on `α` and `V`, then order the vertices first by their color,
   -- and then by themselves to break ties (i.e. use the lexicographic order).
   let r := Prod.Lex WellOrderingRel WellOrderingRel |>.onFun fun v ↦ (C v, v)
-  have : IsWellOrder V r := Function.Injective.isWellOrder_onFun _ fun _ _ h ↦ congr(($h).snd)
+  have : IsWellOrder V r := Function.Injective.isWellOrder _ fun _ _ h ↦ congr(($h).snd)
   -- For every color `v` assigned in the greedy coloring, let `f v` be the first vertex that was
   -- greedy-colored by the color `v`, with respect to the order `r`.
   let f : Set.range (G.greedyColoring r) → V := (IsWellFounded.wf.min (r := r) _ <| ·.prop)
diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
index 4e065c127d7509..b25796dcddb91a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -41,16 +41,6 @@ or `card_verts`.
   is locally finite, too.
 -/
 
-@[expose] public section Dependencies
-
-set_option warn.sorry false
-set_option linter.style.longLine false
-
--- #35628
-theorem SimpleGraph.neighborSet_map {V W : Type*} (G : SimpleGraph V) (v : V) (f : V ↪ W) : (G.map f).neighborSet (f v) = f '' G.neighborSet v := sorry
-
-end Dependencies
-
 @[expose] public section
 
 

From 01f173afa690f42926eab0cbd6f5e1b837b3e65b Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 29 Apr 2026 07:32:43 +0300
Subject: [PATCH 06/13] delete unused dependencies

---
 Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
index 05578196376072..ceac5357d55f8c 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -17,16 +17,12 @@ public import Mathlib.SetTheory.Ordinal.Arithmetic
 set_option warn.sorry false
 set_option linter.style.longLine false
 
--- #35619
-theorem SimpleGraph.isClique_top {α : Type*} (s : Set α) : (⊤ : SimpleGraph α).IsClique s := sorry
 -- #35619
 theorem SimpleGraph.isClique_univ_iff {V : Type*} (G : SimpleGraph V) : G.IsClique .univ ↔ G = ⊤ := sorry
 -- #36626
 theorem IsLowerSet.eqOn_id_of_injOn_of_forall_not_lt {α : Type*} {r : α → α → Prop} [IsWellOrder α r] {s : Set α} (hs : @IsLowerSet α ⟨r⟩ s) {f : α → α} (hf : s.InjOn f) (h : ∀ x ∈ s, ¬r x (f x)) : s.EqOn f id := sorry
--- #36626
-theorem IsWellOrder.eq_id_of_injective_of_forall_not_lt {α : Type*} {r : α → α → Prop} [IsWellOrder α r] {f : α → α} (hf : f.Injective) (h : ∀ x, ¬r x (f x)) : f = id := sorry
 /-- #38422 -/
-@[simps] def SimpleGraph.Coloring.homMap {V α : Type*} {G : SimpleGraph V} (f : G.Coloring α) : G →g G.map f := ⟨f, sorry⟩
+@[simps] abbrev SimpleGraph.Coloring.homMap {V α : Type*} {G : SimpleGraph V} (f : G.Coloring α) : G →g G.map f := ⟨f, sorry⟩
 
 end Dependencies
 

From 216316e3d2e24cb39ec36549457ca40d4ebc2fca Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 6 May 2026 13:19:22 +0300
Subject: [PATCH 07/13] name fixes

---
 Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean | 6 +++---
 Mathlib/Combinatorics/SimpleGraph/Finite.lean          | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
index ceac5357d55f8c..b2f4e4b8ee9374 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -250,11 +250,11 @@ theorem nonempty_coloring_iff_exists_isWellOrder {α : Type*} :
   -- But since `G.Adj w (f v)` and `C` is a valid coloring, this is a contradiction.
   exact absurd (by grind) <| C.map_adj hadj
 
-theorem coe_greedyColoringOfEmbedding_le_degree {n : ℕ} (f : V ↪ Fin n) (v : V)
+theorem coe_recolorGreedily_coloringOfEmbedding_le_degree {n : ℕ} (f : V ↪ Fin n) (v : V)
     [Fintype <| G.neighborSet v] :
     (G.coloringOfEmbedding f).recolorGreedily LT.lt v ≤ G.degree v := by
   classical
-  grw [← G.degree_map f, ← Nat.cast_le (α := Ordinal),
+  grw [← G.degree_map_apply f, ← Nat.cast_le (α := Ordinal),
     ← typein_greedyColoring_le_coe_degree _ LT.lt, typein_lt_fin]
   rfl
 
@@ -264,7 +264,7 @@ noncomputable def coloringMaxDegreeAddOne [Fintype V] [DecidableRel G.Adj] :
     G.Coloring <| Fin <| G.maxDegree + 1 :=
   .castLT (G.coloringOfEmbedding (Fintype.equivFin V).toEmbedding |>.recolorGreedily LT.lt)
     fun v ↦ by
-      grw [coe_greedyColoringOfEmbedding_le_degree, degree_le_maxDegree]
+      grw [coe_recolorGreedily_coloringOfEmbedding_le_degree, degree_le_maxDegree]
       apply Nat.lt_add_one
 
 theorem colorable_maxDegree_add_one [Fintype V] [DecidableRel G.Adj] :
diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
index b25796dcddb91a..db3c713ba4dd98 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -640,7 +640,7 @@ theorem card_edgeFinset_map (f : V ↪ W) (G : SimpleGraph V) [DecidableRel G.Ad
   rw [edgeFinset_map]
   exact G.edgeFinset.card_map f.sym2Map
 
-theorem degree_map {V W : Type*} (G : SimpleGraph V) (f : V ↪ W) (v : V)
+theorem degree_map_apply {V W : Type*} (G : SimpleGraph V) (f : V ↪ W) (v : V)
     [Fintype <| G.neighborSet v] [Fintype <| G.map f |>.neighborSet <| f v] :
     (G.map f).degree (f v) = G.degree v := by
   simp_rw [← card_neighborSet_eq_degree, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',

From 246b047166308b76c9e1ca579bc750a713e7792e Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 21 May 2026 15:22:43 +0300
Subject: [PATCH 08/13] `homMap` dependency was merged

---
 Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
index b2f4e4b8ee9374..a9d7dd33da8997 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -21,8 +21,6 @@ set_option linter.style.longLine false
 theorem SimpleGraph.isClique_univ_iff {V : Type*} (G : SimpleGraph V) : G.IsClique .univ ↔ G = ⊤ := sorry
 -- #36626
 theorem IsLowerSet.eqOn_id_of_injOn_of_forall_not_lt {α : Type*} {r : α → α → Prop} [IsWellOrder α r] {s : Set α} (hs : @IsLowerSet α ⟨r⟩ s) {f : α → α} (hf : s.InjOn f) (h : ∀ x ∈ s, ¬r x (f x)) : s.EqOn f id := sorry
-/-- #38422 -/
-@[simps] abbrev SimpleGraph.Coloring.homMap {V α : Type*} {G : SimpleGraph V} (f : G.Coloring α) : G →g G.map f := ⟨f, sorry⟩
 
 end Dependencies
 

From 22083cf5173a44e2a6f2537e1cc08ce5efeca53e Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 21 May 2026 15:40:51 +0300
Subject: [PATCH 09/13] fix deprecated ordinal lemma usage

---
 Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
index a9d7dd33da8997..09873ced88fb68 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -213,7 +213,7 @@ theorem not_lt_enum_ord_greedyColorsBefore (v : V) (h : G.greedyColorsBefore r v
 
 theorem not_lt_enum_degree_greedyColoring (v : V) [Fintype <| G.neighborSet v] :
     ¬r (enum r ⟨G.degree v, by
-      rw [Set.mem_Iio, ← card_neighborFinset_eq_degree, ← ord_nat, ← Cardinal.mk_coe_finset]
+      rw [Set.mem_Iio, ← card_neighborFinset_eq_degree, ← ord_natCast, ← Cardinal.mk_coe_finset]
       exact ord_mk_lt_type r (Finset.finite_toSet _) ⟨v, G.notMem_neighborFinset_self v⟩
     ⟩) (G.greedyColoring r v) := by
   grw [← typein_le_typein, typein_enum, typein_greedyColoring_le_coe_degree]

From e0808a045b83ff925ea4a8009285ca32bf8d9d0f Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 1 Jun 2026 06:11:03 +0300
Subject: [PATCH 10/13] exclude `Set.fintypeCard_eq_ncard` in `simp`

---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean     | 2 +-
 Mathlib/Combinatorics/SimpleGraph/Finite.lean   | 7 ++++---
 Mathlib/Combinatorics/SimpleGraph/Subgraph.lean | 2 +-
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index e17ae25f87c389..41a16c0b477de2 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -314,7 +314,7 @@ alias ⟨IsContained.exists_iso_subgraph, IsContained.of_exists_iso_subgraph⟩
 
 theorem Copy.degree_le (f : Copy G H) (v : V) [Fintype <| G.neighborSet v]
     [Fintype <| H.neighborSet (f v)] : G.degree v ≤ H.degree (f v) := by
-  simpa [card_neighborSet_eq_degree] using
+  simpa [card_neighborSet_eq_degree, -Set.fintypeCard_eq_ncard] using
     Fintype.card_le_of_injective _ (f.mapNeighborSet v).injective
 
 theorem Copy.max_degree_le [Fintype V] [Fintype W] [DecidableRel G.Adj] [DecidableRel H.Adj]
diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
index 5847934d097517..e811e763645ca3 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -126,7 +126,7 @@ theorem card_edgeSet : Fintype.card G.edgeSet = #G.edgeFinset :=
   .symm <| Set.toFinset_card _
 
 theorem edgeSet_univ_card : #(univ : Finset G.edgeSet) = #G.edgeFinset := by
-  simp [card_edgeSet]
+  simp [card_edgeSet, -Set.fintypeCard_eq_ncard]
 
 variable [Fintype V]
 
@@ -255,7 +255,7 @@ theorem degree_compl [Fintype (Gᶜ.neighborSet v)] [Fintype V] :
   classical
     rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
     simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v)),
-      card_neighborSet_eq_degree]
+      card_neighborSet_eq_degree, -Set.fintypeCard_eq_ncard]
 
 instance incidenceSetFintype [DecidableEq V] : Fintype (G.incidenceSet v) :=
   Fintype.ofEquiv (G.neighborSet v) (G.incidenceSetEquivNeighborSet v).symm
@@ -526,7 +526,8 @@ theorem Adj.card_commonNeighbors_lt_degree {G : SimpleGraph V} [DecidableRel G.A
 
 theorem card_commonNeighbors_top [DecidableEq V] {v w : V} (h : v ≠ w) :
     Fintype.card (commonNeighbors ⊤ v w) = Fintype.card V - 2 := by
-  simp [commonNeighbors_top_eq, ← Set.toFinset_card, Finset.card_sdiff, h]
+  simp [commonNeighbors_top_eq, ← Set.toFinset_card, Finset.card_sdiff, h,
+    -Set.fintypeCard_eq_ncard]
 
 end Finite
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
index 3dde862f14c0e5..ae6c3ed9f658cd 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@@ -879,7 +879,7 @@ theorem card_neighborSet_toSubgraph (G H : SimpleGraph V) (h : H ≤ G)
 lemma degree_toSubgraph (G H : SimpleGraph V) (h : H ≤ G) {v : V}
     [Fintype ↑((toSubgraph H h).neighborSet v)] [Fintype ↑(H.neighborSet v)] :
     (toSubgraph H h).degree v = H.degree v := by
-  simp [Subgraph.degree, card_neighborSet_toSubgraph]
+  simp [Subgraph.degree, card_neighborSet_toSubgraph, -Set.fintypeCard_eq_ncard]
 
 section MkProperties
 

From ac5f9cae5343fc6ed51ddad8e0520df2b7e49d3d Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 1 Jun 2026 06:13:46 +0300
Subject: [PATCH 11/13] dependency was merged

---
 Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
index 09873ced88fb68..4030e09a4d72bd 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -17,8 +17,6 @@ public import Mathlib.SetTheory.Ordinal.Arithmetic
 set_option warn.sorry false
 set_option linter.style.longLine false
 
--- #35619
-theorem SimpleGraph.isClique_univ_iff {V : Type*} (G : SimpleGraph V) : G.IsClique .univ ↔ G = ⊤ := sorry
 -- #36626
 theorem IsLowerSet.eqOn_id_of_injOn_of_forall_not_lt {α : Type*} {r : α → α → Prop} [IsWellOrder α r] {s : Set α} (hs : @IsLowerSet α ⟨r⟩ s) {f : α → α} (hf : s.InjOn f) (h : ∀ x ∈ s, ¬r x (f x)) : s.EqOn f id := sorry
 
@@ -188,7 +186,7 @@ theorem greedyColoring_isClique_tfae {s : Set V} (hs : @IsLowerSet V ⟨r⟩ s)
 variable {G r} in
 theorem greedyColoring_eq_id_tfae :
     [Function.Injective (G.greedyColoring r), ↑(G.greedyColoring r) = id, G = ⊤].TFAE := by
-  rw [← Set.eqOn_univ, ← Set.injOn_univ, ← isClique_univ_iff]
+  rw [← Set.eqOn_univ, ← Set.injOn_univ, ← isClique_univ]
   exact greedyColoring_isClique_tfae <| @isLowerSet_univ V ⟨r⟩
 
 @[simp]

From 624a1c1ede43d6524a3da2d5a24ffd4e4029f234 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Tue, 2 Jun 2026 07:06:15 +0300
Subject: [PATCH 12/13] fix

---
 Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
index 05fb44896d50fe..d64a3cf732e03e 100644
--- a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
@@ -106,7 +106,8 @@ variable [NonAssocSemiring R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e
 
 theorem sum_incMatrix_apply [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :
     ∑ e, G.incMatrix R a e = G.degree a := by
-  simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset, card_incidenceSet_eq_degree]
+  simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset, card_incidenceSet_eq_degree,
+    -Set.fintypeCard_eq_ncard]
 
 theorem incMatrix_mul_transpose_diag [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :
     (G.incMatrix R * (G.incMatrix R)ᵀ) a a = G.degree a := by

From 4df25829492984dcdcc5f6e56e503ea6ee72740d Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sun, 7 Jun 2026 20:33:35 +0300
Subject: [PATCH 13/13] fix import after merge

---
 Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
index 4030e09a4d72bd..4866661a558501 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/Greedy.lean
@@ -5,7 +5,7 @@ Authors: Snir Broshi
 -/
 module
 
-public import Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
+public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
 public import Mathlib.SetTheory.Ordinal.Arithmetic
 
 /-!