feat(Combinatorics/SimpleGraph/Hasse): Define the Eulerian path of a path graph

[SnirBroshi]

---

Such statements are left for a future PR, since they add imports so we probably want to split them into a separate file:

theorem IsEulerian.ofPathGraph : ofPathGraph n |>.IsEulerian := by sorry
theorem IsHamiltonian.ofPathGraph : ofPathGraph n |>.IsHamiltonian := by sorry

theorem exists_path_iff_isContained_pathGraph :
    (∃ (u v : V) (w : G.Path u v), w.val.support.length = n) ↔ pathGraph n ⊑ G := by
  sorry

(the last statement also requires #33121, this PR gives the right-to-left implication and that PR gives the left-to-right)

[github-actions]

PR summary 5908048297

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Embedding.hasse
+ IsPath.ofPathGraph
+ length_ofPathGraph
+ ofPathGraph
+ support_ofPathGraph

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.

---

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

[vlad902]

I don't think this belongs in the IsPath namespace.

Suggested change

	theorem IsPath.ofPathGraph : ofPathGraph n |>.IsPath :=
	theorem isPath_ofPathGraph : ofPathGraph n |>.IsPath :=

[SnirBroshi]

I disagree, path graphs are very related to IsPath and this allows for dot notation when the expected type is IsPath

[vlad902]

I'm not sure I follow, how can dot notation be used here when IsPath is the conclusion rather than a hypothesis?

[SnirBroshi]

Here's a straightforward example:

def myPath : (pathGraph 3).Path 0 2 := ⟨.ofPathGraph _, .ofPathGraph _⟩

and here's a slightly less trivial example that might occur "in the wild":

namespace SimpleGraph

theorem IsAcyclic.pathGraph (n : ℕ) : (pathGraph n).IsAcyclic := sorry

theorem foo : s(0, 1) ∈ (Walk.ofPathGraph 1).edges := by
  have := IsAcyclic.path_concat
    (.pathGraph 2)
    (.takeUntil (.ofPathGraph 1) (u := 0) (by simp))
    (.ofPathGraph 1)
    (by grind [pathGraph_adj, CovBy])
    (by simp)
  rw [this]
  simp

end SimpleGraph

[vlad902]

This still feels backwards to me, where I would flip the names, e.g. ofPathGraph.isPath instead and maybe make n implicit, but yeah I'm happy to let the reviewers judge--I don't feel like I have a good enough feel for API design.

[vihdzp]

I've seen this pattern before, I have no qualms with it.