From a5a091ea3c3bf8892701fe6d2122f78addeb22bc Mon Sep 17 00:00:00 2001 From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> Date: Thu, 9 Jul 2026 05:41:14 +0300 Subject: [PATCH 1/3] feat(Combinatorics/SimpleGraph/Paths): existence of longest paths/trails/cycles/circuits --- .../Combinatorics/SimpleGraph/Acyclic.lean | 42 ++++++++++ .../SimpleGraph/Connectivity/Connected.lean | 30 ++++++++ Mathlib/Combinatorics/SimpleGraph/Paths.lean | 76 ++++++++++++++++++- 3 files changed, 144 insertions(+), 4 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean index 297353a932b46e..08638f946dc06b 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,32 @@ 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 + let s := {(p.length) | (v : V) (p : G.Walk v v) (hp : p.IsCircuit)} + have := Fintype.ofFinite G.edgeSet + have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) + fun n ⟨v, p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset + have ⟨v, p₀, hp₀⟩ := not_isAcyclic_iff_exists_isCircuit.mp h + have ⟨n, hmax⟩ := this.exists_maximal ⟨_, ⟨v, p₀, hp₀, rfl⟩⟩ + obtain ⟨v, p, hp, rfl⟩ := hmax.prop + exact ⟨v, p, hp, (hmax.le ⟨·, ·, ·, rfl⟩)⟩ + +/-- 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 + let s := {(p.length) | (v : V) (p : G.Walk v v) (hp : p.IsCycle)} + have := Fintype.ofFinite G.edgeSet + have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) + fun n ⟨v, p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset + have ⟨v, p₀, hp₀⟩ := not_isAcyclic_iff_exists_isCycle.mp h + have ⟨n, hmax⟩ := this.exists_maximal ⟨_, ⟨v, p₀, hp₀, rfl⟩⟩ + obtain ⟨v, p, hp, rfl⟩ := hmax.prop + exact ⟨v, p, hp, (hmax.le ⟨·, ·, ·, rfl⟩)⟩ + 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..2d38d331979dc2 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean @@ -220,6 +220,36 @@ 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 + let s := {(p.length) | (p : G.Walk u v) (hp : p.IsTrail)} + have := Fintype.ofFinite G.edgeSet + have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) + fun n ⟨p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset + have ⟨p₀, hp₀⟩ := huv.exists_isPath + have ⟨n, hmax⟩ := this.exists_maximal ⟨_, ⟨p₀, hp₀.isTrail, rfl⟩⟩ + obtain ⟨p, hp, rfl⟩ := hmax.prop + exact ⟨p, hp, (hmax.le ⟨·, ·, 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 + let s := {(p.length) | (p : G.Walk u v) (hp : p.IsPath)} + have := Fintype.ofFinite G.edgeSet + have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) + fun n ⟨p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset + have ⟨p₀, hp₀⟩ := huv.exists_isPath + have ⟨n, hmax⟩ := this.exists_maximal ⟨_, ⟨p₀, hp₀, rfl⟩⟩ + obtain ⟨p, hp, rfl⟩ := hmax.prop + exact ⟨p, hp, (hmax.le ⟨·, ·, rfl⟩)⟩ + /-- 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..29cf89d2dd36f6 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Paths.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Paths.lean @@ -367,8 +367,8 @@ theorem IsPath.dropLast (hp : p.IsPath) : p.dropLast.IsPath := hp.take _ /-- 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) + [N : 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 @@ -381,9 +381,13 @@ lemma exists_isTrail_forall_isTrail_length_le_length (G : SimpleGraph V) [N : No have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩ lia +@[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) + [N : 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 @@ -396,6 +400,39 @@ lemma exists_isPath_forall_isPath_length_le_length (G : SimpleGraph V) [N : None have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩ lia +@[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 + let s := {(p.length) | (v : V) (p : G.Walk u v) (hp : p.IsTrail)} + have := Fintype.ofFinite G.edgeSet + have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) + fun n ⟨v, p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset + have ⟨n, hmax⟩ := this.exists_maximal ⟨0, ⟨u, nil, .nil, rfl⟩⟩ + obtain ⟨v, p, hp, rfl⟩ := hmax.prop + exact ⟨v, p, hp, (hmax.le ⟨·, ·, ·, 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 + let s := {(p.length) | (v : V) (p : G.Walk u v) (hp : p.IsPath)} + have := Fintype.ofFinite G.edgeSet + have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) + fun n ⟨v, p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset + have ⟨n, hmax⟩ := this.exists_maximal ⟨0, ⟨u, nil, .nil, rfl⟩⟩ + obtain ⟨v, p, hp, rfl⟩ := hmax.prop + exact ⟨v, p, hp, (hmax.le ⟨·, ·, ·, rfl⟩)⟩ + /-! ### About paths -/ instance [DecidableEq V] {u v : V} (p : G.Walk u v) : Decidable p.IsPath := by @@ -970,6 +1007,37 @@ 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 + let s := {(p.length) | (p : G.Walk v v) (hp : p.IsCircuit)} + have := Fintype.ofFinite G.edgeSet + have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) + fun n ⟨p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset + have ⟨p₀, hp₀⟩ := h + have ⟨n, hmax⟩ := this.exists_maximal ⟨_, p₀, hp₀, rfl⟩ + obtain ⟨p, hp, rfl⟩ := hmax.prop + exact ⟨p, hp, (hmax.le ⟨·, ·, rfl⟩)⟩ + +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 + let s := {(p.length) | (p : G.Walk v v) (hp : p.IsCycle)} + have := Fintype.ofFinite G.edgeSet + have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) + fun n ⟨p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset + have ⟨p₀, hp₀⟩ := h + classical + have ⟨n, hmax⟩ := this.exists_maximal ⟨_, _, hp₀.isCycle_cycleBypass, rfl⟩ + obtain ⟨p, hp, rfl⟩ := hmax.prop + exact ⟨p, hp, (hmax.le ⟨·, ·, rfl⟩)⟩ + /-! ### Mapping paths -/ namespace Walk From d65f0fc59cf3c7e7e4a0117493212294e6eb3c71 Mon Sep 17 00:00:00 2001 From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> Date: Thu, 9 Jul 2026 06:29:14 +0300 Subject: [PATCH 2/3] generalize to "exists longest trail with property" and golf --- .../Combinatorics/SimpleGraph/Acyclic.lean | 22 ++---- .../SimpleGraph/Connectivity/Connected.lean | 18 +---- Mathlib/Combinatorics/SimpleGraph/Paths.lean | 78 ++++++++----------- 3 files changed, 42 insertions(+), 76 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean index 08638f946dc06b..c2ee334d070acb 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean @@ -124,27 +124,17 @@ lemma IsAcyclic.anti {G' : SimpleGraph V} (hsub : G ≤ G') (h : G'.IsAcyclic) : 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 - let s := {(p.length) | (v : V) (p : G.Walk v v) (hp : p.IsCircuit)} - have := Fintype.ofFinite G.edgeSet - have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) - fun n ⟨v, p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset - have ⟨v, p₀, hp₀⟩ := not_isAcyclic_iff_exists_isCircuit.mp h - have ⟨n, hmax⟩ := this.exists_maximal ⟨_, ⟨v, p₀, hp₀, rfl⟩⟩ - obtain ⟨v, p, hp, rfl⟩ := hmax.prop - exact ⟨v, p, hp, (hmax.le ⟨·, ·, ·, rfl⟩)⟩ + 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 - let s := {(p.length) | (v : V) (p : G.Walk v v) (hp : p.IsCycle)} - have := Fintype.ofFinite G.edgeSet - have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) - fun n ⟨v, p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset - have ⟨v, p₀, hp₀⟩ := not_isAcyclic_iff_exists_isCycle.mp h - have ⟨n, hmax⟩ := this.exists_maximal ⟨_, ⟨v, p₀, hp₀, rfl⟩⟩ - obtain ⟨v, p, hp, rfl⟩ := hmax.prop - exact ⟨v, p, hp, (hmax.le ⟨·, ·, ·, rfl⟩)⟩ + 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) : diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean index 2d38d331979dc2..6fd39981a07184 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean @@ -226,14 +226,9 @@ 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 - let s := {(p.length) | (p : G.Walk u v) (hp : p.IsTrail)} - have := Fintype.ofFinite G.edgeSet - have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) - fun n ⟨p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset have ⟨p₀, hp₀⟩ := huv.exists_isPath - have ⟨n, hmax⟩ := this.exists_maximal ⟨_, ⟨p₀, hp₀.isTrail, rfl⟩⟩ - obtain ⟨p, hp, rfl⟩ := hmax.prop - exact ⟨p, hp, (hmax.le ⟨·, ·, rfl⟩)⟩ + 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 @@ -241,14 +236,9 @@ 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 - let s := {(p.length) | (p : G.Walk u v) (hp : p.IsPath)} - have := Fintype.ofFinite G.edgeSet - have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) - fun n ⟨p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset have ⟨p₀, hp₀⟩ := huv.exists_isPath - have ⟨n, hmax⟩ := this.exists_maximal ⟨_, ⟨p₀, hp₀, rfl⟩⟩ - obtain ⟨p, hp, rfl⟩ := hmax.prop - exact ⟨p, hp, (hmax.le ⟨·, ·, rfl⟩)⟩ + 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] diff --git a/Mathlib/Combinatorics/SimpleGraph/Paths.lean b/Mathlib/Combinatorics/SimpleGraph/Paths.lean index 29cf89d2dd36f6..70ef40d97b36d8 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Paths.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Paths.lean @@ -366,20 +366,31 @@ 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 _root_.SimpleGraph.exists_isTrail_forall_isTrail_length_le_length (G : SimpleGraph V) [N : 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 := @@ -390,15 +401,9 @@ lemma _root_.SimpleGraph.exists_isPath_forall_isPath_length_le_length (G : Simpl [N : 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 @@ -410,13 +415,7 @@ theorem _root_.SimpleGraph.exists_isTrail_forall_isTrail_length_le_length' [Fini (u : V) : ∃ (v : V) (p : G.Walk u v), p.IsTrail ∧ ∀ v' (p' : G.Walk u v'), p'.IsTrail → p'.length ≤ p.length := by - let s := {(p.length) | (v : V) (p : G.Walk u v) (hp : p.IsTrail)} - have := Fintype.ofFinite G.edgeSet - have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) - fun n ⟨v, p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset - have ⟨n, hmax⟩ := this.exists_maximal ⟨0, ⟨u, nil, .nil, rfl⟩⟩ - obtain ⟨v, p, hp, rfl⟩ := hmax.prop - exact ⟨v, p, hp, (hmax.le ⟨·, ·, ·, rfl⟩)⟩ + 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 @@ -425,13 +424,8 @@ theorem _root_.SimpleGraph.exists_isPath_forall_isPath_length_le_length' [Finite (u : V) : ∃ (v : V) (p : G.Walk u v), p.IsPath ∧ ∀ v' (p' : G.Walk u v'), p'.IsPath → p'.length ≤ p.length := by - let s := {(p.length) | (v : V) (p : G.Walk u v) (hp : p.IsPath)} - have := Fintype.ofFinite G.edgeSet - have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) - fun n ⟨v, p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset - have ⟨n, hmax⟩ := this.exists_maximal ⟨0, ⟨u, nil, .nil, rfl⟩⟩ - obtain ⟨v, p, hp, rfl⟩ := hmax.prop - exact ⟨v, p, hp, (hmax.le ⟨·, ·, ·, rfl⟩)⟩ + 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 -/ @@ -1013,14 +1007,10 @@ 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 - let s := {(p.length) | (p : G.Walk v v) (hp : p.IsCircuit)} - have := Fintype.ofFinite G.edgeSet - have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) - fun n ⟨p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset have ⟨p₀, hp₀⟩ := h - have ⟨n, hmax⟩ := this.exists_maximal ⟨_, p₀, hp₀, rfl⟩ - obtain ⟨p, hp, rfl⟩ := hmax.prop - exact ⟨p, hp, (hmax.le ⟨·, ·, rfl⟩)⟩ + 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 @@ -1028,15 +1018,11 @@ 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 - let s := {(p.length) | (p : G.Walk v v) (hp : p.IsCycle)} - have := Fintype.ofFinite G.edgeSet - have : s.Finite := .subset (Set.finite_le_nat G.edgeFinset.card) - fun n ⟨p, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset have ⟨p₀, hp₀⟩ := h classical - have ⟨n, hmax⟩ := this.exists_maximal ⟨_, _, hp₀.isCycle_cycleBypass, rfl⟩ - obtain ⟨p, hp, rfl⟩ := hmax.prop - exact ⟨p, hp, (hmax.le ⟨·, ·, rfl⟩)⟩ + 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 -/ From 7d3065d46a3152bb33cae90dc127e795273f589e Mon Sep 17 00:00:00 2001 From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> Date: Thu, 9 Jul 2026 12:05:25 +0300 Subject: [PATCH 3/3] remove `Nonempty` param names --- Mathlib/Combinatorics/SimpleGraph/Paths.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Paths.lean b/Mathlib/Combinatorics/SimpleGraph/Paths.lean index 70ef40d97b36d8..ef8b206e0aef1e 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Paths.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Paths.lean @@ -385,7 +385,7 @@ theorem _root_.SimpleGraph.exists_isTrail_forall_length_le_of_pred [Finite G.edg /-- There exists a trail of maximal length in a non-empty graph on finite edges. -/ lemma _root_.SimpleGraph.exists_isTrail_forall_isTrail_length_le_length (G : SimpleGraph V) - [N : Nonempty V] [Finite G.edgeSet] : + [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 v₀ := Classical.arbitrary V @@ -398,7 +398,7 @@ alias exists_isTrail_forall_isTrail_length_le_length := /-- There exists a path of maximal length in a non-empty graph on finite edges. -/ lemma _root_.SimpleGraph.exists_isPath_forall_isPath_length_le_length (G : SimpleGraph V) - [N : Nonempty V] [Finite G.edgeSet] : + [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 v₀ := Classical.arbitrary V