From f2ff2a17f0f7f10ec806fecdac68eb75e6da9604 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 11 Jul 2026 20:18:04 +0300
Subject: [PATCH] feat(SimpleGraph/Trails): a walk is Eulerian iff it is a
 trail of length `G.edgeSet.encard`

---
 Mathlib/Combinatorics/SimpleGraph/Paths.lean  | 16 ++++++++--
 Mathlib/Combinatorics/SimpleGraph/Trails.lean | 32 ++++++++++++++++---
 2 files changed, 41 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Paths.lean b/Mathlib/Combinatorics/SimpleGraph/Paths.lean
index ada1da35a5daf0..589cad388facb8 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Paths.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Paths.lean
@@ -6,9 +6,7 @@ Authors: Kyle Miller
 module
 
 public import Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
-public import Mathlib.Combinatorics.SimpleGraph.Walk.Maps
-public import Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
-public import Mathlib.Order.Preorder.Finite
+public import Mathlib.Data.Set.Card
 
 /-!
 
@@ -184,6 +182,18 @@ theorem IsTrail.length_le_card_edgeFinset [Fintype G.edgeSet] {u v : V}
     simpa [edges] using h
   exact Finset.card_le_card this
 
+theorem isTrail_iff_ncard_edgeSet_eq_length : p.IsTrail ↔ p.edgeSet.ncard = p.length := by
+  classical
+  rw [isTrail_def, ← length_edges, edgeSet, ← List.coe_toFinset, Set.ncard_coe_finset,
+    List.card_toFinset, ← List.dedup_eq_self, p.edges.dedup_sublist.length_eq]
+
+alias ⟨IsTrail.ncard_edgeSet, _⟩ := isTrail_iff_ncard_edgeSet_eq_length
+
+theorem isTrail_iff_encard_edgeSet_eq_length : p.IsTrail ↔ p.edgeSet.encard = p.length := by
+  simp [isTrail_iff_ncard_edgeSet_eq_length, edgeSet, ← p.edges.finite_toSet.cast_ncard_eq]
+
+alias ⟨IsTrail.encard_edgeSet, _⟩ := isTrail_iff_encard_edgeSet_eq_length
+
 theorem IsPath.nil {u : V} : (nil : G.Walk u u).IsPath := by constructor <;> simp
 
 theorem IsPath.of_cons {u v w : V} {h : G.Adj u v} {p : G.Walk v w} :
diff --git a/Mathlib/Combinatorics/SimpleGraph/Trails.lean b/Mathlib/Combinatorics/SimpleGraph/Trails.lean
index d2e877fc573e22..08388391af435e 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Trails.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Trails.lean
@@ -5,7 +5,6 @@ Authors: Kyle Miller
 -/
 module
 
-public import Mathlib.Algebra.Ring.Parity
 public import Mathlib.Combinatorics.SimpleGraph.Paths
 
 /-!
@@ -110,20 +109,45 @@ theorem isEulerian_iff {u v : V} (p : G.Walk u v) :
   · rintro ⟨h, hl⟩
     exact h.isEulerian_of_forall_mem hl
 
+theorem isEulerian_iff_isTrail_and_edgeSet_eq {u v : V} {p : G.Walk u v} :
+    p.IsEulerian ↔ p.IsTrail ∧ p.edgeSet = G.edgeSet := by
+  rw [isEulerian_iff, and_congr_right_iff]
+  exact fun _ ↦ ⟨Set.Subset.antisymm p.edges_subset_edgeSet, fun h ↦ by simp [← h]⟩
+
+theorem isEulerian_iff_isTrail_and_length_eq_encard {u v : V} {p : G.Walk u v} :
+    p.IsEulerian ↔ p.IsTrail ∧ p.length = G.edgeSet.encard := by
+  rw [isEulerian_iff_isTrail_and_edgeSet_eq, and_congr_right_iff, ← length_edges]
+  intro hp
+  rw [← hp.edges_nodup.dedup, ← List.card_toFinset, ← Set.ncard_coe_finset, List.coe_toFinset,
+    p.edges.finite_toSet.cast_ncard_eq, ← edgeSet]
+  refine ⟨congrArg _, fun h ↦ ?_⟩
+  exact p.edges.finite_toSet.eq_of_subset_of_encard_le p.edges_subset_edgeSet h.symm.le
+
 theorem IsTrail.isEulerian_iff {u v : V} {p : G.Walk u v} (hp : p.IsTrail) :
-    p.IsEulerian ↔ p.edgeSet = G.edgeSet :=
-  ⟨fun h ↦ Set.Subset.antisymm p.edges_subset_edgeSet (p.isEulerian_iff.mp h).2,
-   fun h ↦ p.isEulerian_iff.mpr ⟨hp, by simp [← h]⟩⟩
+    p.IsEulerian ↔ p.edgeSet = G.edgeSet := by
+  simp [isEulerian_iff_isTrail_and_edgeSet_eq, hp]
 
 theorem IsEulerian.edgeSet_eq {u v : V} {p : G.Walk u v} (h : p.IsEulerian) :
     p.edgeSet = G.edgeSet := by
   rwa [← h.isTrail.isEulerian_iff]
 
+theorem IsEulerian.finite_edgeSet {u v : V} {p : G.Walk u v} (h : p.IsEulerian) :
+    G.edgeSet.Finite :=
+  h.edgeSet_eq ▸ p.edges.finite_toSet
+
+theorem IsEulerian.length_eq_ncard_edgeSet {u v : V} {p : G.Walk u v} (h : p.IsEulerian) :
+    p.length = G.edgeSet.ncard := by
+  rw [← h.isTrail.ncard_edgeSet, h.edgeSet_eq]
+
 theorem IsEulerian.edgesFinset_eq [Fintype G.edgeSet] {u v : V} {p : G.Walk u v}
     (h : p.IsEulerian) : h.isTrail.edgesFinset = G.edgeFinset := by
   ext e
   simp [h.mem_edges_iff]
 
+theorem IsEulerian.length_eq_card_edgeFinset [Fintype G.edgeSet] {u v : V} {p : G.Walk u v}
+    (h : p.IsEulerian) : p.length = G.edgeFinset.card := by
+  simp [← h.edgesFinset_eq]
+
 theorem IsEulerian.even_degree_iff {x u v : V} {p : G.Walk u v} (ht : p.IsEulerian) [Fintype V]
     [DecidableRel G.Adj] : Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v := by
   convert! ht.isTrail.even_countP_edges_iff x