[Merged by Bors] - chore(Combinatorics/SimpleGraph): rename and add gcongr tag to distance lemmas

[Rida-Hamadani]

---

[github-actions]

PR summary ac6beadadb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Reachable.dist_anti
+ edist_anti
- dist_le_subgraph_dist
- edist_le_subgraph_edist

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.

[Rida-Hamadani]

@YaelDillies is it a good idea to tag the dist lemma with gcongr too?

[YaelDillies]

Let's go!

maintainer merge

[github-actions]

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

[b-mehta]

Nice stuff

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[Ruben-VandeVelde]

Deprecated aliases seem to be missing?

[Rida-Hamadani]

@Ruben-VandeVelde Sorry, these lemmas were added recently, and so far only used in an open PR by me which I will edit. Should we add deprecated aliases or is it okay if we leave it this way?