feat(Combinatorics/SimpleGraph/Coloring/Greedy): Greedy coloring

[SnirBroshi]

---

Dependencies are included as sorried theorems to make the diff saner, but exist in the dependent PRs in full.

• depends on: [Merged by Bors] - feat(Combinatorics/SimpleGraph/Clique): intersection and union of cliques #35619
• depends on: [Merged by Bors] - feat(Logic/Function/Basic): onFun and swap preserve relation properties #35622
• depends on: [Merged by Bors] - feat(Combinatorics/SimpleGraph/Maps): characterize neighborSet and edgeSet across an embedding #35628
• depends on: feat(Order/UpperLower/Basic): an injective function constrained by the identity function using a well-order is the identity #36626
• depends on: [Merged by Bors] - feat(Combinatorics/SimpleGraph/Maps): G →g G.map f #38422
• depends on: feat(Combinatorics/SimpleGraph/Finite): Set.ncard of neighborSet #40624

[github-actions]

PR summary 90a26f1466

Import changes exceeding 2%

%	File
+30.82%	Mathlib.Combinatorics.SimpleGraph.Copy
+34.45%	Mathlib.Combinatorics.SimpleGraph.Finite
+9.90%	Mathlib.Combinatorics.SimpleGraph.IncMatrix
+31.55%	Mathlib.Combinatorics.SimpleGraph.Subgraph

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Finite	566	761	+195 (+34.45%)
Mathlib.Combinatorics.SimpleGraph.Subgraph	580	763	+183 (+31.55%)
Mathlib.Combinatorics.SimpleGraph.Copy	584	764	+180 (+30.82%)
Mathlib.Combinatorics.SimpleGraph.IncMatrix	798	877	+79 (+9.90%)

Import changes for all files

Files	Import difference
10 files Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite	1
Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic	59
Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Metric	75
Mathlib.Combinatorics.SimpleGraph.IncMatrix	79
Mathlib.Combinatorics.SimpleGraph.Extremal.Basic	100
3 files Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Finsubgraph	133
Mathlib.Combinatorics.SimpleGraph.Trails	151
Mathlib.Combinatorics.SimpleGraph.Copy Mathlib.Combinatorics.SimpleGraph.LineGraph	180
Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected	181
Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Combinatorics.SimpleGraph.Subgraph	183
4 files Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.Paths Mathlib.Combinatorics.SimpleGraph.Walk.Counting Mathlib.Combinatorics.SimpleGraph.Walks.Counting	187
9 files Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp Mathlib.Combinatorics.SimpleGraph.EdgeLabeling Mathlib.Combinatorics.SimpleGraph.Walk.Decomp Mathlib.Combinatorics.SimpleGraph.Walk.Maps Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks Mathlib.Combinatorics.SimpleGraph.Walks.Decomp Mathlib.Combinatorics.SimpleGraph.Walks.Maps Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks	189
Mathlib.Combinatorics.SimpleGraph.DeleteEdges	190
Mathlib.Combinatorics.SimpleGraph.Finite	195
Mathlib.Combinatorics.SimpleGraph.Coloring.Greedy (new file)	806

---

Declarations diff (regex)

+ Coloring.attach
+ Coloring.castLT
+ Coloring.natToFin
+ Coloring.recolorGreedily
+ IsLowerSet.eqOn_id_of_injOn_of_forall_not_lt
+ card_typein_greedyColoring_le_mk_greedyColorsBefore
+ chromaticNumber_le_maxDegree_add_one
+ coe_recolorGreedily_coloringOfEmbedding_le_degree
+ colorable_maxDegree_add_one
+ coloringMaxDegreeAddOne
+ coloringOfEmbedding
+ degree_map_apply
+ encard_greedyColorsBefore_le_coe_degree
+ greedyColoring
+ greedyColoring_eq_id_tfae
+ greedyColoring_eq_iff_subset_and_notMem
+ greedyColoring_eq_min
+ greedyColoring_eq_of_greedyColorsBefore_eq
+ greedyColoring_eq_self_tfae
+ greedyColoring_isClique_tfae
+ greedyColoring_mem_greedyColorsBefore
+ greedyColoring_notMem_greedyColorsBefore
+ greedyColoring_top_eq_id
+ greedyColorsBefore
+ greedyColorsBefore_subset_image_neighborSet
+ isLowerSet_range_greedyColoring
+ lt_of_mem_greedyColorsBefore
+ mem_greedyColorsBefore_of_lt_greedyColoring
+ mk_greedyColorsBefore_le_coe_degree
+ ncard_greedyColorsBefore_le_degree
+ nonempty_coloring_iff_exists_isWellOrder
+ notMem_greedyColorsBefore_self
+ not_lt_enum_degree_greedyColoring
+ not_lt_enum_ord_greedyColorsBefore
+ not_lt_greedyColoring
+ typein_greedyColoring_le_coe_degree

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 90a26f1).

