feat(SimpleGraph): relate takeUntil/dropUntil to take/drop (leanprover-community#34620)

Add lemmas to allow going from takeUntil/dropUntil to a take/drop in terms of an explicit index `p.support.idxOf w`.

Author: vlad902

Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

@@ -57,6 +57,24 @@ lemma takeUntil_first (p : G.Walk u v) :
 lemma nil_takeUntil (p : G.Walk u v) (hwp : w ∈ p.support) :
     (p.takeUntil w hwp).Nil ↔ u = w := ⟨Nil.eq, (by cases ·; simp)⟩
 
+lemma takeUntil_eq_take (p : G.Walk u v) (h : w ∈ p.support) :
+    p.takeUntil w h = (p.take <| p.support.idxOf w).copy rfl (p.getVert_support_idxOf h) := by
+  apply ext_support
+  induction p with
+  | nil =>
+    simp only [takeUntil, eq_mpr_eq_cast, support_nil, getVert_nil, take, support_copy]
+    grind [mem_support_nil_iff, support_nil]
+  | @cons a _ _ _ p ih =>
+    by_cases! h' : w = a
+    · grind [List.idxOf_cons_self, take_zero, copy_rfl_rfl, support_nil, takeUntil_first]
+    · rw [take_cons_eq _ _ _ (by grind), takeUntil_cons (List.mem_of_ne_of_mem h' h) h'.symm,
+        support_cons, support_copy, ih (by grind)]
+      grind
+
+lemma length_takeUntil (p : G.Walk u v) (h : w ∈ p.support) :
+    (p.takeUntil w h).length = p.support.idxOf w := by
+  simp [takeUntil_eq_take, Nat.le_iff_lt_add_one, ← length_support, List.idxOf_lt_length_of_mem h]
+
 /-- Given a vertex in the support of a path, give the path from (and including) that vertex to
 the end. In other words, drop vertices from the front of a path until (and not including)
 that vertex. -/
@@ -85,6 +103,29 @@ theorem take_spec {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
     · simp! only
       split_ifs with h' <;> subst_vars <;> simp [*]
 
+@[simp]
+lemma dropUntil_first (p : G.Walk u v) (h : u ∈ p.support) : p.dropUntil u h = p := by
+  unfold dropUntil
+  split <;> simp
+
+lemma dropUntil_eq_drop (p : G.Walk u v) (h : w ∈ p.support) :
+    p.dropUntil w h = (p.drop <| p.support.idxOf w).copy (p.getVert_support_idxOf h) rfl := by
+  apply ext_support
+  induction p with
+  | nil =>
+    simp only [dropUntil, eq_mpr_eq_cast, support_nil, getVert_nil, drop, support_copy]
+    grind [mem_support_nil_iff, support_nil]
+  | @cons a _ _ _ p ih =>
+    by_cases! h' : w = a
+    · subst h'
+      simp [dropUntil_first, drop_support_eq_support_drop_min]
+    · rw [drop_cons_eq _ _ _ (by grind), support_copy, dropUntil]
+      grind
+
+lemma length_dropUntil (p : G.Walk u v) (h : w ∈ p.support) :
+    (p.dropUntil w h).length = p.length - p.support.idxOf w := by
+  simp [dropUntil_eq_drop]
+
 theorem isSubwalk_takeUntil (p : G.Walk u v) (h : w ∈ p.support) : (p.takeUntil w h).IsSubwalk p :=
   ⟨nil, p.dropUntil w h, by simp⟩
 

Mathlib/Combinatorics/SimpleGraph/Walks/Operations.lean

@@ -524,6 +524,13 @@ lemma drop_add_eq (p : G.Walk u v) (n m : ℕ) :
 lemma nil_drop_iff (p : G.Walk u v) (n : ℕ) : (p.drop n).Nil ↔ p.length ≤ n := by
   induction p generalizing n <;> cases n <;> simp [*, drop]
 
+lemma drop_cons_eq (h : G.Adj u v) (p : G.Walk v w) (n : ℕ) (hn : n ≠ 0) :
+    (cons h p).drop n = (p.drop (n - 1)).copy (p.getVert_cons h hn).symm rfl := by
+  apply ext_support
+  obtain ⟨_, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.ne_zero_iff_zero_lt.mp hn)
+  conv_lhs => unfold drop
+  simp
+
 lemma darts_drop (p : G.Walk u v) (n : ℕ) : (p.drop n).darts = p.darts.drop n := by
   induction p generalizing n <;> cases n <;> simp [*, drop]
 
@@ -576,6 +583,11 @@ lemma take_of_length_le {u v n} {p : G.Walk u v} (h : p.length ≤ n) :
     rw [length_cons, Nat.add_le_add_iff_right] at h
     simp [take, ih h]
 
+lemma take_cons_eq (h : G.Adj u v) (p : G.Walk v w) (n : ℕ) (hn : n ≠ 0) :
+    (cons h p).take n = cons h ((p.take <| n - 1).copy rfl (p.getVert_cons h hn).symm) := by
+  apply ext_support
+  grind [support_copy, take_support_eq_support_take_succ]
+
 lemma darts_take (p : G.Walk u v) (n : ℕ) : (p.take n).darts = p.darts.take n := by
   induction p generalizing n <;> cases n <;> simp [*, take]
 

Mathlib/Combinatorics/SimpleGraph/Walks/Traversal.lean

@@ -110,6 +110,11 @@ lemma getVert_eq_getD_support {u v : V} (p : G.Walk u v) (n : ℕ) :
   · simp [← getVert_eq_support_getElem? p h]
   grind [getVert_of_length_le, length_support]
 
+@[simp]
+lemma getVert_support_idxOf [DecidableEq V] (p : G.Walk u v) (h : w ∈ p.support) :
+    p.getVert (p.support.idxOf w) = w := by
+  grind [getVert_eq_support_getElem]
+
 theorem getVert_comp_val_eq_get_support {u v : V} (p : G.Walk u v) :
     p.getVert ∘ Fin.val = p.support.get := by
   grind [getVert_eq_support_getElem, length_support]