diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 297353a932b46e..c2ee334d070acb 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -67,6 +67,22 @@ structure IsTree : Prop extends
 
 variable {G G'}
 
+theorem isAcyclic_iff_forall_not_isCycle : G.IsAcyclic ↔ ∀ ⦃v⦄ (c : G.Walk v v), ¬c.IsCycle :=
+  .rfl
+
+theorem isAcyclic_iff_forall_not_isCircuit :
+    G.IsAcyclic ↔ ∀ ⦃v⦄ (c : G.Walk v v), ¬c.IsCircuit := by
+  classical
+  exact ⟨fun h v c hc ↦ h c.cycleBypass hc.isCycle_cycleBypass, fun h v c hc ↦ h c hc.isCircuit⟩
+
+theorem not_isAcyclic_iff_exists_isCycle :
+    ¬G.IsAcyclic ↔ ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
+  simp [isAcyclic_iff_forall_not_isCycle]
+
+theorem not_isAcyclic_iff_exists_isCircuit :
+    ¬G.IsAcyclic ↔ ∃ (v : V) (c : G.Walk v v), c.IsCircuit := by
+  simp [isAcyclic_iff_forall_not_isCircuit]
+
 @[simp] lemma isAcyclic_bot : IsAcyclic (⊥ : SimpleGraph V) := fun _a _w hw ↦ hw.ne_bot rfl
 
 /-- A graph that has an injective homomorphism to an acyclic graph is acyclic. -/
@@ -104,6 +120,22 @@ lemma IsAcyclic.subgraph (h : G.IsAcyclic) (H : G.Subgraph) : H.coe.IsAcyclic :=
 lemma IsAcyclic.anti {G' : SimpleGraph V} (hsub : G ≤ G') (h : G'.IsAcyclic) : G.IsAcyclic :=
   h.comap ⟨_, fun h ↦ hsub h⟩ Function.injective_id
 
+/-- In a non-acyclic graph with finitely-many edges there exists a longest circuit. -/
+theorem exists_isCircuit_forall_isCircuit_length_le_length [Finite G.edgeSet] (h : ¬G.IsAcyclic) :
+    ∃ (v : V) (p : G.Walk v v), p.IsCircuit ∧
+      ∀ v' (p' : G.Walk v' v'), p'.IsCircuit → p'.length ≤ p.length := by
+  have ⟨v₀, p₀, hp₀⟩ := not_isAcyclic_iff_exists_isCircuit.mp h
+  grind [IsCircuit.isTrail, G.exists_isTrail_forall_length_le_of_pred
+    (fun u v p hp ↦ ∃ h : u = v, (h ▸ p).IsCircuit) ⟨v₀, v₀, _, hp₀.isTrail, rfl, hp₀⟩]
+
+/-- In a non-acyclic graph with finitely-many edges there exists a longest cycle. -/
+theorem exists_isCycle_forall_isCycle_length_le_length [Finite G.edgeSet] (h : ¬G.IsAcyclic) :
+    ∃ (v : V) (p : G.Walk v v), p.IsCycle ∧
+      ∀ v' (p' : G.Walk v' v'), p'.IsCycle → p'.length ≤ p.length := by
+  have ⟨v₀, p₀, hp₀⟩ := not_isAcyclic_iff_exists_isCycle.mp h
+  grind [IsCycle.isCircuit, IsCircuit.isTrail, G.exists_isTrail_forall_length_le_of_pred
+    (fun u v p hp ↦ ∃ h : u = v, (h ▸ p).IsCycle) ⟨v₀, v₀, _, hp₀.isTrail, rfl, hp₀⟩]
+
 private lemma Walk.exists_mem_contains_edges_of_directed (Hs : Set <| SimpleGraph V)
     (hHs : Hs.Nonempty) (h_dir : DirectedOn (· ≤ ·) Hs) {u v : V} (p : (sSup Hs).Walk u v) :
     ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet := by
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
index d0cabb0db4a0e8..6fd39981a07184 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
@@ -220,6 +220,26 @@ lemma not_reachable_of_right_degree_zero {G : SimpleGraph V} {u v : V} [Fintype
   rw [reachable_comm]
   exact not_reachable_of_left_degree_zero huv.symm hu
 
+variable {G} in
+/-- In a graph with finitely-many edges, between any reachable endpoints there exists a longest
+trail among trails between them. -/
+theorem Reachable.exists_isTrail_forall_isTrail_length_le_length [Finite G.edgeSet] {u v : V}
+    (huv : G.Reachable u v) :
+    ∃ p : G.Walk u v, p.IsTrail ∧ ∀ p' : G.Walk u v, p'.IsTrail → p'.length ≤ p.length := by
+  have ⟨p₀, hp₀⟩ := huv.exists_isPath
+  grind [G.exists_isTrail_forall_length_le_of_pred (fun u' v' p hp ↦ u' = u ∧ v' = v)
+    ⟨u, v, p₀, hp₀.isTrail, rfl, rfl⟩]
+
+variable {G} in
+/-- In a graph with finitely-many edges, between any reachable endpoints there exists a longest
+path among paths between them. -/
+theorem Reachable.exists_isPath_forall_isPath_length_le_length [Finite G.edgeSet] {u v : V}
+    (huv : G.Reachable u v) :
+    ∃ p : G.Walk u v, p.IsPath ∧ ∀ p' : G.Walk u v, p'.IsPath → p'.length ≤ p.length := by
+  have ⟨p₀, hp₀⟩ := huv.exists_isPath
+  grind [Walk.IsPath.isTrail, G.exists_isTrail_forall_length_le_of_pred
+    (fun u' v' p hp ↦ u' = u ∧ v' = v ∧ p.IsPath) ⟨u, v, p₀, hp₀.isTrail, rfl, rfl, hp₀⟩]
+
 /-- The equivalence relation on vertices given by `SimpleGraph.Reachable`. -/
 @[implicit_reducible]
 def reachableSetoid : Setoid V := Setoid.mk _ G.reachable_is_equivalence
diff --git a/Mathlib/Combinatorics/SimpleGraph/Paths.lean b/Mathlib/Combinatorics/SimpleGraph/Paths.lean
index ada1da35a5daf0..ef8b206e0aef1e 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Paths.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Paths.lean
@@ -366,35 +366,66 @@ theorem IsCycle.isPath_dropLast {p : G.Walk u u} (h : p.IsCycle) : p.dropLast.Is
 theorem IsPath.dropLast (hp : p.IsPath) : p.dropLast.IsPath :=
   hp.take _
 
+variable (G) in
+/-- In a graph with finitely-many edges, for a satisfiable property of trails there exists a longest
+trail satisfying that property. -/
+theorem _root_.SimpleGraph.exists_isTrail_forall_length_le_of_pred [Finite G.edgeSet]
+    (P : ∀ ⦃u v⦄ ⦃p : G.Walk u v⦄, p.IsTrail → Prop)
+    (h : ∃ (u v : V) (p : G.Walk u v) (hp : p.IsTrail), P hp) :
+    ∃ (u v : V) (p : G.Walk u v) (hp : p.IsTrail), P hp ∧
+      ∀ u' v' (p' : G.Walk u' v') (hp' : p'.IsTrail), P hp' → p'.length ≤ p.length := by
+  have := Fintype.ofFinite G.edgeSet
+  let s := {(p.length) | (u : V) (v : V) (p : G.Walk u v) (hp : p.IsTrail) (hp' : P hp)}
+  have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
+    fun n ⟨u, v, p, hp, hp', hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset
+  have ⟨u₀, v₀, p₀, hp₀, hp₀'⟩ := h
+  have ⟨n, hmax⟩ := this.exists_maximal ⟨_, ⟨u₀, v₀, p₀, hp₀, hp₀', rfl⟩⟩
+  obtain ⟨u, v, p, hp, hp', rfl⟩ := hmax.prop
+  exact ⟨u, v, p, hp, hp', (hmax.le ⟨·, ·, ·, ·, ·, rfl⟩)⟩
+
 /-- There exists a trail of maximal length in a non-empty graph on finite edges. -/
-lemma exists_isTrail_forall_isTrail_length_le_length (G : SimpleGraph V) [N : Nonempty V]
-    [Finite G.edgeSet] :
+lemma _root_.SimpleGraph.exists_isTrail_forall_isTrail_length_le_length (G : SimpleGraph V)
+    [Nonempty V] [Finite G.edgeSet] :
     ∃ (u v : V) (p : G.Walk u v) (_ : p.IsTrail),
       ∀ (u' v' : V) (p' : G.Walk u' v') (_ : p'.IsTrail), p'.length ≤ p.length := by
-  have := Fintype.ofFinite G.edgeSet
-  let s := {n | ∃ (u v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
-  have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
-    fun n ⟨_, _, _, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset
-  obtain ⟨x⟩ := N
-  obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩
-  refine ⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩
-  have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩
-  lia
+  have v₀ := Classical.arbitrary V
+  grind [G.exists_isTrail_forall_length_le_of_pred (fun u v p hp ↦ True)
+    ⟨v₀, v₀, nil, .nil, trivial⟩]
+
+@[deprecated (since := "2026-07-08")]
+alias exists_isTrail_forall_isTrail_length_le_length :=
+  exists_isTrail_forall_isTrail_length_le_length
 
 /-- There exists a path of maximal length in a non-empty graph on finite edges. -/
-lemma exists_isPath_forall_isPath_length_le_length (G : SimpleGraph V) [N : Nonempty V]
-    [Finite G.edgeSet] :
+lemma _root_.SimpleGraph.exists_isPath_forall_isPath_length_le_length (G : SimpleGraph V)
+    [Nonempty V] [Finite G.edgeSet] :
     ∃ (u v : V) (p : G.Walk u v) (_ : p.IsPath),
       ∀ (u' v' : V) (p' : G.Walk u' v') (_ : p'.IsPath), p'.length ≤ p.length := by
-  have := Fintype.ofFinite G.edgeSet
-  let s := {n | ∃ (u v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
-  have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
-    fun n ⟨_, _, _, hp, hn⟩ ↦ hn ▸ hp.isTrail.length_le_card_edgeFinset
-  obtain ⟨x⟩ := N
-  obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩
-  refine ⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩
-  have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩
-  lia
+  have v₀ := Classical.arbitrary V
+  grind [IsPath.isTrail, G.exists_isTrail_forall_length_le_of_pred (fun u v p hp ↦ p.IsPath)
+    ⟨v₀, v₀, nil, .nil, .nil⟩]
+
+@[deprecated (since := "2026-07-08")]
+alias exists_isPath_forall_isPath_length_le_length := exists_isPath_forall_isPath_length_le_length
+
+variable (G) in
+/-- In a graph with finitely-many edges, from any start vertex there exists a longest trail among
+trails from that vertex. -/
+theorem _root_.SimpleGraph.exists_isTrail_forall_isTrail_length_le_length' [Finite G.edgeSet]
+    (u : V) :
+    ∃ (v : V) (p : G.Walk u v), p.IsTrail ∧
+      ∀ v' (p' : G.Walk u v'), p'.IsTrail → p'.length ≤ p.length := by
+  grind [G.exists_isTrail_forall_length_le_of_pred (fun u' v p hp ↦ u' = u) ⟨u, u, nil, .nil, rfl⟩]
+
+variable (G) in
+/-- In a graph with finitely-many edges, from any start vertex there exists a longest path among
+paths from that vertex. -/
+theorem _root_.SimpleGraph.exists_isPath_forall_isPath_length_le_length' [Finite G.edgeSet]
+    (u : V) :
+    ∃ (v : V) (p : G.Walk u v), p.IsPath ∧
+      ∀ v' (p' : G.Walk u v'), p'.IsPath → p'.length ≤ p.length := by
+  grind [IsPath.isTrail, G.exists_isTrail_forall_length_le_of_pred
+    (fun u' v p hp ↦ u' = u ∧ p.IsPath) ⟨u, u, nil, .nil, rfl, .nil⟩]
 
 /-! ### About paths -/
 
@@ -970,6 +1001,29 @@ lemma IsTrail.isCycle_cycleBypass {w : G.Walk v v} (hw : w ≠ .nil) (hw' : w.Is
 
 end Walk
 
+variable {G} in
+/-- In a graph with finitely-many edges and a circuit containing a vertex, there exists a longest
+circuit among circuits containing that vertex. -/
+theorem exists_isCircuit_forall_isCircuit_length_le_length' [Finite G.edgeSet] {v : V}
+    (h : ∃ p : G.Walk v v, p.IsCircuit) :
+    ∃ p : G.Walk v v, p.IsCircuit ∧ ∀ p' : G.Walk v v, p'.IsCircuit → p'.length ≤ p.length := by
+  have ⟨p₀, hp₀⟩ := h
+  grind [Walk.IsCircuit.isTrail, G.exists_isTrail_forall_length_le_of_pred
+    (fun u' v' p hp ↦ u' = v ∧ v' = v ∧ ∃ h : u' = v', (h ▸ p).IsCircuit)
+    ⟨v, v, p₀, hp₀.isTrail, rfl, rfl, rfl, hp₀⟩]
+
+variable {G} in
+/-- In a graph with finitely-many edges and a circuit containing a vertex, there exists a longest
+cycle among cycles containing that vertex. -/
+theorem exists_isCycle_forall_isCycle_length_le_length' [Finite G.edgeSet] {v : V}
+    (h : ∃ p : G.Walk v v, p.IsCircuit) :
+    ∃ p : G.Walk v v, p.IsCycle ∧ ∀ p' : G.Walk v v, p'.IsCycle → p'.length ≤ p.length := by
+  have ⟨p₀, hp₀⟩ := h
+  classical
+  grind [Walk.IsCycle.isCircuit, Walk.IsCircuit.isTrail, G.exists_isTrail_forall_length_le_of_pred
+    (fun u' v' p hp ↦ u' = v ∧ v' = v ∧ ∃ h : u' = v', (h ▸ p).IsCycle)
+    ⟨v, v, _, hp₀.isCycle_cycleBypass.isTrail, rfl, rfl, rfl, hp₀.isCycle_cycleBypass⟩]
+
 /-! ### Mapping paths -/
 
 namespace Walk