feat(Combinatorics/SimpleGraph/Walk): make p.Nil the simpNF of p = nil and p.length = 0

[SnirBroshi]

These are equivalent, and p.Nil works even when the endpoints of the walk aren't defeq.

The main event is Walk/Basic.lean:

• Swapped sides of nil_iff_eq_nil to create eq_nil_iff_nil, tagged @[simp] and deprecated the original
• Changed the RHS of length_eq_zero_iff from p = nil to p.Nil, and generalized to non-closed walks
• Deprecated nil_iff_length_eq which is the symmetric iff
• Added Nil.length_eq_zero alias
• Untagged exists_length_eq_zero_iff with @[simp] and added exists_nil_iff to replace it

The rest is fixing everything that broke (or uses of now-deprecated lemmas), and:

• [Walk/Maps] Added nil_map_iff to replace map_eq_nil_iff which is the same but with .Nil instead of = nil
• [Walk/Decomp] Added nil_rotate to replace rotate_eq_nil which is the same but with .Nil instead of = nil

---

Also renamed set_walk_* in Counting.lean to follow the naming convention.

[github-actions]

PR summary 686c76b39d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Nil.length_eq_zero
+ Walk.setOf_length_eq_add_one
+ Walk.setOf_length_eq_zero
+ Walk.setOf_length_eq_zero_of_ne
+ eq_nil_iff_nil
+ exists_nil_iff
+ nil_map_iff
+ nil_rotate

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.