feat(Combinatorics/SimpleGraph/Paths): add lemma SimpleGraph.Walk.IsPath.mem_support_iff_exists_append (leanprover-community#27461)

This contribution was created as part of the Utrecht Summerschool "Formalizing Mathematics in Lean" in July 2025.

Author: IvanRenison

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -233,14 +233,21 @@ theorem IsPath.concat {p : G.Walk u v} (hp : p.IsPath) (hw : w ∉ p.support)
     (h : G.Adj v w) : (p.concat h).IsPath :=
   (concat_isPath_iff h).mpr ⟨hp, hw⟩
 
-lemma IsPath.disjoint_support_of_append {u v w : V} {p : G.Walk u v} {q : G.Walk v w}
+lemma IsPath.mem_support_iff_exists_append {p : G.Walk u v} (hp : p.IsPath) :
+    w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), q.IsPath ∧ r.IsPath ∧ p = q.append r := by
+  refine ⟨fun hw ↦ ?_, fun ⟨q, r, hq, hr, hqr⟩ ↦ p.mem_support_iff_exists_append.mpr ⟨q, r, hqr⟩⟩
+  obtain ⟨q, r, hqr⟩ := p.mem_support_iff_exists_append.mp hw
+  have : (q.append r).IsPath := hqr ▸ hp
+  exact ⟨q, r, this.of_append_left, this.of_append_right, hqr⟩
+
+lemma IsPath.disjoint_support_of_append {p : G.Walk u v} {q : G.Walk v w}
     (hpq : (p.append q).IsPath) (hq : ¬q.Nil) : p.support.Disjoint q.tail.support := by
   have hpq' := hpq.support_nodup
   rw [support_append] at hpq'
   rw [support_tail_of_not_nil q hq]
   exact List.disjoint_of_nodup_append hpq'
 
-lemma IsPath.ne_of_mem_support_of_append {u v w : V} {p : G.Walk u v} {q : G.Walk v w}
+lemma IsPath.ne_of_mem_support_of_append {p : G.Walk u v} {q : G.Walk v w}
     (hpq : (p.append q).IsPath) {x y : V} (hyv : y ≠ v) (hx : x ∈ p.support) (hy : y ∈ q.support) :
     x ≠ y := by
   rintro rfl