refactor(Combinatorics): move Walk from SimpleGraph to HasAdj (and refactor)

[IvanRenison]

The idea for the Walk structure comes from Shreyas4991#1 as suggested in Zulip

---

Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/HasAdj/with/575843445

• depends on: [Merged by Bors] - feat(Data/List): add theorem length_eq_two' #35775
• depends on: feat(Combinatorics): define HasAdj for capturing the common structure of different kinds of (simple) graphs #35776
• depends on: refactor(Combinatorics): move Dart from SimpleGraph to HasAdj #35783

[github-actions]

PR summary 9b809f3970

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
60 files Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.Bipartite Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp Mathlib.Combinatorics.SimpleGraph.Copy Mathlib.Combinatorics.SimpleGraph.Dart Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.DeleteEdges Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.EdgeLabeling Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Extremal.Basic Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity Mathlib.Combinatorics.SimpleGraph.Extremal.Turan Mathlib.Combinatorics.SimpleGraph.Finite Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Combinatorics.SimpleGraph.FiveWheelLike Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Combinatorics.SimpleGraph.Hall Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Combinatorics.SimpleGraph.Maps Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Paths Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Combinatorics.SimpleGraph.Subgraph Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite Mathlib.Combinatorics.SimpleGraph.Tutte Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Combinatorics.SimpleGraph.VertexCover Mathlib.Combinatorics.SimpleGraph.Walks.Basic Mathlib.Combinatorics.SimpleGraph.Walks.Maps Mathlib.Combinatorics.SimpleGraph.Walks.Operations Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks Mathlib.Combinatorics.SimpleGraph.Walks.Traversal	3
Mathlib.Combinatorics.HasAdj.Basic (new file)	214
Mathlib.Combinatorics.HasAdj.Walk (new file)	344
Mathlib.Combinatorics.HasAdj.Dart (new file)	491
Mathlib.Combinatorics.Digraph.HasAdj (new file)	502
Mathlib.Combinatorics.SimpleGraph.HasAdj (new file)	524

---

Declarations diff

+ Adj.left_mem_verts
+ Adj.right_mem_verts
+ HasAdj
+ IsNil
+ IsNil.exist_nil
+ IsNil.head_eq_last
+ IsNil.mem_support_iff_eq_head
+ IsNil.mem_support_iff_eq_last
+ IsNil.support_eq_head
+ IsNil.support_eq_last
+ Walk
+ _root_.HasAdj.Adj.adj_toWalk_head_last
+ _root_.HasAdj.Adj.head_toWalk
+ _root_.HasAdj.Adj.last_toWalk
+ _root_.HasAdj.Adj.length_toWalk
+ _root_.HasAdj.Adj.support_toWalk
+ _root_.HasAdj.Adj.toWalk
+ _root_.HasAdj.Dart.edge_fiber
+ adj_head_last_of_length_eq_one
+ cons
+ exists_eq_cons_of_not_nil
+ ext_iff
+ head
+ head_cons
+ head_eq_last_of_length_eq_zero
+ head_mem_support
+ head_mem_verts
+ head_nil
+ ind
+ instance : HasAdj α (Digraph α)
+ instance : HasAdj α (SimpleGraph α)
+ instance [DecidableEq α] (G : Gr) : DecidableEq (Dart G)
+ isChain_adj_cons_support
+ isNil_nil
+ last
+ last_cons
+ last_mem_support
+ last_mem_verts
+ last_nil
+ length
+ length_cons
+ length_eq_one_iff_support_eq_head_last
+ length_eq_two'
+ length_eq_zero_iff_isNil
+ length_eq_zero_iff_support_eq_singleton
+ length_nil
+ length_pos_ifff_not_nil
+ length_support_pos
+ mem_support_nil_iff
+ nil
+ support_cons
+ support_nil
+ support_nonempty
+ support_subset_support_cons
- Dart.edge_fiber
- Dart.fst_ne_snd
- Dart.snd_ne_fst

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Data/List): add theorem length_eq_two' #35775
• feat(Combinatorics): define HasAdj for capturing the common structure of different kinds of (simple) graphs #35776
• refactor(Combinatorics): move Dart from SimpleGraph to HasAdj #35783
  By Dependent Issues (🤖). Happy coding!

[b-mehta]

I don't think Walk should be changed away from the current inductive definition.

[IvanRenison]

Simply using the recursive version in #35831