feat(Combinatorics/SimpleGraph/Finite): Set.ncard of neighborSet

[SnirBroshi]

Since #39414 the simpNF of the cardinality of neighborSet uses Set.ncard rather than Fintype.card, therefore we import Set.ncard into SimpleGraph/Finite.lean and show (G.neighborSet v).ncard = G.degree v.

Also includes some other results that benefit from the import/lemma:

• (commonNeighbors ⊤ u v).encard = ENat.card V - 2
• (G.map f).degree (f v) = G.degree v for an injective f
• G'.degree (f v) = G.degree v for f : G ↪g G', given G'.neighborSet (f v) ⊆ Set.range f

---

[github-actions]

PR summary 7c6196c20f

Import changes exceeding 2%

%	File
+33.39%	Mathlib.Combinatorics.SimpleGraph.Finite
+9.72%	Mathlib.Combinatorics.SimpleGraph.IncMatrix
+30.59%	Mathlib.Combinatorics.SimpleGraph.Subgraph

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Finite	581	775	+194 (+33.39%)
Mathlib.Combinatorics.SimpleGraph.Subgraph	595	777	+182 (+30.59%)
Mathlib.Combinatorics.SimpleGraph.IncMatrix	813	892	+79 (+9.72%)

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	179
Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected	180
Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Combinatorics.SimpleGraph.Subgraph	182
4 files Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.Paths Mathlib.Combinatorics.SimpleGraph.Walk.Counting Mathlib.Combinatorics.SimpleGraph.Walks.Counting	186
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	188
Mathlib.Combinatorics.SimpleGraph.DeleteEdges	189
Mathlib.Combinatorics.SimpleGraph.Finite	194

---

Declarations diff (regex)

+ Embedding.degree_eq_of_neighborSet_subset_range
+ degree_map_apply
+ encard_commonNeighbors_top
+ encard_incidenceSet
+ encard_neighborSet
+ ncard_incidenceSet
+ ncard_neighborSet

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 7c6196c).

• +7 new declarations
• −0 removed declarations

+SimpleGraph.Embedding.degree_eq_of_neighborSet_subset_range
+SimpleGraph.degree_map_apply
+SimpleGraph.encard_commonNeighbors_top
+SimpleGraph.encard_incidenceSet
+SimpleGraph.encard_neighborSet
+SimpleGraph.ncard_incidenceSet
+SimpleGraph.ncard_neighborSet

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 7c6196c20f
Reference commit 7c77f1a0a4

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).