Refactoring the graph theory library

Stream: mathlib4

[Jeremy Tan]

I have already made some PRs splitting the monolithic Combinatorics.SimpleGraph.Basic into smaller pieces. #10123 continues that by splitting out "finite" parts; would like review/merge.

Later on I plan to split .Connectivity into its several concepts of walk, trail, path and cycle.

[Jeremy Tan]

(But I can't do the latter now because the former will change the dependencies substantially)

[Yury G. Kudryashov]

Please tag the authors of the files you're splitting.

[Jeremy Tan]

@Kyle Miller :up: @Aaron Anderson @Alena Gusakov

[Jeremy Tan]

#10312 continues the refactor by splitting out darts @Kyle Miller

[Jeremy Tan]

#10329 is the big one!

[Jeremy Tan]

@Kyle Miller :up: