From 1450ccebb122e41d67d49d561cb07c4a444d711b Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Tue, 14 Jul 2026 01:23:21 +0300
Subject: [PATCH] feat(Combinatorics/SimpleGraph/Paths): existence of a
 shortest cycle at a vertex

---
 Mathlib/Combinatorics/SimpleGraph/Paths.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Paths.lean b/Mathlib/Combinatorics/SimpleGraph/Paths.lean
index ada1da35a5daf0..141e29bb3c9f99 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Paths.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Paths.lean
@@ -968,6 +968,20 @@ lemma IsTrail.isCycle_cycleBypass {w : G.Walk v v} (hw : w ≠ .nil) (hw' : w.Is
     w.cycleBypass.IsCycle :=
   (w.isCircuit_def.mpr ⟨hw', hw⟩).isCycle_cycleBypass
 
+omit [DecidableEq V] in
+/-- For every vertex that lies on some circuit there exists a shortest cycle among circuits
+containing that vertex.
+
+For circuits not fixed to a specific vertex use `exists_girth_eq_length` and
+`IsCircuit.girth_le_length`. -/
+theorem exists_isCycle_forall_isCircuit_length_le_length {v : V}
+    (h : ∃ p : G.Walk v v, p.IsCircuit) :
+    ∃ p : G.Walk v v, p.IsCycle ∧ ∀ p' : G.Walk v v, p'.IsCircuit → p.length ≤ p'.length := by
+  have ⟨p, hmin⟩ := exists_minimalFor_of_wellFoundedLT IsCircuit length h
+  classical
+  refine ⟨p.cycleBypass, hmin.prop.isCycle_cycleBypass, fun p' hp' ↦ ?_⟩
+  grw [p.length_cycleBypass_le_length, hmin.le hp']
+
 end Walk
 
 /-! ### Mapping paths -/