feat(Combinatorics/SimpleGraph/Walk/Paths): a trail which isn't a path has a cycle subwalk (#39061)

- `p.IsPath ↔ ∀ (v : V) (w : G.Walk v v), w.IsSubwalk p → w.Nil`
- `p.IsTrail → (p.IsPath ↔ ∀ (v : V) (w : G.Walk v v), w.IsSubwalk p → ¬w.IsCycle)`

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

@@ -505,7 +505,7 @@ lemma exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty (s : Finset V)
     have := p.length_takeUntil_le hx
     lia
   obtain ⟨y, hys, hyp, h⟩ := ih _ this (s.erase x) h rfl
-  use y, mem_of_mem_erase hys, support_takeUntil_subset p hx hyp
+  use y, mem_of_mem_erase hys, support_takeUntil_subset_support p hx hyp
   rwa [takeUntil_takeUntil, erase_right_comm, filter_erase, erase_eq_of_notMem] at h
   simp only [mem_filter, mem_erase, ne_eq, not_and, and_imp]
   rintro hxy -

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -612,6 +612,30 @@ lemma endpoint_notMem_support_takeUntil {p : G.Walk u v} (hp : p.IsPath) (hw : w
 
 end WalkDecomp
 
+theorem isPath_iff_isSubwalk_imp_nil {u v} {p : G.Walk u v} :
+    p.IsPath ↔ ∀ (v : V) (w : G.Walk v v), w.IsSubwalk p → w.Nil := by
+  refine ⟨fun hp v w hwp ↦ ?_, fun h ↦ .mk' ?_⟩
+  · simp [w.isPath_iff_eq_nil.mp <| isPath_of_isSubwalk hwp hp]
+  · refine List.pairwise_iff_getElem.mpr fun i j _ _ _ _ ↦ ?_
+    let p' := p.take j |>.drop i
+    have : ¬p'.Nil := by grind [nil_drop_iff, take_length]
+    have : p'.IsSubwalk p := isSubwalk_drop _ i |>.trans <| p.isSubwalk_take j
+    grind [take_getVert, getVert_eq_support_getElem]
+
+theorem IsTrail.isPath_iff_isSubwalk_imp_not_isCycle {u v} {p : G.Walk u v} (ht : p.IsTrail) :
+    p.IsPath ↔ ∀ (v : V) (w : G.Walk v v), w.IsSubwalk p → ¬w.IsCycle := by
+  refine ⟨by grind [isPath_iff_isSubwalk_imp_nil, IsCycle.not_nil], fun h ↦ ?_⟩
+  classical
+  match p with
+  | .nil => simp
+  | .cons hadj p =>
+    have hp := isPath_iff_isSubwalk_imp_not_isCycle ht.of_cons |>.mpr (h · · <| ·.cons hadj)
+    refine cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩
+    · rw [isSubwalk_iff_support_isInfix, support_cons, support_cons]
+      exact (List.prefix_cons_inj u |>.mpr <| p.support_takeUntil_prefix_support hup).isInfix
+    · refine cons_isCycle_iff .. |>.mpr ⟨hp.takeUntil hup, fun he ↦ ?_⟩
+      exact ht.edges_nodup.notMem <| p.edges_takeUntil_subset hup he
+
 end Walk
 
 /-! ### Type of paths -/

Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean

@@ -185,11 +185,18 @@ theorem dropUntil_copy {u v w v' w'} (p : G.Walk v w) (hv : v = v') (hw : w = w'
   subst_vars
   rfl
 
-theorem support_takeUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
+theorem support_takeUntil_prefix_support (p : G.Walk v w) (h : u ∈ p.support) :
+    (p.takeUntil u h).support <+: p.support := by
+  grw [takeUntil_eq_take, support_copy, take_support_eq_support_take_succ, List.take_prefix]
+
+theorem support_takeUntil_subset_support {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
     (p.takeUntil u h).support ⊆ p.support := fun x hx => by
   rw [← take_spec p h, mem_support_append_iff]
   exact Or.inl hx
 
+@[deprecated (since := "2026-05-25")]
+alias support_takeUntil_subset := support_takeUntil_subset_support
+
 theorem support_dropUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
     (p.dropUntil u h).support ⊆ p.support := fun x hx => by
   rw [← take_spec p h, mem_support_append_iff]
@@ -270,12 +277,13 @@ lemma length_takeUntil_lt {u v w : V} {p : G.Walk v w} (h : u ∈ p.support) (hu
 
 lemma takeUntil_takeUntil {w x : V} (p : G.Walk u v) (hw : w ∈ p.support)
     (hx : x ∈ (p.takeUntil w hw).support) :
-    (p.takeUntil w hw).takeUntil x hx = p.takeUntil x (p.support_takeUntil_subset hw hx) := by
+    (p.takeUntil w hw).takeUntil x hx =
+      p.takeUntil x (p.support_takeUntil_subset_support hw hx) := by
   simp_rw [← takeUntil_append_of_mem_left _ (p.dropUntil w hw) hx, take_spec]
 
 lemma notMem_support_takeUntil_support_takeUntil_subset {p : G.Walk u v} {w x : V} (h : x ≠ w)
     (hw : w ∈ p.support) (hx : x ∈ (p.takeUntil w hw).support) :
-    w ∉ (p.takeUntil x (p.support_takeUntil_subset hw hx)).support := by
+    w ∉ (p.takeUntil x (p.support_takeUntil_subset_support hw hx)).support := by
   rw [← takeUntil_takeUntil p hw hx]
   intro hw'
   have h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length