feat(Combinatorics/SimpleGraph/Walk): relate edges and darts (leanprover-community#41720)

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

@@ -281,42 +281,18 @@ theorem toSubgraph_adj_penultimate {u v} (w : G.Walk u v) (h : ¬ w.Nil) :
   simpa [show w.length - 1 + 1 = w.length by lia]
     using w.toSubgraph_adj_getVert (by lia : w.length - 1 < w.length)
 
+lemma adj_toSubgraph_iff_mem_edges {u v u' v' : V} {p : G.Walk u v} :
+    p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.edges := by
+  rw [← mem_edges_toSubgraph, Subgraph.mem_edgeSet]
+
 theorem toSubgraph_adj_iff {u v u' v'} (w : G.Walk u v) :
     w.toSubgraph.Adj u' v' ↔ ∃ i, s(w.getVert i, w.getVert (i + 1)) =
       s(u', v') ∧ i < w.length := by
-  constructor
-  · intro hadj
-    unfold Walk.toSubgraph at hadj
-    match w with
-    | .nil =>
-      simp only [singletonSubgraph_adj, Pi.bot_apply, Prop.bot_eq_false] at hadj
-    | .cons h p =>
-      simp only [Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
-        Prod.swap_prod_mk] at hadj
-      cases hadj with
-      | inl hl =>
-        use 0
-        simp only [Walk.getVert_zero, zero_add, getVert_cons_succ]
-        refine ⟨?_, by simp only [length_cons, Nat.zero_lt_succ]⟩
-        exact Sym2.eq_iff.mpr hl
-      | inr hr =>
-        obtain ⟨i, hi⟩ := (toSubgraph_adj_iff _).mp hr
-        use i + 1
-        simp only [getVert_cons_succ]
-        constructor
-        · exact hi.1
-        · simp only [Walk.length_cons, Nat.add_lt_add_right hi.2 1]
-  · rintro ⟨i, hi⟩
-    rw [← Subgraph.mem_edgeSet, ← hi.1, Subgraph.mem_edgeSet]
-    exact toSubgraph_adj_getVert _ hi.2
+  grind [adj_toSubgraph_iff_mem_edges, mk_mem_edges_iff_exists]
 
 lemma mem_support_of_adj_toSubgraph {u v u' v' : V} {p : G.Walk u v} (hp : p.toSubgraph.Adj u' v') :
     u' ∈ p.support := p.mem_verts_toSubgraph.mp (p.toSubgraph.edge_vert hp)
 
-lemma adj_toSubgraph_iff_mem_edges {u v u' v' : V} {p : G.Walk u v} :
-    p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.edges := by
-  rw [← p.mem_edges_toSubgraph, Subgraph.mem_edgeSet]
-
 theorem toSubgraph_le_iff {w : G.Walk u v} (hnil : ¬w.Nil) {G' : G.Subgraph} :
     w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet := by
   refine ⟨fun hw e he ↦ Subgraph.edgeSet_mono hw <| w.mem_edges_toSubgraph.mpr he, fun hw ↦ ?_⟩

Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean

@@ -125,6 +125,9 @@ def darts {u v : V} : G.Walk u v → List G.Dart
 This is defined to be the list of edges underlying `SimpleGraph.Walk.darts`. -/
 def edges {u v : V} (p : G.Walk u v) : List (Sym2 V) := p.darts.map Dart.edge
 
+theorem edges_eq_map_darts (p : G.Walk u v) : p.edges = p.darts.map Dart.edge :=
+  rfl
+
 @[simp]
 theorem support_nil {u : V} : (nil : G.Walk u u).support = [u] := rfl
 
@@ -253,6 +256,16 @@ theorem length_darts {u v : V} (p : G.Walk u v) : p.darts.length = p.length := b
 @[simp, grind =]
 theorem length_edges {u v : V} (p : G.Walk u v) : p.edges.length = p.length := by simp [edges]
 
+/-- Use `edge_getElem_darts` to rewrite in the reverse direction. -/
+theorem getElem_edges_eq_edge_getElem_darts {p : G.Walk u v} {i : ℕ} (h : i < p.edges.length) :
+    p.edges[i] = (p.darts[i]'(by grind)).edge :=
+  List.getElem_map ..
+
+/-- Use `getElem_edges_eq_edge_getElem_darts` to rewrite in the reverse direction. -/
+theorem edge_getElem_darts {p : G.Walk u v} {i : ℕ} (h : i < p.darts.length) :
+    p.darts[i].edge = p.edges[i]'(by grind) := by
+  rw [getElem_edges_eq_edge_getElem_darts]
+
 @[simp]
 theorem fst_darts_getElem {p : G.Walk u v} {i : ℕ} (hi : i < p.darts.length) :
     p.darts[i].fst = p.support.dropLast[i]'(by grind) := by

Mathlib/Combinatorics/SimpleGraph/Walk/Traversal.lean

@@ -129,6 +129,14 @@ theorem darts_getElem_eq_getVert {u v : V} {p : G.Walk u v} (n : ℕ) (h : n < p
   rw [p.length_darts] at h
   ext <;> simp [p.getVert_eq_support_getElem (le_of_lt h), p.getVert_eq_support_getElem h]
 
+theorem getElem_edges {p : G.Walk u v} {i : ℕ} (h : i < p.edges.length) :
+    p.edges[i] = s(p.getVert i, p.getVert (i + 1)) := by
+  simp [getElem_edges_eq_edge_getElem_darts, darts_getElem_eq_getVert]
+
+theorem mk_mem_edges_iff_exists {u' v' : V} (p : G.Walk u v) :
+    s(u', v') ∈ p.edges ↔ ∃ i < p.length, s(p.getVert i, p.getVert (i + 1)) = s(u', v') := by
+  constructor <;> grind [getElem_edges, List.mem_iff_getElem]
+
 theorem adj_of_infix_support {u v u' v'} {p : G.Walk u v} (h : [u', v'] <:+: p.support) :
     G.Adj u' v' := by
   have ⟨k, hk, h⟩ := List.infix_iff_getElem?.mp h