feat(SimpleGraph/Trails): in a preconnected Eulerian graph there exists an Eulerian circuit from any vertex

[SnirBroshi]

This lets us take a circuit at a specific vertex, much like IsHamiltonian.exists_isHamiltonianCycle in Hamiltonian graphs.

---

[github-actions]

PR summary c8e4a0d749

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Trails	633	642	+9 (+1.42%)

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.Trails	9

---

Declarations diff (regex)

+ IsEulerian.rotate
+ _root_.SimpleGraph.Preconnected.exists_isEulerian
+ _root_.SimpleGraph.exists_isEulerian_of_mem_support
+ isEulerian_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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit c8e4a0d).

• +5 new declarations
• −0 removed declarations

+SimpleGraph.Preconnected.exists_isEulerian
+SimpleGraph.Walk.IsEulerian.congr_simp
+SimpleGraph.Walk.IsEulerian.rotate
+SimpleGraph.Walk.isEulerian_rotate
+SimpleGraph.exists_isEulerian_of_mem_support

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit c8e4a0d749
Reference commit 80ffd59621

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[vlad902]

Similarly below

Suggested change

	(hp : ∃ (v' : V) (p : G.Walk v' v'), p.IsEulerian) {v : V} (hv : v ∈ G.support) :
	{v v' : V} {p : G.Walk v' v'} (hp : p.IsEulerian) (hv : v ∈ G.support) :

[SnirBroshi]

This is intentional; as the style guide says about this:

We do not enforce one way or the other because providing i explicitly can be harder than proving its existence.

Though I'm not 100% sure about this choice. The unfolded version will let us have dot-notation on IsEulerian, but it means sometimes users of this theorem will have to instead awkward Exists.some/Exists.some_spec. Also the current version makes it clear that v' isn't used in the rest of the statement.
I think it makes sense that these theorems are Exists → Exists.