feat(Combinatorics/SimpleGraph/Walk): lemmas about the first and last darts/edges (#31416)

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -284,7 +284,7 @@ theorem IsAcyclic.isPath_iff_isChain (hG : G.IsAcyclic) {v w : V} (p : G.Walk v
       by_contra hhh
       refine hcc.1 s(u', v') ?_ rfl
       rw [← tail.cons_tail_eq (by simp [not_nil_iff_lt_length, h'])]
-      have := IsPath.mk' this |>.eq_snd_of_mem_edges (by simp [head.ne.symm]) (Sym2.eq_swap ▸ hhh)
+      have := IsPath.mk' this |>.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hhh)
       simp [this, snd_takeUntil head.ne]
 
 theorem IsAcyclic.isPath_iff_isTrail (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) :

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -398,15 +398,16 @@ lemma IsPath.getVert_injOn_iff (p : G.Walk u v) : Set.InjOn p.getVert {i | i ≤
       (by rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero])
     omega
 
-theorem IsPath.eq_snd_of_mem_edges {p : G.Walk u v} (hp : p.IsPath) (hnil : ¬p.Nil)
-    (hmem : s(u, w) ∈ p.edges) : w = p.snd := by
+theorem IsPath.eq_snd_of_mem_edges {p : G.Walk u v} (hp : p.IsPath) (hmem : s(u, w) ∈ p.edges) :
+    w = p.snd := by
+  have hnil := edges_eq_nil.not.mp <| List.ne_nil_of_mem hmem
   rw [← cons_tail_eq _ hnil, edges_cons, List.mem_cons, Sym2.eq, Sym2.rel_iff'] at hmem
   have : u ∉ p.tail.support := by induction p <;> simp_all
   grind [fst_mem_support_of_mem_edges]
 
-theorem IsPath.eq_penultimate_of_mem_edges {p : G.Walk u v} (hp : p.IsPath) (hnil : ¬p.Nil)
+theorem IsPath.eq_penultimate_of_mem_edges {p : G.Walk u v} (hp : p.IsPath)
     (hmem : s(v, w) ∈ p.edges) : w = p.penultimate := by
-  simpa [hnil, hmem] using isPath_reverse_iff p |>.mpr hp |>.eq_snd_of_mem_edges (w := w)
+  simpa [hmem] using isPath_reverse_iff p |>.mpr hp |>.eq_snd_of_mem_edges (w := w)
 
 /-! ### About cycles -/
 

Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean

@@ -239,19 +239,6 @@ theorem map_fst_darts_append {u v : V} (p : G.Walk u v) :
 theorem map_fst_darts {u v : V} (p : G.Walk u v) : p.darts.map (·.fst) = p.support.dropLast := by
   simpa! using congr_arg List.dropLast (map_fst_darts_append p)
 
-@[simp]
-theorem head_darts_fst {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) :
-    (p.darts.head hp).fst = a := by
-  cases p
-  · contradiction
-  · simp
-
-@[simp]
-theorem getLast_darts_snd {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) :
-    (p.darts.getLast hp).snd = b := by
-  rw [← List.getLast_map (f := fun x : G.Dart ↦ x.snd) (by simpa)]
-  simp_rw [p.map_snd_darts, List.getLast_tail, p.getLast_support]
-
 @[simp]
 theorem edges_nil {u : V} : (nil : G.Walk u u).edges = [] := rfl
 
@@ -348,6 +335,14 @@ lemma not_nil_of_ne {p : G.Walk v w} : v ≠ w → ¬ p.Nil := mt Nil.eq
 lemma nil_iff_support_eq {p : G.Walk v w} : p.Nil ↔ p.support = [v] := by
   cases p <;> simp
 
+@[simp]
+lemma darts_eq_nil {p : G.Walk v w} : p.darts = [] ↔ p.Nil := by
+  cases p <;> simp
+
+@[simp]
+lemma edges_eq_nil {p : G.Walk v w} : p.edges = [] ↔ p.Nil := by
+  cases p <;> simp
+
 lemma nil_iff_length_eq {p : G.Walk v w} : p.Nil ↔ p.length = 0 := by
   cases p <;> simp
 

Mathlib/Combinatorics/SimpleGraph/Walks/Traversal.lean

@@ -84,6 +84,7 @@ lemma getVert_cons {u v w n} (p : G.Walk v w) (h : G.Adj u v) (hn : n ≠ 0) :
 theorem getVert_mem_support {u v : V} (p : G.Walk u v) (i : ℕ) : p.getVert i ∈ p.support := by
   induction p generalizing i <;> cases i <;> simp [*]
 
+/-- Use `support_getElem_eq_getVert` to rewrite in the reverse direction. -/
 lemma getVert_eq_support_getElem {u v : V} {n : ℕ} (p : G.Walk u v) (h : n ≤ p.length) :
     p.getVert n = p.support[n]'(p.length_support ▸ Nat.lt_add_one_of_le h) := by
   cases p with
@@ -94,6 +95,11 @@ lemma getVert_eq_support_getElem {u v : V} {n : ℕ} (p : G.Walk u v) (h : n ≤
       simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]
       exact getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)
 
+/-- Use `getVert_eq_support_getElem` to rewrite in the reverse direction. -/
+lemma support_getElem_eq_getVert {u v : V} {n : ℕ} (p : G.Walk u v) (h) :
+    p.support[n]'h = p.getVert n :=
+  (p.getVert_eq_support_getElem <| by grind).symm
+
 lemma getVert_eq_support_getElem? {u v : V} {n : ℕ} (p : G.Walk u v) (h : n ≤ p.length) :
     some (p.getVert n) = p.support[n]? := by
   rw [getVert_eq_support_getElem p h, ← List.getElem?_eq_getElem]
@@ -122,7 +128,9 @@ theorem darts_getElem_eq_getVert {u v : V} {p : G.Walk u v} (n : ℕ) (h : n < p
   ext
   · simp only [p.getVert_eq_support_getElem (le_of_lt h)]
     by_cases h' : n = 0
-    · simp [h', List.getElem_zero]
+    · cases p
+      · contradiction
+      · simp [h']
     · 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]
@@ -140,6 +148,16 @@ lemma snd_cons {u v w} (q : G.Walk v w) (hadj : G.Adj u v) :
 lemma snd_mem_tail_support {u v : V} {p : G.Walk u v} (h : ¬p.Nil) : p.snd ∈ p.support.tail :=
   p.notNilRec (by simp) h
 
+/-- Use `snd_eq_support_getElem_one` to rewrite in the reverse direction. -/
+@[simp]
+lemma support_getElem_one {p : G.Walk u v} (hp) : p.support[1]'hp = p.snd := by
+  grind [getVert_eq_support_getElem]
+
+/-- Use `support_getElem_one` to rewrite in the reverse direction. -/
+lemma snd_eq_support_getElem_one {p : G.Walk u v} (hnil : ¬p.Nil) :
+    p.snd = p.support[1]'(by grind [not_nil_iff_lt_length]) :=
+  support_getElem_one _ |>.symm
+
 /-- The penultimate vertex of a walk, or the only vertex in a nil walk. -/
 abbrev penultimate (p : G.Walk u v) : V := p.getVert (p.length - 1)
 
@@ -164,6 +182,16 @@ lemma adj_penultimate {p : G.Walk v w} (hp : ¬ p.Nil) :
   rw [nil_iff_length_eq] at hp
   convert adj_getVert_succ _ _ <;> omega
 
+lemma penultimate_mem_dropLast_support {p : G.Walk u v} (h : ¬p.Nil) :
+    p.penultimate ∈ p.support.dropLast := by
+  have := adj_penultimate h |>.ne
+  grind [getVert_mem_support, List.dropLast_concat_getLast, getLast_support]
+
+@[simp]
+lemma support_getElem_length_sub_one_eq_penultimate {p : G.Walk u v} :
+    p.support[p.length - 1] = p.penultimate := by
+  grind [getVert_eq_support_getElem]
+
 /-- The first dart of a walk. -/
 @[simps]
 def firstDart (p : G.Walk v w) (hp : ¬ p.Nil) : G.Dart where
@@ -193,6 +221,72 @@ theorem lastDart_eq {p : G.Walk v w} (h₁ : ¬ p.Nil) (h₂ : 0 < p.darts.lengt
   simp (disch := grind) [Dart.ext_iff, lastDart_toProd, darts_getElem_eq_getVert,
     p.getVert_of_length_le]
 
+/-- Use `firstDart_eq_head_darts` to rewrite in the reverse direction. -/
+@[simp]
+theorem head_darts_eq_firstDart {p : G.Walk v w} (hnil : p.darts ≠ []) :
+    p.darts.head hnil = p.firstDart (darts_eq_nil.not.mp hnil) := by
+  grind [firstDart_eq]
+
+/-- Use `head_darts_eq_firstDart` to rewrite in the reverse direction. -/
+theorem firstDart_eq_head_darts {p : G.Walk v w} (hnil : ¬p.Nil) :
+    p.firstDart hnil = p.darts.head (darts_eq_nil.not.mpr hnil) :=
+  head_darts_eq_firstDart _ |>.symm
+
+@[deprecated "Use `head_darts_eq_firstDart`" (since := "2025-12-10")]
+theorem head_darts_fst {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) :
+    (p.darts.head hp).fst = a := by
+  simp
+
+@[simp]
+theorem firstDart_mem_darts {p : G.Walk v w} (hnil : ¬p.Nil) : p.firstDart hnil ∈ p.darts :=
+  p.firstDart_eq_head_darts _ ▸ List.head_mem _
+
+@[simp]
+theorem getLast_darts_eq_lastDart {p : G.Walk v w} (hnil : p.darts ≠ []) :
+    p.darts.getLast hnil = p.lastDart (darts_eq_nil.not.mp hnil) := by
+  grind [lastDart_eq, not_nil_iff_lt_length]
+
+theorem lastDart_eq_getLast_darts {p : G.Walk v w} (hnil : ¬p.Nil) :
+    p.lastDart hnil = p.darts.getLast (darts_eq_nil.not.mpr hnil) := by
+  grind [lastDart_eq, not_nil_iff_lt_length]
+
+@[deprecated "Use `getLast_darts_eq_lastDart`" (since := "2025-12-10")]
+theorem getLast_darts_snd {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) :
+    (p.darts.getLast hp).snd = b := by
+  simp
+
+@[simp]
+theorem lastDart_mem_darts {p : G.Walk v w} (hnil : ¬p.Nil) : p.lastDart hnil ∈ p.darts :=
+  p.lastDart_eq_getLast_darts _ ▸ List.getLast_mem _
+
+/-- Use `mk_start_snd_eq_head_edges` to rewrite in the reverse direction. -/
+@[simp]
+theorem head_edges_eq_mk_start_snd {p : G.Walk v w} (hp) : p.edges.head hp = s(v, p.snd) := by
+  simp [p.edge_firstDart, Walk.edges]
+
+/-- Use `head_edges_eq_mk_start_snd` to rewrite in the reverse direction. -/
+theorem mk_start_snd_eq_head_edges {p : G.Walk v w} (hnil : ¬p.Nil) :
+    s(v, p.snd) = p.edges.head (edges_eq_nil.not.mpr hnil) :=
+  head_edges_eq_mk_start_snd _ |>.symm
+
+theorem mk_start_snd_mem_edges {p : G.Walk v w} (hnil : ¬p.Nil) : s(v, p.snd) ∈ p.edges :=
+  p.mk_start_snd_eq_head_edges hnil ▸ List.head_mem _
+
+/-- Use `mk_penultimate_end_eq_getLast_edges` to rewrite in the reverse direction. -/
+@[simp]
+theorem getLast_edges_eq_mk_penultimate_end {p : G.Walk v w} (hp) :
+    p.edges.getLast hp = s(p.penultimate, w) := by
+  simp [p.edge_lastDart, Walk.edges]
+
+/-- Use `getLast_edges_eq_mk_penultimate_end` to rewrite in the reverse direction. -/
+theorem mk_penultimate_end_eq_getLast_edges {p : G.Walk v w} (hnil : ¬p.Nil) :
+    s(p.penultimate, w) = p.edges.getLast (edges_eq_nil.not.mpr hnil) :=
+  getLast_edges_eq_mk_penultimate_end _ |>.symm
+
+theorem mk_penultimate_end_mem_edges {p : G.Walk v w} (hnil : ¬p.Nil) :
+    s(p.penultimate, w) ∈ p.edges :=
+  p.mk_penultimate_end_eq_getLast_edges hnil ▸ List.getLast_mem _
+
 end Walk
 
 end SimpleGraph