feat(SimpleGraph): lemmas relating edges and darts to the support (#26720)

Useful lemmas to make it easier to pass between the support/edges/darts of a walk.

- [x] depends on: #25812

Author: vlad902

Mathlib/Combinatorics/SimpleGraph/Walk.lean

@@ -824,6 +824,23 @@ theorem nodup_tail_support_reverse {u : V} {p : G.Walk u u} :
     ← getVert_eq_support_getElem? _ (by rw [Walk.length_support]; cutsat)]
   aesop
 
+theorem edges_eq_zipWith_support {u v : V} {p : G.Walk u v} :
+    p.edges = List.zipWith (s(·, ·)) p.support p.support.tail := by
+  induction p with
+  | nil => simp
+  | cons _ p' ih => cases p' <;> simp [edges_cons, ih]
+
+theorem darts_getElem_eq_getVert {u v : V} {p : G.Walk u v} (n : ℕ) (h : n < p.darts.length) :
+    p.darts[n] = ⟨⟨p.getVert n, p.getVert (n + 1)⟩, p.adj_getVert_succ (p.length_darts ▸ h)⟩ := by
+  rw [p.length_darts] at h
+  ext
+  · simp only [p.getVert_eq_support_getElem (le_of_lt h)]
+    by_cases h' : n = 0
+    · simp [h', List.getElem_zero]
+    · have := p.isChain_dartAdj_darts.getElem (n - 1) (by grind)
+      grind [DartAdj, =_ cons_map_snd_darts]
+  · simp [p.getVert_eq_support_getElem h, ← p.cons_map_snd_darts]
+
 theorem edges_injective {u v : V} : Function.Injective (Walk.edges : G.Walk u v → List (Sym2 V))
   | .nil, .nil, _ => rfl
   | .nil, .cons _ _, h => by simp at h
@@ -1103,6 +1120,15 @@ lemma edge_firstDart (p : G.Walk v w) (hp : ¬ p.Nil) :
 lemma edge_lastDart (p : G.Walk v w) (hp : ¬ p.Nil) :
     (p.lastDart hp).edge = s(p.penultimate, w) := rfl
 
+theorem firstDart_eq {p : G.Walk v w} (h₁ : ¬ p.Nil) (h₂ : 0 < p.darts.length) :
+    p.firstDart h₁ = p.darts[0] := by
+  simp [Dart.ext_iff, firstDart_toProd, darts_getElem_eq_getVert]
+
+theorem lastDart_eq {p : G.Walk v w} (h₁ : ¬ p.Nil) (h₂ : 0 < p.darts.length) :
+    p.lastDart h₁ = p.darts[p.darts.length - 1] := by
+  simp (disch := grind) [Dart.ext_iff, lastDart_toProd, darts_getElem_eq_getVert,
+    p.getVert_of_length_le]
+
 lemma cons_tail_eq (p : G.Walk u v) (hp : ¬ p.Nil) :
     cons (p.adj_snd hp) p.tail = p := by
   cases p with
@@ -1556,3 +1582,5 @@ lemma isSubwalk_antisymm {u v} {p₁ p₂ : G.Walk u v} (h₁ : p₁.IsSubwalk p
 end Walk
 
 end SimpleGraph
+
+set_option linter.style.longFile 1700