feat(Combinatorics/SimpleGraph): vertices in cycles

[pimotte]

This adds various lemmas on vertices in cycles: Non-equality, and the exact neighbors and size of the neighborSet, along with some smaller supporting lemmas for walks.

In preparation for Tutte's theorem.

---

Zulip thread on Tutte's
Context in my proof of Tutte's

These results are used in the proof to connect IsCycles to IsCycle.

[github-actions]

PR summary e047541f9c

Import changes exceeding 2%

%	File
+25.31%	Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph	561	703	+142 (+25.31%)

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph	142

---

Declarations diff

+ IsCycle.getVert_endpoint_iff
+ IsCycle.getVert_injOn
+ IsCycle.getVert_injOn'
+ IsCycle.getVert_sub_one_neq_getVert_add_one
+ IsCycle.snd_ne_penultimate
+ Nil.tail
+ ncard_neighborSet_toSubgraph_eq_two
+ neighborSet_toSubgraph_endpoint
+ neighborSet_toSubgraph_internal
+ not_nil_of_isCycle_cons
+ not_nil_of_tail_not_nil
+ toSubgraph_adj_penultimate
+ toSubgraph_adj_snd

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

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

[YaelDillies]

Ouch, +142 imports for importing Data.Set.Card. Maybe complain on Zulip that this is a huge price to pay to just write Set.ncard.

Do you think it would make your like any easier if we had a getCycleVert : ℤ → V function that's p.length-periodic? Then you wouldn't have to split cases on whether you are at the endpoint or not. Maybe @kmill has thoughts here too.

[pimotte]

Ouch, +142 imports for importing Data.Set.Card. Maybe complain on Zulip that this is a huge price to pay to just write Set.ncard.

Strictly speaking I'm not just using Set.ncard, but also the result for pairs. There might be something that could be refactored over there, but I'm not sure that would in the end really help here. Between this, #20024 and more results on my backlog I'm also open to starting Combinatorics.SimpleGraph.Card, how do you feel about that?

Do you think it would make your like any easier if we had a getCycleVert : ℤ → V function that's p.length-periodic? Then you wouldn't have to split cases on whether you are at the endpoint or not. Maybe @kmill has thoughts here too.

I think the results in this PR are more or less my way of abstracting the endpoint business, so from my perspective it doesn't help much beyond this. I can see how it would be nice here and give some cleaner results, so I'm not particularly leaning one way or the other. If we decide this is worthwhile I'd be happy to try to whip something up.