• +42 new declarations
• −0 removed declarations

+IsLowerSet.eqOn_id_of_injOn_of_forall_not_lt
+IsWellFounded.fix.congr_simp
+SimpleGraph.Coloring.attach
+SimpleGraph.Coloring.attach_apply_coe
+SimpleGraph.Coloring.castLT
+SimpleGraph.Coloring.castLT_apply_val
+SimpleGraph.Coloring.natToFin
+SimpleGraph.Coloring.natToFin_apply_val
+SimpleGraph.Coloring.recolorGreedily
+SimpleGraph.card_typein_greedyColoring_le_mk_greedyColorsBefore
+SimpleGraph.chromaticNumber_le_maxDegree_add_one
+SimpleGraph.coe_recolorGreedily_coloringOfEmbedding_le_degree
+SimpleGraph.colorable_maxDegree_add_one
+SimpleGraph.coloringMaxDegreeAddOne
+SimpleGraph.coloringOfEmbedding
+SimpleGraph.coloringOfEmbedding_apply
+SimpleGraph.degree_map_apply
+SimpleGraph.encard_greedyColorsBefore_le_coe_degree
+SimpleGraph.greedyColoring
+SimpleGraph.greedyColoring.congr_simp
+SimpleGraph.greedyColoring_eq_id_tfae
+SimpleGraph.greedyColoring_eq_iff_subset_and_notMem
+SimpleGraph.greedyColoring_eq_min
+SimpleGraph.greedyColoring_eq_of_greedyColorsBefore_eq
+SimpleGraph.greedyColoring_eq_self_tfae
+SimpleGraph.greedyColoring_isClique_tfae
+SimpleGraph.greedyColoring_mem_greedyColorsBefore
+SimpleGraph.greedyColoring_notMem_greedyColorsBefore
+SimpleGraph.greedyColoring_top_eq_id
+SimpleGraph.greedyColorsBefore
+SimpleGraph.greedyColorsBefore_subset_image_neighborSet
+SimpleGraph.isLowerSet_range_greedyColoring
+SimpleGraph.lt_of_mem_greedyColorsBefore
+SimpleGraph.mem_greedyColorsBefore_of_lt_greedyColoring
+SimpleGraph.mk_greedyColorsBefore_le_coe_degree
+SimpleGraph.ncard_greedyColorsBefore_le_degree
+SimpleGraph.nonempty_coloring_iff_exists_isWellOrder
+SimpleGraph.notMem_greedyColorsBefore_self
+SimpleGraph.not_lt_enum_degree_greedyColoring
+SimpleGraph.not_lt_enum_ord_greedyColorsBefore
+SimpleGraph.not_lt_greedyColoring
+SimpleGraph.typein_greedyColoring_le_coe_degree

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
4942	1	exposed public sections

Current commit 90a26f1466
Reference commit 261b5e314a

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Combinatorics/SimpleGraph/Clique): intersection and union of cliques #35619
• [Merged by Bors] - feat(Logic/Function/Basic): onFun and swap preserve relation properties #35622
• [Merged by Bors] - feat(Combinatorics/SimpleGraph/Maps): characterize neighborSet and edgeSet across an embedding #35628
• feat(Order/UpperLower/Basic): an injective function constrained by the identity function using a well-order is the identity #36626
• [Merged by Bors] - feat(Combinatorics/SimpleGraph/Maps): G →g G.map f #38422
• feat(Combinatorics/SimpleGraph/Finite): Set.ncard of neighborSet #40624
  By Dependent Issues (🤖). Happy coding!