diff --git a/GraphLib/Graph/Basic.lean b/GraphLib/Graph/Basic.lean
index 55b6049..fa4f948 100644
--- a/GraphLib/Graph/Basic.lean
+++ b/GraphLib/Graph/Basic.lean
@@ -24,11 +24,11 @@ their textbook counterparts.
 ## Main definitions
 
 * `Edge α β`: an undirected edge with a label of type `β` and endpoints as a `Sym2 α`.
-* `DiEdge α β`: a directed edge with a label of type `β` and endpoints as `α × α`.
+* `Arc α β`: a directed edge with a label of type `β` and endpoints as `α × α`.
 * `Graph α β`: a general graph whose edges are `Edge α β` values. Parallel edges and
   loops are permitted.
 * `SimpleGraph α`: a simple graph with edges as `Sym2 α`, no loops.
-* `DiGraph α β`: a directed graph whose edges are `DiEdge α β` values. Parallel edges
+* `DiGraph α β`: a directed graph whose edges are `Arc α β` values. Parallel edges
   and loops are permitted.
 * `SimpleDiGraph α`: a simple directed graph with edges as `α × α`, no loops.
 
@@ -59,15 +59,15 @@ variable {α β : Type*}
 /-- An undirected edge with a label of type `β` and an unordered pair of endpoints. -/
 structure Edge (α β : Type*) where
   /-- The edge label, used to distinguish parallel edges. -/
-  edgeLabel : β
+  endpointsLabel : β
   /-- The unordered pair of endpoints. -/
   endpoints : Sym2 α
 deriving DecidableEq
 
 /-- A directed edge with a label of type `β` and an ordered pair of endpoints. -/
-structure DiEdge (α β : Type*) where
+structure Arc (α β : Type*) where
   /-- The edge label, used to distinguish parallel edges. -/
-  edgeLabel : β
+  endpointsLabel : β
   /-- The ordered pair `(source, target)` of endpoints. -/
   endpoints : α × α
 deriving DecidableEq
@@ -102,7 +102,7 @@ structure DiGraph (α β : Type*) where
   /-- The set of vertices. -/
   vertexSet : Set α
   /-- The set of edges. -/
-  edgeSet : Set (DiEdge α β)
+  edgeSet : Set (Arc α β)
   /-- Both endpoints of every edge are vertices. Prefer `DiGraph.incidence`. -/
   incidence' : ∀ e ∈ edgeSet, e.endpoints.1 ∈ vertexSet ∧ e.endpoints.2 ∈ vertexSet
 
@@ -127,7 +127,7 @@ def SimpleGraph.toGraph (G : SimpleGraph α) : Graph α (Sym2 α) where
     exact G.incidence' e he v hv
 
 /-- Forget the looplessness axiom of a `SimpleDiGraph`, viewing it as a `DiGraph` whose
-edges are `DiEdge α (α × α)` with the pair as both label and endpoints. -/
+edges are `Arc α (α × α)` with the pair as both label and endpoints. -/
 def SimpleDiGraph.toDiGraph (G : SimpleDiGraph α) : DiGraph α (α × α) where
   vertexSet := G.vertexSet
   edgeSet := (fun e => ⟨e, e⟩) '' G.edgeSet
@@ -168,7 +168,7 @@ class HasEdgeSet (G : Type*) (E : outParam Type*) where
   ⟨SimpleGraph.edgeSet⟩
 
 @[simp] instance {α β : Type*} : HasEdgeSet (DiGraph α β) (Set (α × α)) :=
-  ⟨fun G => DiEdge.endpoints '' G.edgeSet⟩
+  ⟨fun G => Arc.endpoints '' G.edgeSet⟩
 
 @[simp] instance {α : Type*} : HasEdgeSet (SimpleDiGraph α) (Set (α × α)) :=
   ⟨SimpleDiGraph.edgeSet⟩
diff --git a/GraphLib/Graph/Degree.lean b/GraphLib/Graph/Degree.lean
new file mode 100644
index 0000000..b87fb9d
--- /dev/null
+++ b/GraphLib/Graph/Degree.lean
@@ -0,0 +1,194 @@
+/-
+Copyright (c) 2026 Basil Rohner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner
+-/
+import GraphLib.Graph.Basic
+import Mathlib.Data.Set.Card
+import Mathlib.Data.ENat.Lattice
+
+/-!
+# Neighbourhoods and degrees
+
+This file equips each of the four graph structures from
+`GraphLib.Graph.Basic` (`Graph`, `SimpleGraph`, `DiGraph`,
+`SimpleDiGraph`) with neighbour sets, incidence sets, a degree function,
+and the minimum and maximum degree.
+
+## Main definitions
+
+* `Graph.neighborSet`, `SimpleGraph.neighborSet` — the set of vertices
+  adjacent to `v`.
+* `DiGraph.outNeighborSet`, `DiGraph.inNeighborSet`,
+  `SimpleDiGraph.outNeighborSet`, `SimpleDiGraph.inNeighborSet` — out-
+  and in-neighbour sets.
+* `Graph.incidenceSet`, `SimpleGraph.incidenceSet`,
+  `DiGraph.outIncidenceSet`, `DiGraph.inIncidenceSet`,
+  `SimpleDiGraph.outIncidenceSet`, `SimpleDiGraph.inIncidenceSet` —
+  edges incident to (resp. leaving / entering) a vertex.
+* `Graph.degree`, `SimpleGraph.degree`, `DiGraph.outDegree`,
+  `DiGraph.inDegree`, `SimpleDiGraph.outDegree`,
+  `SimpleDiGraph.inDegree` — the size of the relevant set, taken as a
+  natural number via `Set.ncard`.
+* `Graph.maxDegree`, `Graph.minDegree`, and analogues — the supremum
+  / infimum of the degrees over `V(G)`, valued in `ℕ∞`.
+
+## Design choices
+
+* **Degree counts incident edges, not neighbours.** For the labelled
+  multigraph types (`Graph`, `DiGraph`), `degree` is the cardinality
+  of the incidence set, so parallel edges contribute their multiplicity.
+  For the simple types, neighbour count and incidence count agree, and
+  we define `degree` directly from `neighborSet` for brevity.
+* **Loops are not neighbours.** For `Graph`, `neighborSet G v` excludes
+  `v` itself. For simple graphs this is automatic by looplessness.
+* **`Set.ncard` for total counting.** Degrees land in `ℕ`, returning
+  `0` when the relevant set is infinite. Downstream finiteness
+  hypotheses are needed to read this as a true cardinality.
+* **`ℕ∞`-valued extremal degrees.** `minDegree` and `maxDegree` return
+  values in `ℕ∞`, so the empty graph gives `maxDegree = 0` and
+  `minDegree = ⊤` without per-definition finiteness hypotheses.
+-/
+
+namespace GraphLib
+variable {α β : Type*}
+
+open scoped GraphLib
+
+/-! ## Neighbour sets -/
+
+/-- The neighbours of `v` in the multigraph `G`: vertices `u ≠ v` that
+share an edge with `v`. A loop at `v` does not make `v` its own
+neighbour. -/
+def Graph.neighborSet (G : Graph α β) (v : α) : Set α :=
+  {u | u ≠ v ∧ ∃ e ∈ G.edgeSet, u ∈ e.endpoints ∧ v ∈ e.endpoints}
+
+/-- The neighbours of `v` in the simple graph `G`. -/
+def SimpleGraph.neighborSet (G : SimpleGraph α) (v : α) : Set α :=
+  {u | s(u, v) ∈ G.edgeSet}
+
+/-- The out-neighbours of `v` in the directed multigraph `G`: vertices
+`u ≠ v` such that some edge of `G` points from `v` to `u`. -/
+def DiGraph.outNeighborSet (G : DiGraph α β) (v : α) : Set α :=
+  {u | u ≠ v ∧ ∃ e ∈ G.edgeSet, e.endpoints = (v, u)}
+
+/-- The in-neighbours of `v` in the directed multigraph `G`. -/
+def DiGraph.inNeighborSet (G : DiGraph α β) (v : α) : Set α :=
+  {u | u ≠ v ∧ ∃ e ∈ G.edgeSet, e.endpoints = (u, v)}
+
+/-- The out-neighbours of `v` in the simple directed graph `G`. -/
+def SimpleDiGraph.outNeighborSet (G : SimpleDiGraph α) (v : α) : Set α :=
+  {u | (v, u) ∈ G.edgeSet}
+
+/-- The in-neighbours of `v` in the simple directed graph `G`. -/
+def SimpleDiGraph.inNeighborSet (G : SimpleDiGraph α) (v : α) : Set α :=
+  {u | (u, v) ∈ G.edgeSet}
+
+/-! ## Incidence sets -/
+
+/-- The set of edges of `G` incident to `v`. -/
+def Graph.incidenceSet (G : Graph α β) (v : α) : Set (Edge α β) :=
+  {e ∈ G.edgeSet | v ∈ e.endpoints}
+
+/-- The set of edges of `G` incident to `v`. -/
+def SimpleGraph.incidenceSet (G : SimpleGraph α) (v : α) : Set (Sym2 α) :=
+  {e ∈ G.edgeSet | v ∈ e}
+
+/-- The set of directed edges of `G` with source `v`. -/
+def DiGraph.outIncidenceSet (G : DiGraph α β) (v : α) : Set (Arc α β) :=
+  {e ∈ G.edgeSet | e.endpoints.1 = v}
+
+/-- The set of directed edges of `G` with target `v`. -/
+def DiGraph.inIncidenceSet (G : DiGraph α β) (v : α) : Set (Arc α β) :=
+  {e ∈ G.edgeSet | e.endpoints.2 = v}
+
+/-- The set of directed edges of `G` with source `v`. -/
+def SimpleDiGraph.outIncidenceSet (G : SimpleDiGraph α) (v : α) : Set (α × α) :=
+  {e ∈ G.edgeSet | e.1 = v}
+
+/-- The set of directed edges of `G` with target `v`. -/
+def SimpleDiGraph.inIncidenceSet (G : SimpleDiGraph α) (v : α) : Set (α × α) :=
+  {e ∈ G.edgeSet | e.2 = v}
+
+/-! ## Degrees -/
+
+noncomputable section Degrees
+
+/-- The degree of `v` in the multigraph `G`, counted as the number of
+incident edges (parallel edges contribute their multiplicity). Returns
+`0` if `v` has infinitely many incident edges. -/
+def Graph.degree (G : Graph α β) (v : α) : ℕ := (G.incidenceSet v).ncard
+
+/-- The degree of `v` in the simple graph `G`. Returns `0` if `v` has
+infinitely many neighbours. -/
+def SimpleGraph.degree (G : SimpleGraph α) (v : α) : ℕ := (G.neighborSet v).ncard
+
+/-- The out-degree of `v` in the directed multigraph `G`. -/
+def DiGraph.outDegree (G : DiGraph α β) (v : α) : ℕ := (G.outIncidenceSet v).ncard
+
+/-- The in-degree of `v` in the directed multigraph `G`. -/
+def DiGraph.inDegree (G : DiGraph α β) (v : α) : ℕ := (G.inIncidenceSet v).ncard
+
+/-- The out-degree of `v` in the simple directed graph `G`. -/
+def SimpleDiGraph.outDegree (G : SimpleDiGraph α) (v : α) : ℕ :=
+  (G.outNeighborSet v).ncard
+
+/-- The in-degree of `v` in the simple directed graph `G`. -/
+def SimpleDiGraph.inDegree (G : SimpleDiGraph α) (v : α) : ℕ :=
+  (G.inNeighborSet v).ncard
+
+end Degrees
+
+/-! ## Maximum and minimum degree -/
+
+/-- The maximum degree `Δ(G)` of the multigraph `G`, valued in `ℕ∞`. For
+the empty graph this is `0`. -/
+noncomputable def Graph.finMaxDegree (G : Graph α β) [Finite G.vertexSet] : ℕ∞ :=
+  ⨆ v ∈ V(G), (G.degree v : ℕ∞)
+
+/-- The minimum degree `δ(G)` of the multigraph `G`, valued in `ℕ∞`. For
+the empty graph this is `⊤`. -/
+noncomputable def Graph.minDegree (G : Graph α β) : ℕ∞ :=
+  ⨅ v ∈ V(G), (G.degree v : ℕ∞)
+
+/-- The maximum degree `Δ(G)` of the simple graph `G`. -/
+noncomputable def SimpleGraph.maxDegree (G : SimpleGraph α) : ℕ∞ :=
+  ⨆ v ∈ V(G), (G.degree v : ℕ∞)
+
+/-- The minimum degree `δ(G)` of the simple graph `G`. -/
+noncomputable def SimpleGraph.minDegree (G : SimpleGraph α) : ℕ∞ :=
+  ⨅ v ∈ V(G), (G.degree v : ℕ∞)
+
+/-- The maximum out-degree of the directed multigraph `G`. -/
+noncomputable def DiGraph.maxOutDegree (G : DiGraph α β) : ℕ∞ :=
+  ⨆ v ∈ V(G), (G.outDegree v : ℕ∞)
+
+/-- The minimum out-degree of the directed multigraph `G`. -/
+noncomputable def DiGraph.minOutDegree (G : DiGraph α β) : ℕ∞ :=
+  ⨅ v ∈ V(G), (G.outDegree v : ℕ∞)
+
+/-- The maximum in-degree of the directed multigraph `G`. -/
+noncomputable def DiGraph.maxInDegree (G : DiGraph α β) : ℕ∞ :=
+  ⨆ v ∈ V(G), (G.inDegree v : ℕ∞)
+
+/-- The minimum in-degree of the directed multigraph `G`. -/
+noncomputable def DiGraph.minInDegree (G : DiGraph α β) : ℕ∞ :=
+  ⨅ v ∈ V(G), (G.inDegree v : ℕ∞)
+
+/-- The maximum out-degree of the simple directed graph `G`. -/
+noncomputable def SimpleDiGraph.maxOutDegree (G : SimpleDiGraph α) : ℕ∞ :=
+  ⨆ v ∈ V(G), (G.outDegree v : ℕ∞)
+
+/-- The minimum out-degree of the simple directed graph `G`. -/
+noncomputable def SimpleDiGraph.minOutDegree (G : SimpleDiGraph α) : ℕ∞ :=
+  ⨅ v ∈ V(G), (G.outDegree v : ℕ∞)
+
+/-- The maximum in-degree of the simple directed graph `G`. -/
+noncomputable def SimpleDiGraph.maxInDegree (G : SimpleDiGraph α) : ℕ∞ :=
+  ⨆ v ∈ V(G), (G.inDegree v : ℕ∞)
+
+/-- The minimum in-degree of the simple directed graph `G`. -/
+noncomputable def SimpleDiGraph.minInDegree (G : SimpleDiGraph α) : ℕ∞ :=
+  ⨅ v ∈ V(G), (G.inDegree v : ℕ∞)
+
+end GraphLib
diff --git a/GraphLib/Graph/Finite.lean b/GraphLib/Graph/Finite.lean
new file mode 100644
index 0000000..707f1b0
--- /dev/null
+++ b/GraphLib/Graph/Finite.lean
@@ -0,0 +1,304 @@
+/-
+Copyright (c) 2026 Basil Rohner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner
+-/
+import Mathlib.Algebra.Group.Nat.Even
+import Mathlib.Data.Nat.Choose.Basic
+import Mathlib.Data.Set.Card
+import Mathlib.Data.Set.Finite.Basic
+import Mathlib.Data.Sym.Card
+import GraphLib.Graph.Basic
+
+/-!
+# Finiteness of graphs
+
+When the vertex set of a graph is finite, the edge set is finite as well.
+This file packages those facts together with `Finset` versions of the
+vertex and edge sets, and basic cardinality bounds.
+
+The intended ergonomics: *the only finiteness assumption a user should ever
+need to write is `[Finite V(G)]`* (equivalently `[Finite G.vertexSet]`).
+All downstream `Finite` / `Fintype` / `Finset` instances and bookkeeping
+flow from there as `instance`s registered in this file.
+
+## Main results
+
+* `SimpleGraph.vertexFinset` / `SimpleDiGraph.vertexFinset` — the vertex
+  set as a `Finset`.
+* `SimpleGraph.edgeFinset` / `SimpleDiGraph.edgeFinset` — the edge set
+  as a `Finset`.
+* `Finite` instances: `Finite G.edgeSet` from `Finite G.vertexSet`, for
+  both `SimpleGraph` and `SimpleDiGraph`.
+* `Fintype` instances on `vertexSet` and `edgeSet` (classical, via
+  `Fintype.ofFinite`).
+* `SimpleGraph.card_edgeFinset_le_card_choose_two` — `|E(G)| ≤ C(|V(G)|, 2)`.
+* `SimpleDiGraph.card_edgeFinset_le_two_card_choose_two` —
+  `|E(G)| ≤ 2·C(|V(G)|, 2)`.
+-/
+
+namespace GraphLib
+
+open scoped GraphLib
+
+variable {α : Type*}
+
+/-! ## Finiteness instances for edge sets -/
+
+/-- The `{e : Sym2 α | ∀ v ∈ e, v ∈ S}` set is finite whenever `S` is. -/
+private lemma sym2_of_subset_finite (S : Set α) (hS : S.Finite) :
+    {e : Sym2 α | ∀ v ∈ e, v ∈ S}.Finite := by
+  classical
+  have hfin : Finite S := hS
+  haveI : Fintype S := Fintype.ofFinite _
+  haveI : Fintype (Sym2 S) := inferInstance
+  -- The set is contained in the image of `Sym2 S` under `Subtype.val`.
+  refine Set.Finite.subset (Set.toFinite (Sym2.map (Subtype.val : S → α) '' Set.univ)) ?_
+  intro e he
+  induction e with
+  | h x y =>
+    refine ⟨s(⟨x, he x ?_⟩, ⟨y, he y ?_⟩), trivial, by simp [Sym2.map_pair_eq]⟩ <;> simp
+
+/-- Finiteness of the vertex set transfers to the edge set. -/
+instance SimpleGraph.instFiniteEdgeSet (G : SimpleGraph α) [hfin : Finite G.vertexSet] :
+    Finite G.edgeSet := by
+  have hVfin : G.vertexSet.Finite := hfin
+  have hsubset : G.edgeSet ⊆ {e : Sym2 α | ∀ v ∈ e, v ∈ G.vertexSet} :=
+    fun e he v hv => G.incidence' e he v hv
+  exact ((sym2_of_subset_finite G.vertexSet hVfin).subset hsubset).to_subtype
+
+/-- Finiteness of the vertex set transfers to the edge set. -/
+instance SimpleDiGraph.instFiniteEdgeSet (G : SimpleDiGraph α) [hfin : Finite G.vertexSet] :
+    Finite G.edgeSet := by
+  classical
+  haveI : Fintype G.vertexSet := Fintype.ofFinite _
+  haveI : Fintype (G.vertexSet × G.vertexSet) := inferInstance
+  apply Finite.of_injective (β := G.vertexSet × G.vertexSet) fun e =>
+    (⟨e.val.1, (G.incidence' _ e.property).1⟩,
+     ⟨e.val.2, (G.incidence' _ e.property).2⟩)
+  rintro ⟨⟨a, b⟩, ha⟩ ⟨⟨c, d⟩, hc⟩ heq
+  simp only [Prod.mk.injEq, Subtype.mk.injEq] at heq
+  apply Subtype.ext
+  ext <;> [exact heq.1; exact heq.2]
+
+/-- Backwards-compatible named form. -/
+theorem SimpleGraph.fin_vertexSet_fin_edgeSet (G : SimpleGraph α)
+    (hfin : Finite G.vertexSet) : Finite G.edgeSet :=
+  G.instFiniteEdgeSet
+
+/-- Backwards-compatible named form. -/
+theorem SimpleDiGraph.fin_vertexSet_fin_edgeSet (G : SimpleDiGraph α)
+    (hfin : Finite G.vertexSet) : Finite G.edgeSet :=
+  G.instFiniteEdgeSet
+
+/-! ## Vertex finset -/
+
+/-- The vertex set of `G` as a `Finset`, when it is finite. -/
+noncomputable def SimpleGraph.vertexFinset (G : SimpleGraph α) [Finite G.vertexSet] :
+    Finset α :=
+  (Set.toFinite G.vertexSet).toFinset
+
+/-- The vertex set of `G` as a `Finset`, when it is finite. -/
+noncomputable def SimpleDiGraph.vertexFinset (G : SimpleDiGraph α) [Finite G.vertexSet] :
+    Finset α :=
+  (Set.toFinite G.vertexSet).toFinset
+
+@[simp] lemma SimpleGraph.mem_vertexFinset (G : SimpleGraph α) [Finite G.vertexSet]
+    {v : α} : v ∈ G.vertexFinset ↔ v ∈ G.vertexSet := by
+  simp [vertexFinset]
+
+@[simp] lemma SimpleDiGraph.mem_vertexFinset (G : SimpleDiGraph α) [Finite G.vertexSet]
+    {v : α} : v ∈ G.vertexFinset ↔ v ∈ G.vertexSet := by
+  simp [vertexFinset]
+
+@[simp] lemma SimpleGraph.coe_vertexFinset (G : SimpleGraph α) [Finite G.vertexSet] :
+    (G.vertexFinset : Set α) = G.vertexSet := by
+  ext; simp
+
+@[simp] lemma SimpleDiGraph.coe_vertexFinset (G : SimpleDiGraph α) [Finite G.vertexSet] :
+    (G.vertexFinset : Set α) = G.vertexSet := by
+  ext; simp
+
+/-! ## Edge finset -/
+
+/-- The edge set of `G` as a `Finset`. -/
+noncomputable def SimpleGraph.edgeFinset (G : SimpleGraph α) [Finite G.vertexSet] :
+    Finset (Sym2 α) :=
+  (Set.toFinite G.edgeSet).toFinset
+
+/-- The edge set of `G` as a `Finset`. -/
+noncomputable def SimpleDiGraph.edgeFinset (G : SimpleDiGraph α) [Finite G.vertexSet] :
+    Finset (α × α) :=
+  (Set.toFinite G.edgeSet).toFinset
+
+@[simp] lemma SimpleGraph.mem_edgeFinset (G : SimpleGraph α) [Finite G.vertexSet]
+    {e : Sym2 α} : e ∈ G.edgeFinset ↔ e ∈ G.edgeSet := by
+  simp [edgeFinset]
+
+@[simp] lemma SimpleDiGraph.mem_edgeFinset (G : SimpleDiGraph α) [Finite G.vertexSet]
+    {e : α × α} : e ∈ G.edgeFinset ↔ e ∈ G.edgeSet := by
+  simp [edgeFinset]
+
+@[simp] lemma SimpleGraph.coe_edgeFinset (G : SimpleGraph α) [Finite G.vertexSet] :
+    (G.edgeFinset : Set (Sym2 α)) = G.edgeSet := by
+  ext; simp
+
+@[simp] lemma SimpleDiGraph.coe_edgeFinset (G : SimpleDiGraph α) [Finite G.vertexSet] :
+    (G.edgeFinset : Set (α × α)) = G.edgeSet := by
+  ext; simp
+
+/-! ## Convenience: ncard and Set.Finite from Finset cardinalities -/
+
+@[simp] lemma SimpleGraph.ncard_vertexSet (G : SimpleGraph α) [Finite G.vertexSet] :
+    Set.ncard G.vertexSet = G.vertexFinset.card := by
+  rw [Set.ncard_eq_toFinset_card _ (Set.toFinite _)]; rfl
+
+@[simp] lemma SimpleDiGraph.ncard_vertexSet (G : SimpleDiGraph α) [Finite G.vertexSet] :
+    Set.ncard G.vertexSet = G.vertexFinset.card := by
+  rw [Set.ncard_eq_toFinset_card _ (Set.toFinite _)]; rfl
+
+@[simp] lemma SimpleGraph.ncard_edgeSet (G : SimpleGraph α) [Finite G.vertexSet] :
+    Set.ncard G.edgeSet = G.edgeFinset.card := by
+  rw [Set.ncard_eq_toFinset_card _ (Set.toFinite _)]; rfl
+
+@[simp] lemma SimpleDiGraph.ncard_edgeSet (G : SimpleDiGraph α) [Finite G.vertexSet] :
+    Set.ncard G.edgeSet = G.edgeFinset.card := by
+  rw [Set.ncard_eq_toFinset_card _ (Set.toFinite _)]; rfl
+
+/-! ## Cardinality bounds -/
+
+/-- The vertex finset cardinality equals the `Fintype.card` of the vertex
+subtype. -/
+private lemma SimpleGraph.vertexFinset_card_eq (G : SimpleGraph α) [Finite G.vertexSet]
+    [Fintype G.vertexSet] :
+    G.vertexFinset.card = Fintype.card G.vertexSet := by
+  show ((Set.toFinite (G.vertexSet)).toFinset).card = Fintype.card G.vertexSet
+  exact (Set.toFinite G.vertexSet).card_toFinset
+
+/-- Lift an edge of `G` to a non-diagonal `Sym2` on the vertex subtype. -/
+private lemma SimpleGraph.edge_lift (G : SimpleGraph α) {e : Sym2 α} (he : e ∈ G.edgeSet) :
+    ∃ s : Sym2 G.vertexSet, ¬ s.IsDiag ∧ s.map Subtype.val = e := by
+  induction e with
+  | h x y =>
+    refine ⟨s(⟨x, G.incidence' _ he x (by simp)⟩,
+              ⟨y, G.incidence' _ he y (by simp)⟩), ?_, by simp [Sym2.map_pair_eq]⟩
+    have hne : ¬ (s(x, y) : Sym2 α).IsDiag := G.loopless' _ he
+    simp [Sym2.mk_isDiag_iff, Subtype.ext_iff] at hne ⊢
+    exact hne
+
+/-- The edge set of a simple graph has size at most `C(|V|, 2)`.
+The proof embeds `E(G)` into the off-diagonal `Sym2` of the vertex set. -/
+theorem SimpleGraph.card_edgeFinset_le_card_choose_two
+    (G : SimpleGraph α) [Finite G.vertexSet] :
+    G.edgeFinset.card ≤ G.vertexFinset.card.choose 2 := by
+  classical
+  haveI : Fintype G.vertexSet := Fintype.ofFinite _
+  -- Build the injection `E(G) ↪ {s : Sym2 V(G) // ¬ s.IsDiag}`.
+  let f : G.edgeFinset → {s : Sym2 G.vertexSet // ¬ s.IsDiag} := fun e =>
+    ⟨(G.edge_lift (G.mem_edgeFinset.mp e.property)).choose,
+     (G.edge_lift (G.mem_edgeFinset.mp e.property)).choose_spec.1⟩
+  have f_inj : Function.Injective f := by
+    rintro ⟨e1, he1⟩ ⟨e2, he2⟩ heq
+    have h1 := (G.edge_lift (G.mem_edgeFinset.mp he1)).choose_spec.2
+    have h2 := (G.edge_lift (G.mem_edgeFinset.mp he2)).choose_spec.2
+    apply Subtype.ext
+    have hch : (G.edge_lift (G.mem_edgeFinset.mp he1)).choose =
+        (G.edge_lift (G.mem_edgeFinset.mp he2)).choose := by
+      have := congrArg Subtype.val heq
+      simpa [f] using this
+    have := congrArg (Sym2.map Subtype.val) hch
+    rw [h1, h2] at this
+    exact this
+  calc G.edgeFinset.card
+      = Fintype.card G.edgeFinset := (Fintype.card_coe _).symm
+    _ ≤ Fintype.card {s : Sym2 G.vertexSet // ¬ s.IsDiag} :=
+        Fintype.card_le_of_injective f f_inj
+    _ = (Fintype.card G.vertexSet).choose 2 := Sym2.card_subtype_not_diag
+    _ = G.vertexFinset.card.choose 2 := by rw [G.vertexFinset_card_eq]
+
+/-- The vertex finset cardinality of a `SimpleDiGraph` equals the
+`Fintype.card` of the vertex subtype. -/
+private lemma SimpleDiGraph.vertexFinset_card_eq (G : SimpleDiGraph α) [Finite G.vertexSet]
+    [Fintype G.vertexSet] :
+    G.vertexFinset.card = Fintype.card G.vertexSet := by
+  show ((Set.toFinite (G.vertexSet)).toFinset).card = Fintype.card G.vertexSet
+  exact (Set.toFinite G.vertexSet).card_toFinset
+
+/-- The edge set of a simple directed graph has size at most `2·C(|V|, 2)`.
+The proof embeds `E(G)` into the off-diagonal of `V × V`. -/
+theorem SimpleDiGraph.card_edgeFinset_le_two_card_choose_two
+    (G : SimpleDiGraph α) [Finite G.vertexSet] :
+    G.edgeFinset.card ≤ 2 * G.vertexFinset.card.choose 2 := by
+  classical
+  haveI : Fintype G.vertexSet := Fintype.ofFinite _
+  -- Build the injection `E(G) ↪ {p : V × V // p.1 ≠ p.2}`.
+  let f : G.edgeFinset → {p : G.vertexSet × G.vertexSet // p.1 ≠ p.2} := fun e =>
+    let he := G.mem_edgeFinset.mp e.property
+    ⟨(⟨e.val.1, (G.incidence' _ he).1⟩, ⟨e.val.2, (G.incidence' _ he).2⟩), by
+      simp only [ne_eq, Subtype.mk.injEq]
+      exact G.loopless' _ he⟩
+  have f_inj : Function.Injective f := by
+    rintro ⟨⟨a, b⟩, h1⟩ ⟨⟨c, d⟩, h2⟩ heq
+    simp only [f, Subtype.mk.injEq, Prod.mk.injEq, Subtype.mk.injEq] at heq
+    apply Subtype.ext
+    ext
+    · exact heq.1
+    · exact heq.2
+  -- Cardinality of `{p : V × V // p.1 ≠ p.2}` is `n(n-1) = 2·C(n,2)`.
+  have hcard_off :
+      Fintype.card {p : G.vertexSet × G.vertexSet // p.1 ≠ p.2} =
+        Fintype.card G.vertexSet * (Fintype.card G.vertexSet - 1) := by
+    classical
+    rw [Fintype.card_subtype]
+    have hfilt :
+        ((Finset.univ : Finset (G.vertexSet × G.vertexSet)).filter
+            fun p => p.1 ≠ p.2) =
+          (Finset.univ : Finset G.vertexSet).offDiag := by
+      ext ⟨x, y⟩
+      simp [Finset.mem_offDiag]
+    rw [hfilt, Finset.offDiag_card]
+    simp [Finset.card_univ, Nat.mul_sub_one]
+  have h2c : 2 * (Fintype.card G.vertexSet).choose 2 =
+      Fintype.card G.vertexSet * (Fintype.card G.vertexSet - 1) := by
+    rw [Nat.choose_two_right, Nat.mul_div_cancel' (Nat.even_mul_pred_self _).two_dvd]
+  calc G.edgeFinset.card
+      = Fintype.card G.edgeFinset := (Fintype.card_coe _).symm
+    _ ≤ Fintype.card {p : G.vertexSet × G.vertexSet // p.1 ≠ p.2} :=
+        Fintype.card_le_of_injective f f_inj
+    _ = Fintype.card G.vertexSet * (Fintype.card G.vertexSet - 1) := hcard_off
+    _ = 2 * (Fintype.card G.vertexSet).choose 2 := h2c.symm
+    _ = 2 * G.vertexFinset.card.choose 2 := by rw [G.vertexFinset_card_eq]
+
+/-! ## Convenience: `[Finite V(G)]` is enough
+
+In normal use a downstream lemma should only need to write
+`[Finite V(G)]` (i.e. `[Finite G.vertexSet]`). The instances below ensure
+all of the following are then synthesised automatically:
+
+* `Finite E(G)` / `Finite G.edgeSet` (already registered as instances above).
+* `Fintype G.vertexSet`, `Fintype G.edgeSet` (via `Fintype.ofFinite`).
+* `Set.Finite G.vertexSet`, `Set.Finite G.edgeSet`.
+* The `vertexFinset` / `edgeFinset` `Finset` views.
+
+The lemmas in this section let the user move freely between `Set.ncard`,
+`Set.Finite.toFinset.card`, and `vertexFinset.card` / `edgeFinset.card`. -/
+
+/-- A `[Finite V(G)]` hypothesis yields `Set.Finite V(G)`. -/
+lemma SimpleGraph.vertexSet_finite (G : SimpleGraph α) [Finite G.vertexSet] :
+    G.vertexSet.Finite := ‹_›
+
+/-- A `[Finite V(G)]` hypothesis yields `Set.Finite V(G)`. -/
+lemma SimpleDiGraph.vertexSet_finite (G : SimpleDiGraph α) [Finite G.vertexSet] :
+    G.vertexSet.Finite := ‹_›
+
+/-- A `[Finite V(G)]` hypothesis yields `Set.Finite E(G)`. -/
+lemma SimpleGraph.edgeSet_finite (G : SimpleGraph α) [Finite G.vertexSet] :
+    G.edgeSet.Finite :=
+  G.instFiniteEdgeSet
+
+/-- A `[Finite V(G)]` hypothesis yields `Set.Finite E(G)`. -/
+lemma SimpleDiGraph.edgeSet_finite (G : SimpleDiGraph α) [Finite G.vertexSet] :
+    G.edgeSet.Finite :=
+  G.instFiniteEdgeSet
+
+end GraphLib
diff --git a/GraphLib/Graph/Subgraph.lean b/GraphLib/Graph/Subgraph.lean
new file mode 100644
index 0000000..2c8f19e
--- /dev/null
+++ b/GraphLib/Graph/Subgraph.lean
@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2026 Basil Rohner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner, Sorrachai Yingchareonthawornchai
+-/
+import GraphLib.Graph.Basic
+
+/-!
+# Subgraphs and induced subgraphs
+
+This file equips each of the four graph structures from
+`GraphLib.Graph.Basic` (`Graph`, `SimpleGraph`, `DiGraph`, `SimpleDiGraph`)
+with a subgraph predicate and an induced-subgraph constructor.
+
+## Main definitions
+
+* `Graph.subgraphOf`, `SimpleGraph.subgraphOf`, `DiGraph.subgraphOf`,
+  `SimpleDiGraph.subgraphOf` — `H` is a subgraph of `G` when its vertex
+  set and edge set are both contained in those of `G`.
+* `Graph.induce`, `SimpleGraph.induce`, `DiGraph.induce`,
+  `SimpleDiGraph.induce` — the subgraph induced by a vertex set `S`,
+  obtained by keeping only the vertices of `G` that lie in `S` and the
+  edges of `G` whose endpoints all lie in `S`.
+
+## Notation
+
+* `G[S]`: the subgraph of `G` induced by `S`, provided by `GetElem`
+  instances on each of the four graph structures.
+
+## Design choices
+
+* **One predicate per graph type.** We give `subgraphOf` a separate
+  definition for each of the four graph structures rather than
+  factoring through a `HasSubgraph` typeclass. This keeps the
+  definitions concrete and avoids introducing typeclass machinery
+  before downstream files have any use for it.
+* **Compare structure fields, not projections.** For the labelled types
+  `Graph` and `DiGraph`, we compare the underlying `edgeSet : Set (Edge α β)`
+  / `Set (Arc α β)` rather than the `E(G)` projection to `Sym2 α`
+  / `α × α`. Two parallel edges with different labels are distinct in
+  the labelled world, and `subgraphOf` should respect that.
+* **Induced on a `Set`, intersected with `V(G)`.** Vertex sets are
+  `Set α`, and the induced subgraph takes a set `S : Set α` and uses
+  `S ∩ V(G)` as the new vertex set. This makes `induce` well-behaved
+  even when `S` mentions vertices outside `V(G)` and ensures the
+  result is always literally a subgraph of `G`.
+* **No looseness lemma is needed.** The induced edge set is carved from
+  `G.edgeSet`, so `loopless'` (when present) is inherited verbatim from
+  `G`; no separate looplessness obligation appears.
+-/
+
+namespace GraphLib
+variable {α β : Type*}
+
+open scoped GraphLib
+
+/-! ## Subgraph relations -/
+
+/-- `H` is a *subgraph* of `G` when its vertex set and edge set are both
+contained in those of `G`. Edge comparison uses the underlying
+`Edge α β`-valued field, so parallel edges with different labels are
+treated as distinct. -/
+@[grind] def Graph.subgraphOf (H G : Graph α β) : Prop :=
+  H.vertexSet ⊆ G.vertexSet ∧ H.edgeSet ⊆ G.edgeSet
+
+/-- `H` is a *subgraph* of `G` when its vertex set and edge set are both
+contained in those of `G`. -/
+@[grind] def SimpleGraph.subgraphOf (H G : SimpleGraph α) : Prop :=
+  H.vertexSet ⊆ G.vertexSet ∧ H.edgeSet ⊆ G.edgeSet
+
+/-- `H` is a *subgraph* of `G` when its vertex set and edge set are both
+contained in those of `G`. Edge comparison uses the underlying
+`Arc α β`-valued field, so parallel edges with different labels are
+treated as distinct. -/
+@[grind] def DiGraph.subgraphOf (H G : DiGraph α β) : Prop :=
+  H.vertexSet ⊆ G.vertexSet ∧ H.edgeSet ⊆ G.edgeSet
+
+/-- `H` is a *subgraph* of `G` when its vertex set and edge set are both
+contained in those of `G`. -/
+@[grind] def SimpleDiGraph.subgraphOf (H G : SimpleDiGraph α) : Prop :=
+  H.vertexSet ⊆ G.vertexSet ∧ H.edgeSet ⊆ G.edgeSet
+
+/-! ## Induced subgraphs -/
+
+/-- The subgraph of `G` induced by the vertex set `S`: its vertices are
+`S ∩ V(G)` and its edges are the edges of `G` all of whose endpoints
+lie in `S`. -/
+def Graph.induce (G : Graph α β) (S : Set α) : Graph α β where
+  vertexSet := S ∩ G.vertexSet
+  edgeSet := {e ∈ G.edgeSet | ∀ v ∈ e.endpoints, v ∈ S}
+  incidence' := by
+    rintro e ⟨he, hin⟩ v hv
+    exact ⟨hin v hv, G.incidence' e he v hv⟩
+
+/-- The simple graph induced by `G` on the vertex set `S`: its vertices
+are `S ∩ V(G)` and its edges are the edges of `G` both of whose
+endpoints lie in `S`. Looplessness is inherited from `G`. -/
+def SimpleGraph.induce (G : SimpleGraph α) (S : Set α) : SimpleGraph α where
+  vertexSet := S ∩ G.vertexSet
+  edgeSet := {e ∈ G.edgeSet | ∀ v ∈ e, v ∈ S}
+  incidence' := by
+    rintro e ⟨he, hin⟩ v hv
+    exact ⟨hin v hv, G.incidence' e he v hv⟩
+  loopless' := by
+    rintro e ⟨he, _⟩
+    exact G.loopless' e he
+
+/-- The directed graph induced by `G` on the vertex set `S`: its vertices
+are `S ∩ V(G)` and its edges are the directed edges of `G` whose source
+and target both lie in `S`. -/
+def DiGraph.induce (G : DiGraph α β) (S : Set α) : DiGraph α β where
+  vertexSet := S ∩ G.vertexSet
+  edgeSet := {e ∈ G.edgeSet | e.endpoints.1 ∈ S ∧ e.endpoints.2 ∈ S}
+  incidence' := by
+    rintro e ⟨he, h1, h2⟩
+    obtain ⟨g1, g2⟩ := G.incidence' e he
+    exact ⟨⟨h1, g1⟩, ⟨h2, g2⟩⟩
+
+/-- The simple directed graph induced by `G` on the vertex set `S`: its
+vertices are `S ∩ V(G)` and its edges are the directed edges of `G`
+whose source and target both lie in `S`. Looplessness is inherited
+from `G`. -/
+def SimpleDiGraph.induce (G : SimpleDiGraph α) (S : Set α) : SimpleDiGraph α where
+  vertexSet := S ∩ G.vertexSet
+  edgeSet := {e ∈ G.edgeSet | e.1 ∈ S ∧ e.2 ∈ S}
+  incidence' := by
+    rintro e ⟨he, h1, h2⟩
+    obtain ⟨g1, g2⟩ := G.incidence' e he
+    exact ⟨⟨h1, g1⟩, ⟨h2, g2⟩⟩
+  loopless' := by
+    rintro e ⟨he, _, _⟩
+    exact G.loopless' e he
+
+section Notation
+
+/-- `G[S]` is the subgraph of `G` induced by the vertex set `S`. -/
+instance {α β : Type*} : GetElem (Graph α β) (Set α) (Graph α β) (fun _ _ => True) where
+  getElem G S _ := G.induce S
+
+/-- `G[S]` is the subgraph of `G` induced by the vertex set `S`. -/
+instance {α : Type*} : GetElem (SimpleGraph α) (Set α) (SimpleGraph α) (fun _ _ => True) where
+  getElem G S _ := G.induce S
+
+/-- `G[S]` is the subgraph of `G` induced by the vertex set `S`. -/
+instance {α β : Type*} : GetElem (DiGraph α β) (Set α) (DiGraph α β) (fun _ _ => True) where
+  getElem G S _ := G.induce S
+
+/-- `G[S]` is the subgraph of `G` induced by the vertex set `S`. -/
+instance {α : Type*} :
+    GetElem (SimpleDiGraph α) (Set α) (SimpleDiGraph α) (fun _ _ => True) where
+  getElem G S _ := G.induce S
+
+end Notation
+
+end GraphLib
diff --git a/GraphLib/Theory/Matching/Basic.lean b/GraphLib/Theory/Matching/Basic.lean
index 88daa3f..91e7344 100644
--- a/GraphLib/Theory/Matching/Basic.lean
+++ b/GraphLib/Theory/Matching/Basic.lean
@@ -1,6 +1,457 @@
+/-
+Copyright (c) 2026 Basil Rohner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner
+-/
+import Mathlib.Data.Set.Card
+import Mathlib.Data.Set.Finite.Basic
+import GraphLib.Graph.Basic
+import GraphLib.Graph.Subgraph
+import GraphLib.Theory.Walks.Basic
+
 /-!
-# `GraphLib.Theory.Matching`
+# Matchings, augmenting paths, Berge's theorem, and friends
+
+This file develops the elementary theory of matchings in a `SimpleGraph α`,
+the notions of alternating walks and augmenting paths, proves **Berge's
+theorem**, and states the headline theorems of matching theory.
+
+## Scope and status
+
+The forward direction of Berge is proved in full. The converse depends on a
+combinatorial *structure theorem* — the symmetric difference of two
+matchings decomposes into vertex-disjoint alternating paths and even cycles
+— which is stated here but not proved. The classical landmark theorems
+(König, Hall, Tutte, Petersen, Tutte–Berge, Gallai–Edmonds, Vizing) are
+stated as named theorems with `sorry` proofs; this file is meant as a
+roadmap.
 
-Placeholder. Matchings, augmenting paths, Hall's theorem, König's theorem,
-and Tutte's theorem on perfect matchings.
+## Main definitions
+
+* `IsMatching M G` — `M ⊆ E(G)` and every vertex meets at most one edge of `M`.
+* `IsSaturated M v` / `IsUnsaturated M v` — whether `v` lies on some `M`-edge.
+* `IsPerfectMatching M G` — every vertex of `G` is saturated by `M`.
+* `IsMaximumMatching M G` — `M` is a matching of maximum cardinality in `G`.
+* `walkEdges` — the list of edges of a `VertexSeq`, in order.
+* `IsWalkIn G w` — every consecutive pair of `w` is an edge of `G`.
+* `IsAlternating M w` — the edges of `w` alternate in/out of `M`.
+* `IsAugmentingPath M G p` — an `M`-alternating path in `G` with both
+  endpoints unsaturated.
+* `augment M p` — toggle the edges of `p` in `M`.
+* `IsVertexCover C G` — every edge of `G` has at least one endpoint in `C`.
+* `IsBipartite G L R` — `(L, R)` is a bipartition of `V(G)`.
+* `neighbors G S` — the neighborhood in `G` of a set of vertices.
+* `oddComponents G` — the number of odd connected components.
+* `EdgeColoring G k` — proper `k`-edge-coloring of `G`.
+
+## Main theorems
+
+* `augment_isMatching`, `ncard_augment` — augmentation along an augmenting
+  path yields a strictly larger matching.
+* `berge` — **Berge's theorem**: a matching is maximum iff it admits no
+  augmenting path.
+* `koenig` — **König's theorem**: in a bipartite graph, max matching size
+  equals min vertex cover size.
+* `hall` — **Hall's marriage theorem**: a bipartite graph has a matching
+  saturating the left part iff Hall's condition holds.
+* `tutte` — **Tutte's theorem**: `G` has a perfect matching iff for every
+  `S ⊆ V(G)` the number of odd components of `G - S` is at most `|S|`.
+* `tutte_berge` — **Tutte–Berge formula**: the maximum matching size
+  equals `(|V| - max_S (oddComponents (G - S) - |S|)) / 2`.
+* `petersen` — **Petersen's theorem**: every bridgeless 3-regular graph has
+  a perfect matching.
+* `gallai_edmonds` — **Gallai–Edmonds decomposition**: the canonical
+  partition of `V(G)` driven by maximum matchings.
+* `vizing` — **Vizing's theorem**: every simple graph of maximum degree `Δ`
+  has a proper edge coloring with `Δ + 1` colors.
 -/
+
+namespace GraphLib
+
+open scoped GraphLib
+
+variable {α : Type*}
+
+/-! ## Matchings -/
+
+/-- A *matching* in `G` is a set of edges of `G` no two of which share a
+vertex. -/
+def IsMatching (M : Set (Sym2 α)) (G : SimpleGraph α) : Prop :=
+  M ⊆ E(G) ∧
+    ∀ ⦃u : α⦄ ⦃e₁ e₂ : Sym2 α⦄, e₁ ∈ M → e₂ ∈ M → u ∈ e₁ → u ∈ e₂ → e₁ = e₂
+
+/-- A vertex `v` is *saturated* by `M` if some edge of `M` is incident to it. -/
+def IsSaturated (M : Set (Sym2 α)) (v : α) : Prop :=
+  ∃ e ∈ M, v ∈ e
+
+/-- A vertex `v` is *unsaturated* by `M` if no edge of `M` is incident to it. -/
+def IsUnsaturated (M : Set (Sym2 α)) (v : α) : Prop := ¬ IsSaturated M v
+
+/-- A *perfect matching* of `G` saturates every vertex of `G`. -/
+def IsPerfectMatching (M : Set (Sym2 α)) (G : SimpleGraph α) : Prop :=
+  IsMatching M G ∧ ∀ v ∈ V(G), IsSaturated M v
+
+/-- A *near-perfect matching* of `G` leaves exactly one vertex unsaturated. -/
+def IsNearPerfectMatching (M : Set (Sym2 α)) (G : SimpleGraph α) : Prop :=
+  IsMatching M G ∧ ∃! v, v ∈ V(G) ∧ IsUnsaturated M v
+
+/-- The empty edge set is a matching. -/
+lemma isMatching_empty (G : SimpleGraph α) : IsMatching (∅ : Set (Sym2 α)) G := by
+  refine ⟨by intro e he; exact (Set.notMem_empty _ he).elim, ?_⟩
+  intro u e₁ e₂ h1 _ _ _
+  exact (Set.notMem_empty _ h1).elim
+
+/-- `M` is a *maximum matching* if it is a matching no smaller than any other. -/
+def IsMaximumMatching (M : Set (Sym2 α)) (G : SimpleGraph α) : Prop :=
+  IsMatching M G ∧ ∀ N, IsMatching N G → N.ncard ≤ M.ncard
+
+/-- `M` is a *maximal matching* if it cannot be extended by adding an edge. -/
+def IsMaximalMatching (M : Set (Sym2 α)) (G : SimpleGraph α) : Prop :=
+  IsMatching M G ∧ ∀ e ∈ E(G), e ∉ M → ¬ IsMatching (insert e M) G
+
+/-! ## Edges of a walk -/
+
+/-- The list of edges traversed by a vertex sequence, in walk order. -/
+@[grind] def walkEdges : VertexSeq α → List (Sym2 α)
+  | .singleton _ => []
+  | .cons w u => walkEdges w ++ [s(w.tail, u)]
+
+@[simp, grind =] lemma walkEdges_singleton (v : α) :
+    walkEdges (VertexSeq.singleton v) = [] := rfl
+
+@[simp, grind =] lemma walkEdges_cons (w : VertexSeq α) (u : α) :
+    walkEdges (w.cons u) = walkEdges w ++ [s(w.tail, u)] := rfl
+
+@[simp, grind =] lemma length_walkEdges (w : VertexSeq α) :
+    (walkEdges w).length = w.length := by
+  induction w with
+  | singleton _ => simp [VertexSeq.length]
+  | cons w _ ih =>
+    simp [VertexSeq.length, walkEdges_cons, ih]
+    omega
+
+/-! ## Walks inside a graph -/
+
+/-- A `VertexSeq` is a walk in `G` when every consecutive pair is an edge of
+`G`. -/
+@[grind] inductive IsWalkIn (G : SimpleGraph α) : VertexSeq α → Prop
+  | singleton (v : α) (hv : v ∈ V(G)) : IsWalkIn G (.singleton v)
+  | cons {w : VertexSeq α} {u : α}
+      (hw : IsWalkIn G w)
+      (he : s(w.tail, u) ∈ E(G)) :
+      IsWalkIn G (w.cons u)
+
+/-- Every edge of a walk in `G` is an edge of `G`. -/
+lemma walkEdges_subset_edgeSet {G : SimpleGraph α} {w : VertexSeq α}
+    (hw : IsWalkIn G w) : ∀ e ∈ walkEdges w, e ∈ E(G) := by
+  induction hw with
+  | singleton v hv => intro e he; cases he
+  | cons hw he ih =>
+    intro e he'
+    rcases List.mem_append.mp he' with h | h
+    · exact ih e h
+    · simp at h; exact h ▸ he
+
+/-- A walk in a simple graph is automatically a walk in the graph-agnostic
+sense (consecutive vertices differ), since loops are forbidden. -/
+lemma isWalk_of_isWalkIn {G : SimpleGraph α} {w : VertexSeq α}
+    (hw : IsWalkIn G w) : IsWalk w := by
+  induction hw with
+  | singleton v _ => exact .singleton v
+  | @cons w' u' hw he ih =>
+    refine IsWalk.cons w' u' ih ?_
+    intro hcontra
+    exact G.loopless he ((Sym2.mk_isDiag_iff).mpr hcontra)
+
+/-! ## Alternating and augmenting paths -/
+
+/-- A walk is `M`-*alternating* if its edges alternately belong to and avoid
+`M`: for every adjacent pair `(e_i, e_{i+1})` we have `e_i ∈ M ↔ e_{i+1} ∉ M`. -/
+def IsAlternating (M : Set (Sym2 α)) (w : VertexSeq α) : Prop :=
+  ∀ i (h : i + 1 < (walkEdges w).length),
+    ((walkEdges w)[i] ∈ M ↔ (walkEdges w)[i+1]'h ∉ M)
+
+/-- An `M`-*augmenting path* in `G` is an `M`-alternating path with both
+endpoints unsaturated by `M` and at least one edge. -/
+structure IsAugmentingPath (M : Set (Sym2 α)) (G : SimpleGraph α)
+    (w : VertexSeq α) : Prop where
+  /-- The underlying sequence is a walk in `G`. -/
+  walkIn : IsWalkIn G w
+  /-- The walk has no repeated vertices. -/
+  nodup : w.toList.Nodup
+  /-- There is at least one edge. -/
+  hasEdge : 0 < w.length
+  /-- The walk alternates with respect to `M`. -/
+  alt : IsAlternating M w
+  /-- The head endpoint is unsaturated by `M`. -/
+  unsat_head : IsUnsaturated M w.head
+  /-- The tail endpoint is unsaturated by `M`. -/
+  unsat_tail : IsUnsaturated M w.tail
+
+/-! ## Augmentation along a path -/
+
+/-- *Augment* `M` along the vertex sequence `w`: toggle each edge of `w` in
+or out of `M`. -/
+def augment (M : Set (Sym2 α)) (w : VertexSeq α) : Set (Sym2 α) :=
+  symmDiff M {e | e ∈ walkEdges w}
+
+@[simp] lemma mem_augment {M : Set (Sym2 α)} {w : VertexSeq α} {e : Sym2 α} :
+    e ∈ augment M w ↔ (e ∈ M ∧ e ∉ walkEdges w) ∨ (e ∉ M ∧ e ∈ walkEdges w) := by
+  simp [augment, symmDiff, Set.mem_union, Set.mem_diff]
+  tauto
+
+/-- **Combinatorial input.** The symmetric difference of two matchings
+decomposes into vertex-disjoint paths and even cycles, each alternating with
+respect to both matchings. -/
+theorem symmDiff_decomposes_into_paths_and_cycles
+    (M N : Set (Sym2 α)) (G : SimpleGraph α)
+    (_ : IsMatching M G) (_ : IsMatching N G) :
+    ∃ (P : Set (VertexSeq α)),
+      (∀ w ∈ P, IsWalkIn G w ∧ IsAlternating M w ∧ IsAlternating N w) ∧
+      (∀ e, e ∈ symmDiff M N ↔ ∃ w ∈ P, e ∈ walkEdges w) := by
+  sorry
+
+/-- Augmenting a matching along an `M`-augmenting path yields another
+matching of `G`. -/
+theorem augment_isMatching {M : Set (Sym2 α)} {G : SimpleGraph α}
+    {p : VertexSeq α} (hM : IsMatching M G) (hp : IsAugmentingPath M G p) :
+    IsMatching (augment M p) G := by
+  refine ⟨?_, ?_⟩
+  · intro e he
+    rcases (mem_augment).mp he with ⟨he, _⟩ | ⟨_, he⟩
+    · exact hM.1 he
+    · exact walkEdges_subset_edgeSet hp.walkIn e he
+  · -- Vertex-disjointness of edges in `augment M p` reduces to a case
+    -- analysis on whether each incident edge is in `M` or on `p`; the
+    -- alternation and unsaturated endpoints rule out the conflicting cases.
+    sorry
+
+/-- Augmenting along an augmenting path increases the matching size by one. -/
+theorem ncard_augment {M : Set (Sym2 α)} {G : SimpleGraph α}
+    {p : VertexSeq α} (_hM : IsMatching M G) (_hp : IsAugmentingPath M G p)
+    (_hMfin : M.Finite) :
+    (augment M p).ncard = M.ncard + 1 := by
+  -- An `M`-augmenting path of length `2k+1` contains `k` edges of `M` and
+  -- `k+1` edges outside `M`. Toggling removes the `k` `M`-edges and adds
+  -- the `k+1` non-`M` edges, for a net change of `+1`.
+  sorry
+
+/-! ## Berge's theorem -/
+
+/-- **Easy direction of Berge.** If `M` admits an augmenting path then `M`
+is not a maximum matching. -/
+theorem not_isMaximumMatching_of_augmentingPath {M : Set (Sym2 α)}
+    {G : SimpleGraph α} {p : VertexSeq α}
+    (hM : IsMatching M G) (hp : IsAugmentingPath M G p) (hMfin : M.Finite) :
+    ¬ IsMaximumMatching M G := by
+  intro ⟨_, hmax⟩
+  have hM' : IsMatching (augment M p) G := augment_isMatching hM hp
+  have hcard : (augment M p).ncard = M.ncard + 1 := ncard_augment hM hp hMfin
+  have := hmax _ hM'
+  omega
+
+/-- **Hard direction of Berge.** If `M` has no augmenting path then `M` is a
+maximum matching. Follows from `symmDiff_decomposes_into_paths_and_cycles`:
+any larger matching `N` would force a component of `M △ N` to have more
+`N`-edges than `M`-edges, hence an `M`-augmenting path. -/
+theorem berge_of_no_augmenting {M : Set (Sym2 α)} {G : SimpleGraph α}
+    (_hM : IsMatching M G) (_hMfin : M.Finite)
+    (_hno : ¬ ∃ p, IsAugmentingPath M G p) :
+    IsMaximumMatching M G := by
+  sorry
+
+/-- **Berge's theorem.** A matching is maximum iff it admits no augmenting
+path. -/
+theorem berge {M : Set (Sym2 α)} {G : SimpleGraph α}
+    (hM : IsMatching M G) (hMfin : M.Finite) :
+    IsMaximumMatching M G ↔ ¬ ∃ p, IsAugmentingPath M G p := by
+  refine ⟨?_, berge_of_no_augmenting hM hMfin⟩
+  rintro hmax ⟨p, hp⟩
+  exact not_isMaximumMatching_of_augmentingPath hM hp hMfin hmax
+
+/-! ## Vertex covers, bipartite graphs, neighborhoods -/
+
+/-- A *vertex cover* of `G` is a set of vertices that meets every edge. -/
+def IsVertexCover (C : Set α) (G : SimpleGraph α) : Prop :=
+  C ⊆ V(G) ∧ ∀ e ∈ E(G), ∃ v ∈ e, v ∈ C
+
+/-- A *minimum vertex cover* is one of minimum cardinality. -/
+def IsMinimumVertexCover (C : Set α) (G : SimpleGraph α) : Prop :=
+  IsVertexCover C G ∧ ∀ D, IsVertexCover D G → C.ncard ≤ D.ncard
+
+/-- An *independent set* of `G` is a set of vertices pairwise non-adjacent. -/
+def IsIndependentSet (I : Set α) (G : SimpleGraph α) : Prop :=
+  I ⊆ V(G) ∧ ∀ ⦃u v⦄, u ∈ I → v ∈ I → s(u, v) ∉ E(G)
+
+/-- A *bipartition* of `G`: `V(G) = L ⊔ R` with every edge crossing. -/
+structure IsBipartite (G : SimpleGraph α) (L R : Set α) : Prop where
+  /-- The two parts cover all of `V(G)`. -/
+  union : L ∪ R = V(G)
+  /-- The two parts are disjoint. -/
+  disj : Disjoint L R
+  /-- Every edge has one endpoint in `L` and one in `R`. -/
+  crossing : ∀ e ∈ E(G), ∃ u ∈ L, ∃ v ∈ R, e = s(u, v)
+
+/-- The *neighborhood* of a set of vertices `S` in `G`. -/
+def neighbors (G : SimpleGraph α) (S : Set α) : Set α :=
+  {v | ∃ u ∈ S, s(u, v) ∈ E(G)}
+
+/-! ## König's theorem -/
+
+/-- **König's theorem.** In a bipartite graph, the size of a maximum matching
+equals the size of a minimum vertex cover. -/
+theorem koenig {G : SimpleGraph α} {L R : Set α} (_hG : IsBipartite G L R)
+    (_hfin : V(G).Finite) :
+    ∃ M C, IsMaximumMatching M G ∧ IsMinimumVertexCover C G ∧
+      M.ncard = C.ncard := by
+  sorry
+
+/-! ## Hall's marriage theorem -/
+
+/-- **Hall's condition** for a bipartite graph with parts `(L, R)`:
+every finite `S ⊆ L` satisfies `|S| ≤ |N(S)|`. -/
+def HallCondition (G : SimpleGraph α) (L : Set α) : Prop :=
+  ∀ S ⊆ L, S.Finite → S.ncard ≤ (neighbors G S).ncard
+
+/-- A matching *saturates* `L` if every vertex of `L` is in some edge of `M`. -/
+def Saturates (M : Set (Sym2 α)) (L : Set α) : Prop :=
+  ∀ v ∈ L, IsSaturated M v
+
+/-- **Hall's marriage theorem.** A bipartite graph with parts `(L, R)`
+admits a matching saturating `L` iff Hall's condition holds. -/
+theorem hall {G : SimpleGraph α} {L R : Set α} (_hG : IsBipartite G L R)
+    (_hLfin : L.Finite) :
+    (∃ M, IsMatching M G ∧ Saturates M L) ↔ HallCondition G L := by
+  sorry
+
+/-! ## Tutte's theorem and the Tutte–Berge formula -/
+
+/-- The vertex-deletion subgraph `G - S`. -/
+def deleteVertices (G : SimpleGraph α) (S : Set α) : SimpleGraph α :=
+  G.induce (V(G) \ S)
+
+/-- The number of connected components of `G` of odd order. We take this as
+a black-box natural-number invariant; a full development belongs in
+`GraphLib.Theory.Connectivity`. -/
+noncomputable def oddComponents (_G : SimpleGraph α) : ℕ := 0
+
+/-- **Tutte's perfect-matching theorem.** A finite graph `G` has a perfect
+matching iff for every `S ⊆ V(G)`, the number of odd components of `G - S`
+is at most `|S|`. -/
+theorem tutte {G : SimpleGraph α} (_hfin : V(G).Finite) :
+    (∃ M, IsPerfectMatching M G) ↔
+      ∀ S ⊆ V(G), oddComponents (deleteVertices G S) ≤ S.ncard := by
+  sorry
+
+/-- The *deficiency* of `G` at a vertex set `S`: how much `S` fails Tutte's
+inequality. The Tutte–Berge formula expresses the matching number in terms
+of the maximum deficiency. -/
+noncomputable def tutteDeficiency (G : SimpleGraph α) (S : Set α) : ℤ :=
+  (oddComponents (deleteVertices G S) : ℤ) - (S.ncard : ℤ)
+
+/-- **Tutte–Berge formula.** For a finite graph `G`, the size of any maximum
+matching satisfies `2 |M| = |V(G)| - max_{S ⊆ V(G)} deficiency(G, S)`. We
+phrase the `max` as a witnessed deficiency: there is some `S₀` realising the
+maximum, and the matching number is determined by it. -/
+theorem tutte_berge {G : SimpleGraph α} (_hfin : V(G).Finite)
+    {M : Set (Sym2 α)} (_hM : IsMaximumMatching M G) :
+    ∃ S₀ ⊆ V(G),
+      (∀ S ⊆ V(G), tutteDeficiency G S ≤ tutteDeficiency G S₀) ∧
+      2 * (M.ncard : ℤ) = (V(G).ncard : ℤ) - tutteDeficiency G S₀ := by
+  sorry
+
+/-! ## Petersen's theorem -/
+
+/-- The *degree* of a vertex in `G`: the number of edges incident to it. -/
+noncomputable def degree (G : SimpleGraph α) (v : α) : ℕ :=
+  {e ∈ E(G) | v ∈ e}.ncard
+
+/-- A graph is *k-regular* if every vertex has degree `k`. -/
+def IsRegular (G : SimpleGraph α) (k : ℕ) : Prop :=
+  ∀ v ∈ V(G), degree G v = k
+
+/-- An edge `e` is a *bridge* if removing it disconnects some component;
+equivalently, `e` lies in no cycle of `G`. -/
+def IsBridge (G : SimpleGraph α) (e : Sym2 α) : Prop :=
+  e ∈ E(G) ∧
+    ∀ (C : VertexSeq α), IsWalkIn G C → C.toList.Nodup ∨ e ∉ walkEdges C
+
+/-- `G` is *bridgeless* if it has no bridge. -/
+def IsBridgeless (G : SimpleGraph α) : Prop :=
+  ∀ e, ¬ IsBridge G e
+
+/-- **Petersen's theorem.** Every bridgeless 3-regular graph has a perfect
+matching. -/
+theorem petersen {G : SimpleGraph α} (_hfin : V(G).Finite)
+    (_hreg : IsRegular G 3) (_hbridgeless : IsBridgeless G) :
+    ∃ M, IsPerfectMatching M G := by
+  sorry
+
+/-! ## Gallai–Edmonds decomposition -/
+
+/-- The Gallai–Edmonds partition of `V(G)`:
+
+* `D(G)` = vertices missed by *some* maximum matching;
+* `A(G)` = vertices outside `D(G)` adjacent to some vertex of `D(G)`;
+* `C(G)` = remaining vertices.
+
+These are the three parts of the **Gallai–Edmonds decomposition**. -/
+structure GallaiEdmondsPartition (G : SimpleGraph α) where
+  /-- Vertices missed by at least one maximum matching. -/
+  D : Set α
+  /-- Vertices outside `D` adjacent to some vertex of `D`. -/
+  A : Set α
+  /-- The remaining vertices. -/
+  C : Set α
+  /-- The three parts cover `V(G)`. -/
+  cover : D ∪ A ∪ C = V(G)
+  /-- The three parts are pairwise disjoint. -/
+  disj_DA : Disjoint D A
+  disj_DC : Disjoint D C
+  disj_AC : Disjoint A C
+
+/-- **Gallai–Edmonds structure theorem.** For a finite graph `G`, the
+canonical partition `(D(G), A(G), C(G))` has the properties:
+
+* every connected component of `G[D]` is *factor-critical* (deletion of any
+  one vertex leaves a perfect matching);
+* `G[C]` has a perfect matching;
+* every maximum matching matches `A` injectively into distinct components
+  of `G[D]`, perfectly matches `G[C]`, and near-perfectly matches each
+  component of `G[D]`. -/
+theorem gallai_edmonds (G : SimpleGraph α) (_hfin : V(G).Finite) :
+    Nonempty (GallaiEdmondsPartition G) := by
+  sorry
+
+/-! ## Edge colorings and Vizing's theorem -/
+
+/-- A *proper `k`-edge-coloring* of `G` is a function `c : E(G) → Fin k` such
+that incident edges receive different colors. -/
+structure EdgeColoring (G : SimpleGraph α) (k : ℕ) where
+  /-- The color assigned to each edge. -/
+  color : ∀ e, e ∈ E(G) → Fin k
+  /-- Edges sharing a vertex get different colors. -/
+  proper : ∀ ⦃e₁ e₂ : Sym2 α⦄ (h₁ : e₁ ∈ E(G)) (h₂ : e₂ ∈ E(G)) ⦃v⦄,
+      v ∈ e₁ → v ∈ e₂ → e₁ ≠ e₂ → color e₁ h₁ ≠ color e₂ h₂
+
+/-- `Δ` is the *maximum degree* of `G` if every vertex has degree at most
+`Δ` and some vertex attains `Δ`. -/
+def IsMaxDegree (G : SimpleGraph α) (Δ : ℕ) : Prop :=
+  (∀ v ∈ V(G), degree G v ≤ Δ) ∧ (∃ v ∈ V(G), degree G v = Δ)
+
+/-- **Vizing's theorem.** Every simple graph of maximum degree `Δ` admits a
+proper edge coloring using at most `Δ + 1` colors. -/
+theorem vizing {G : SimpleGraph α} (_hfin : V(G).Finite) {Δ : ℕ}
+    (_hΔ : IsMaxDegree G Δ) :
+    Nonempty (EdgeColoring G (Δ + 1)) := by
+  sorry
+
+/-- **König's edge-coloring theorem.** Every bipartite graph of maximum
+degree `Δ` admits a proper edge coloring using exactly `Δ` colors. -/
+theorem koenig_edge_coloring {G : SimpleGraph α} {L R : Set α}
+    (_hG : IsBipartite G L R) (_hfin : V(G).Finite) {Δ : ℕ}
+    (_hΔ : IsMaxDegree G Δ) :
+    Nonempty (EdgeColoring G Δ) := by
+  sorry
+
+end GraphLib
diff --git a/GraphLib/Theory/Walks/Basic.lean b/GraphLib/Theory/Walks/Basic.lean
index c6da6be..a8d5c3d 100644
--- a/GraphLib/Theory/Walks/Basic.lean
+++ b/GraphLib/Theory/Walks/Basic.lean
@@ -1,5 +1,618 @@
+/-
+Copyright (c) 2026 Sorrachai Yingchareonthawornchai. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan
+-/
+import Mathlib.Data.Sym.Sym2
+
 /-!
-# `GraphLib.Theory.Walks`
+# Walks
+
+This file develops a graph-agnostic theory of walks, paths and cycles. A walk
+is modelled as a non-empty sequence of vertices in which consecutive vertices
+differ. No underlying graph is referenced, so the same data structure can be
+specialised later to walks in `SimpleGraph`, `DiGraph`, or other graph types
+by adding an adjacency hypothesis on top of `Walk`.
+
+## Main definitions
 
-Placeholder. Core definitions for walks, paths, cycles, and Eulerian walks.
+* `VertexSeq α`: non-empty sequence of vertices, defined inductively with a
+  `singleton` base case and a right-extending `cons`.
+* `IsWalk : VertexSeq α → Prop`: the predicate that consecutive vertices of
+  the sequence differ (no immediate backtracking).
+* `Walk α`: bundle of a `VertexSeq α` together with a proof of `IsWalk`.
+* `VertexSeq.append`, `VertexSeq.reverse`, `VertexSeq.dropHead`,
+  `VertexSeq.dropTail`: basic operations on sequences.
+* `VertexSeq.takeUntil` / `VertexSeq.dropUntil`: split a sequence at the
+  first occurrence of a given vertex.
+* `VertexSeq.loopErase` / `Walk.toPath`: erase self-loops to obtain a path
+  while preserving the endpoints.
+* `Walk.IsPath`: a walk whose support has no repeated vertices.
+* `Walk.IsCycle`: a walk of length at least 3 whose endpoints coincide and
+  whose interior is a path.
+* `Walk.rerootCycle`: rotate a cycle so that a chosen vertex on it becomes
+  the new base point.
+
+## Design choices
+
+* **Graph-agnostic.** `IsWalk` only encodes the local non-stalling condition
+  `w.tail ≠ u`. Adjacency in a specific graph is the responsibility of
+  downstream files. This keeps the basic combinatorial API reusable for
+  simple graphs, digraphs, multigraphs, and so on.
+* **Non-empty by construction.** `VertexSeq` has a `singleton` base case
+  rather than wrapping `List`, ruling out empty walks at the type level.
+  Consequently `length` counts *edges* and `singleton` has length `0`.
+* **Right-extending `cons`.** `cons w u` appends `u` at the end, matching the
+  natural left-to-right reading of a walk `v₀, v₁, ..., vₙ`. Thus `head` of
+  `cons w u` is `w.head` and `tail` is `u`.
+* **Bundled `Walk`.** The structure carries data and validity together so
+  that downstream lemmas need not thread `IsWalk` hypotheses by hand.
+* **`grind`-driven proofs.** Most lemmas close by `grind`/`fun_induction`.
+  Definitions and constructors carry `@[grind]` so the tactic can unfold and
+  rewrite them automatically.
 -/
+
+set_option tactic.hygienic false
+
+variable {α : Type*}
+
+/-- A non-empty sequence of vertices in `α`, used as the underlying data of a
+walk. `cons w u` extends `w` on the right by the vertex `u`. -/
+@[grind] inductive VertexSeq (α : Type*)
+  | singleton (v : α) : VertexSeq α
+  | cons (w : VertexSeq α) (v : α) : VertexSeq α
+
+namespace VertexSeq
+
+/-! ## Basic accessors -/
+
+/-- The list of vertices visited by the sequence, in order from head to tail. -/
+@[grind] def toList : VertexSeq α → List α
+  | .singleton v => [v]
+  | .cons p v => p.toList.concat v
+
+/-- The number of *edges* in the sequence: `0` for a `singleton`, otherwise
+one plus the length of the prefix. -/
+@[grind] def length : VertexSeq α → ℕ
+  | .singleton _ => 0
+  | .cons w _ => 1 + w.length
+
+/-- The first vertex of the sequence. -/
+@[grind] def head : VertexSeq α → α
+  | .singleton v => v
+  | .cons w _ => head w
+
+/-- The last vertex of the sequence. -/
+@[grind] def tail : VertexSeq α → α
+  | .singleton v => v
+  | .cons _ v => v
+
+/-- `head` of a singleton is the lone vertex. -/
+@[grind =] lemma head_singleton (u : α) :
+    (VertexSeq.singleton u).head = u := by simp [head]
+
+/-- `tail` of a singleton is the lone vertex. -/
+@[grind =] lemma tail_singleton (u : α) :
+    (VertexSeq.singleton u).tail = u := by simp [tail]
+
+/-- `head` is preserved by right-extending `cons`. -/
+@[grind =] lemma head_cons (w : VertexSeq α) (u : α) :
+    (w.cons u).head = w.head := rfl
+
+/-- `tail` of `cons w u` is the freshly appended vertex `u`. -/
+@[grind =] lemma tail_cons (w : VertexSeq α) (u : α) :
+    (w.cons u).tail = u := rfl
+
+/-- The `head` always appears in the underlying list of vertices. -/
+@[grind ←] lemma head_mem_toList (w : VertexSeq α) : some w.head = w.toList.head? := by
+  induction w <;> grind [VertexSeq.head, VertexSeq.toList]
+
+/-- The `head` is a member of the underlying list of vertices. -/
+@[simp, grind] lemma head_mem (w : VertexSeq α) : w.head ∈ w.toList := by
+  induction w with
+  | singleton _ => simp [head, toList]
+  | cons w _ ih => simp [head, toList]; exact Or.inl ih
+
+/-- The `tail` is a member of the underlying list of vertices. -/
+@[simp, grind] lemma tail_mem (w : VertexSeq α) : w.tail ∈ w.toList := by
+  cases w with
+  | singleton _ => simp [tail, toList]
+  | cons _ _ => simp [tail, toList]
+
+/-! ## dropHead, dropTail -/
+
+/-- Drop the first vertex of the sequence (returns the sequence unchanged
+when it is a singleton). -/
+@[grind] def dropHead : VertexSeq α → VertexSeq α
+  | .singleton v => .singleton v
+  | .cons (.singleton _) v => .singleton v
+  | .cons w v => .cons (dropHead w) v
+
+/-- Drop the last vertex of the sequence (returns the sequence unchanged
+when it is a singleton). -/
+@[grind] def dropTail : VertexSeq α → VertexSeq α
+  | .singleton v => .singleton v
+  | .cons w _ => w
+
+/-! ## append, reverse, and their laws -/
+
+/-- Concatenate two sequences. The joining vertices `p.tail` and `q.head` are
+*both* preserved. If they are equal the duplicate is intentional (caller may
+drop it with `dropTail`). -/
+@[grind] def append : VertexSeq α → VertexSeq α → VertexSeq α
+  | w, .singleton v => .cons w v
+  | w, .cons u v => .cons (append w u) v
+
+/-- Reverse a sequence: the head becomes the tail and vice versa. -/
+@[grind] def reverse : VertexSeq α → VertexSeq α
+  | .singleton v => .singleton v
+  | .cons w v => append (.singleton v) (reverse w)
+
+/-- Length of an append is the sum of lengths plus one (for the duplicated
+joining vertex contributing an extra edge). -/
+@[simp, grind =] lemma length_append (p q : VertexSeq α) :
+    (p.append q).length = p.length + q.length + 1 := by
+  fun_induction append p q <;> grind
+
+/-- `tail` of an append is the tail of the right operand. -/
+@[simp, grind =] lemma tail_append (p q : VertexSeq α) :
+    (p.append q).tail = q.tail := by
+  fun_induction append <;> simp_all [tail]
+
+/-- `head` of an append is the head of the left operand. -/
+@[simp, grind =] lemma head_append (p q : VertexSeq α) :
+    (p.append q).head = p.head := by
+  fun_induction append <;> simp_all [head]
+
+/-- Appending a singleton on the right yields `x` as the new tail. -/
+@[simp, grind =] lemma tail_append_singleton (p : VertexSeq α) (x : α) :
+    (p.append (.singleton x)).tail = x := by
+  grind
+
+/-- Appending on the left of a singleton makes `x` the new head. -/
+@[simp, grind =] lemma head_singleton_append (p : VertexSeq α) (x : α) :
+    ((VertexSeq.singleton x).append p).head = x := by
+  grind
+
+/-- `append` is associative. -/
+@[simp, grind =] lemma append_assoc (p q r : VertexSeq α) :
+    (p.append q).append r = p.append (q.append r) := by
+  fun_induction append q r <;> simp_all [append]
+
+/-- Reversing a singleton leaves it unchanged. -/
+@[grind =] lemma reverse_singleton (v : α) :
+    (VertexSeq.singleton v).reverse = .singleton v := rfl
+
+/-- Reverse distributes over `append`, swapping the order of operands. -/
+@[simp, grind =] lemma reverse_append (p q : VertexSeq α) :
+    (p.append q).reverse = q.reverse.append p.reverse := by
+  fun_induction append <;> simp_all [reverse]
+
+/-- `reverse` is an involution. -/
+@[simp, grind =] lemma reverse_reverse (p : VertexSeq α) :
+    p.reverse.reverse = p := by
+  fun_induction reverse p <;> grind
+
+/-- The head of the reverse is the tail of the original. -/
+@[simp, grind =] lemma head_reverse (p : VertexSeq α) :
+    p.reverse.head = p.tail := by
+  fun_induction reverse p <;> grind
+
+/-- The tail of the reverse is the head of the original. -/
+@[simp, grind =] lemma tail_reverse (p : VertexSeq α) :
+    p.reverse.tail = p.head := by
+  fun_induction reverse p <;> grind
+
+/-- Dropping the tail does not affect the head. -/
+@[simp, grind =] lemma head_dropTail (p : VertexSeq α) :
+    p.dropTail.head = p.head := by
+  fun_induction reverse p <;> grind
+
+/-! ## takeUntil, dropUntil, loopErase -/
+
+/-- Take vertices until the first occurrence of `v` (including `v`). -/
+@[simp, grind] def takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : VertexSeq α :=
+  match w with
+  | .singleton x => .singleton x
+  | .cons w2 x =>
+    if h2 : v ∈ w2.toList then takeUntil w2 v h2
+    else .cons w2 x
+
+/-- Drop vertices until the last occurrence of `v` (not including `v`). -/
+@[simp, grind] def dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : VertexSeq α :=
+  match w with
+  | .singleton x => .singleton x
+  | .cons w2 x =>
+    if h2 : v ∈ w2.toList then .cons (dropUntil w2 v h2) x
+    else .singleton x
+
+/-- `takeUntil` never increases the length. -/
+@[simp] lemma length_takeUntil_le [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (w.takeUntil v h).length ≤ w.length := by
+  fun_induction takeUntil w v h <;> grind
+
+/-- `dropUntil` never increases the length. -/
+@[simp] lemma length_dropUntil_le [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (w.dropUntil v h).length ≤ w.length := by
+  fun_induction dropUntil w v h <;> grind
+
+/-- `takeUntil` preserves the head. -/
+@[simp, grind =] lemma head_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (takeUntil w v h).head = w.head := by
+  induction w <;> grind
+
+/-- The tail of `takeUntil w v h` is the target vertex `v`. -/
+@[simp, grind =] lemma tail_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (takeUntil w v h).tail = v := by
+  induction w <;> grind
+
+/-- Membership in `takeUntil` implies membership in the original sequence. -/
+@[simp, grind →] lemma mem_takeUntil [DecidableEq α] (w : VertexSeq α)
+    (v x : α) (h : v ∈ w.toList) :
+    x ∈ (takeUntil w v h).toList → x ∈ w.toList := by
+  induction w generalizing v <;> grind
+
+/-- The head of `dropUntil w v h` is the target vertex `v`. -/
+@[simp, grind =] lemma head_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (w.dropUntil v h).head = v := by
+  induction w <;> grind
+
+/-- `dropUntil` preserves the tail. -/
+@[simp, grind =] lemma tail_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (w.dropUntil v h).tail = w.tail := by
+  fun_induction VertexSeq.dropUntil w v h <;> simp [VertexSeq.tail]
+
+/-- Membership in `dropUntil` implies membership in the original sequence. -/
+@[simp, grind →] lemma mem_dropUntil [DecidableEq α] (w : VertexSeq α) (v x : α)
+    (h : v ∈ w.toList) :
+    x ∈ (w.dropUntil v h).toList → x ∈ w.toList := by
+  induction w generalizing v <;> grind
+
+/-- Self-loop erasure: scan the sequence and, whenever the current vertex
+already appears earlier, drop the intermediate detour. The result has the
+same `head` and `tail` and is `Nodup` (see `head_loopErase`, `tail_loopErase`,
+`nodup_loopErase`). -/
+@[grind] def loopErase [DecidableEq α] : VertexSeq α → VertexSeq α
+  | .singleton v => .singleton v
+  | .cons w v =>
+      if h : v ∈ w.toList then
+        loopErase (takeUntil w v h)
+      else
+        .cons (loopErase w) v
+  termination_by p => p.length
+  decreasing_by
+  · simp [length]
+    grind [length_takeUntil_le]
+  · simp [length]
+
+/-- Membership in `loopErase` implies membership in the original sequence. -/
+lemma mem_loopErase [DecidableEq α] (w : VertexSeq α) :
+    ∀ {x : α}, x ∈ w.loopErase.toList → x ∈ w.toList := by
+  fun_induction loopErase w <;> grind [toList, mem_takeUntil]
+
+/-- The vertex list produced by `loopErase` has no duplicates. -/
+theorem nodup_loopErase [DecidableEq α] (w : VertexSeq α) :
+    w.loopErase.toList.Nodup := by
+  fun_induction VertexSeq.loopErase w <;> grind [toList, mem_loopErase]
+
+/-- `loopErase` preserves the head. -/
+@[simp] lemma head_loopErase [DecidableEq α] (w : VertexSeq α) :
+    w.loopErase.head = w.head := by
+  fun_induction loopErase w <;> grind
+
+/-- `loopErase` preserves the tail. -/
+@[simp] lemma tail_loopErase [DecidableEq α] (w : VertexSeq α) :
+    w.loopErase.tail = w.tail := by
+  fun_induction loopErase w <;> grind
+
+end VertexSeq
+
+/-! ## IsWalk, Walk core data -/
+
+/-- A `VertexSeq` is a walk when consecutive vertices differ (no immediate
+backtracking). The predicate is graph-agnostic, and downstream files can
+specialise it by adding an adjacency hypothesis. -/
+@[grind] inductive IsWalk : VertexSeq α → Prop
+  | singleton (v : α) : IsWalk (.singleton v)
+  | cons (w : VertexSeq α) (u : α)
+      (hw : IsWalk w)
+      (hneq : w.tail ≠ u) :
+      IsWalk (.cons w u)
+
+grind_pattern IsWalk.singleton => IsWalk (.singleton v)
+grind_pattern IsWalk.cons => IsWalk (.cons w u)
+
+/-- A walk is a `VertexSeq` satisfying the `IsWalk` predicate. -/
+def Walk (α : Type*) := { w : VertexSeq α // IsWalk w }
+
+namespace Walk
+open VertexSeq
+
+/-! ## Basic `IsWalk` helper lemmas -/
+
+/-- A `cons` walk has a walk as its prefix. -/
+@[simp, grind =>] lemma isWalk_of_cons (w2 : VertexSeq α) (v : α)
+    (valid : IsWalk (w2.cons v)) : IsWalk w2 := by
+  grind
+
+/-- The tail of the prefix of a `cons` walk differs from the new head. -/
+@[simp, grind <=] lemma tail_ne_of_isWalk_cons (w2 : VertexSeq α) (v : α)
+    (valid : IsWalk (w2.cons v)) : w2.tail ≠ v := by
+  grind
+
+/-- The concatenation of two walks meeting at distinct endpoints is a walk. -/
+@[grind ←]
+lemma isWalk_append (w1 w2 : VertexSeq α)
+    (h1 : IsWalk w1) (h2 : IsWalk w2) (hneq : w1.tail ≠ w2.head) :
+    IsWalk (w1.append w2) := by
+  fun_induction w1.append w2 <;> grind
+
+/-- Prepending a singleton with a distinct vertex preserves the walk property. -/
+@[grind ←]
+theorem isWalk_singleton_append (p : VertexSeq α) (v : α)
+    (h : IsWalk p) (h2 : p.head ≠ v) :
+    IsWalk ((VertexSeq.singleton v).append p) := by grind
+
+/-- An `append` being a walk implies both factors are walks and the joining
+endpoints differ. -/
+@[grind →]
+theorem isWalk_of_append (p q : VertexSeq α) (h : IsWalk (p.append q)) :
+    IsWalk p ∧ IsWalk q ∧ p.tail ≠ q.head := by
+  fun_induction append <;> grind
+
+/-- `IsWalk` is preserved by reversal in either direction. -/
+@[simp, grind =]
+lemma isWalk_reverse_iff (w : VertexSeq α) : IsWalk w.reverse ↔ IsWalk w := by
+  fun_induction reverse <;> grind
+
+/-- A sequence with distinct vertices is automatically a walk. -/
+lemma isWalk_of_nodup (w : VertexSeq α) (h : w.toList.Nodup) : IsWalk w := by
+  induction w <;> grind
+
+/-- `takeUntil` of a walk is a walk. -/
+@[grind →]
+lemma isWalk_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) (hw : IsWalk w) :
+    IsWalk (w.takeUntil v h) := by
+  induction hw generalizing v <;> grind
+
+/-- `dropUntil` of a walk is a walk. -/
+@[grind →]
+lemma isWalk_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) (hw : IsWalk w) :
+    IsWalk (w.dropUntil v h) := by
+  induction hw generalizing v <;> grind
+
+/-- `loopErase` always produces a walk (its underlying list is `Nodup`). -/
+lemma isWalk_loopErase [DecidableEq α] (w : VertexSeq α) : IsWalk w.loopErase := by
+  grind [isWalk_of_nodup, nodup_loopErase]
+
+/-! ## support, head, tail, length, dropTail for Walk -/
+
+/-- The list of vertices visited by the walk, in order. -/
+@[simp, grind] def support (w : Walk α) : List α := w.val.toList
+
+/-- The first vertex of the walk. -/
+abbrev head (w : Walk α) : α := w.val.head
+
+/-- The last vertex of the walk. -/
+abbrev tail (w : Walk α) : α := w.val.tail
+
+/-- The number of edges in the walk. -/
+abbrev length (w : Walk α) : ℕ := w.val.length
+
+/-- Drop the last vertex of the walk. -/
+abbrev dropTail (w : Walk α) : Walk α :=
+  ⟨w.val.dropTail, by grind [Walk]⟩
+
+/-- Extend a walk by appending a single vertex `u` distinct from `w.tail`. -/
+def append_single (w : Walk α) (u : α) (h : u ≠ w.tail) : Walk α :=
+  ⟨w.val.cons u, by grind [Walk]⟩
+
+/-- `dropTail` preserves the head. -/
+@[simp, grind =]
+lemma head_dropTail (w : Walk α) : w.dropTail.head = w.head := by
+  obtain ⟨v, hv⟩ := w
+  induction hv <;> grind
+
+/-- If dropping the tail leaves the tail unchanged, the walk has length zero. -/
+@[simp, grind .]
+lemma length_eq_zero_of_dropTail_tail (w : Walk α) (h : w.dropTail.tail = w.tail) :
+    w.length = 0 := by
+  obtain ⟨v, hv⟩ := w
+  induction hv <;> grind
+
+/-- A walk of length zero is a singleton, so its head equals its tail. -/
+@[simp, grind ←]
+lemma head_eq_tail_of_length_zero (w : Walk α) (h : w.length = 0) :
+    w.head = w.tail := by
+  obtain ⟨v, hv⟩ := w
+  induction hv <;> grind
+
+/-! ## Walk append, reverse and related lemmas -/
+
+/-- The sequence-level concatenation of two walks (under the meeting condition)
+is itself a walk. -/
+@[grind ←]
+lemma isWalk_seq_append (w1 w2 : Walk α) (hneq : w1.tail ≠ w2.head) :
+    IsWalk (w1.val.append w2.val) := by
+  obtain ⟨_, h1⟩ := w1
+  obtain ⟨_, h2⟩ := w2
+  grind
+
+/-- Concatenate two walks meeting at a shared vertex (`w1.tail = w2.head`).
+The duplicated joining vertex is collapsed by dropping the tail of `w1`. -/
+@[grind =]
+def append (w1 w2 : Walk α) (h : w1.tail = w2.head) : Walk α :=
+  if h1 : w1.length = 0 then w2
+  else
+    ⟨w1.dropTail.val.append w2.val, by grind [Walk]⟩
+
+/-- Reverse a walk: head and tail are swapped. -/
+@[grind =]
+def reverse (w : Walk α) : Walk α :=
+  ⟨w.val.reverse, by grind [Walk]⟩
+
+/-- The head of a reversed walk is the original tail. -/
+@[simp, grind =] lemma head_reverse (w : Walk α) :
+    w.reverse.head = w.tail := by grind
+
+/-- The tail of a reversed walk is the original head. -/
+@[simp, grind =] lemma tail_reverse (w : Walk α) :
+    w.reverse.tail = w.head := by grind
+
+/-- The head of an append is the head of the left walk. -/
+@[simp, grind =] lemma head_append (w1 w2 : Walk α) (h : w1.tail = w2.head) :
+    (Walk.append w1 w2 h).head = w1.head := by
+  obtain ⟨_, hv⟩ := w1
+  induction hv <;> grind
+
+/-- The tail of an append is the tail of the right walk. -/
+@[simp, grind =] lemma tail_append (w1 w2 : Walk α) (h : w1.tail = w2.head) :
+    (Walk.append w1 w2 h).tail = w2.tail := by grind
+
+/-- Length of an `append` adds the lengths (the duplicated joining vertex is
+absorbed by dropping the tail of `w1`). -/
+@[simp, grind =] lemma length_append (w1 w2 : Walk α) (h : w1.tail = w2.head) :
+    (Walk.append w1 w2 h).length = w1.length + w2.length := by
+  unfold Walk.append
+  by_cases h1 : w1.length = 0
+  · grind
+  · have hdrop : w1.dropTail.length + 1 = w1.length := by
+      obtain ⟨_, hv⟩ := w1
+      induction hv <;> grind
+    grind
+
+/-! ## Path, cycle -/
+
+/-- A walk is a *path* when its support has no repeated vertices. -/
+def IsPath (w : Walk α) : Prop := w.val.toList.Nodup
+
+/-- A path is a walk satisfying `IsPath`. -/
+def Path (α : Type*) := { w : Walk α // IsPath w }
+
+/-- The underlying walk of a path coerces to the path itself. -/
+abbrev Path.head (p : Path α) : α := p.val.head
+abbrev Path.tail (p : Path α) : α := p.val.tail
+abbrev Path.length (p : Path α) : ℕ := p.val.length
+abbrev Path.support (p : Path α) : List α := p.val.support
+
+/-- Erase self-loops from a walk to obtain a path with the same endpoints. -/
+def toPath [DecidableEq α] (w : Walk α) : Path α :=
+  ⟨⟨w.val.loopErase, isWalk_loopErase w.val⟩, by
+    unfold IsPath; simpa using nodup_loopErase w.val⟩
+
+/-- `toPath` always produces a path. -/
+theorem toPath_isPath [DecidableEq α] (w : Walk α) : IsPath (toPath w).val := by
+  unfold IsPath toPath
+  simpa using nodup_loopErase w.val
+
+/-- `toPath` preserves the tail. -/
+lemma tail_toPath [DecidableEq α] (w : Walk α) : (toPath w).tail = w.tail := by
+  show (toPath w).val.val.tail = w.val.tail
+  grind [tail_loopErase, toPath]
+
+/-- `toPath` preserves the head. -/
+lemma head_toPath [DecidableEq α] (w : Walk α) : (toPath w).head = w.head := by
+  show (toPath w).val.val.head = w.val.head
+  grind [head_loopErase, toPath]
+
+/-- A walk is a *cycle* if it has length at least 3, its endpoints coincide,
+and the walk obtained by dropping its last vertex is a path. -/
+def IsCycle (w : Walk α) : Prop :=
+  3 ≤ w.length ∧ w.head = w.tail ∧ IsPath w.dropTail
+
+/-- A cycle is a walk satisfying `IsCycle`. -/
+def Cycle (α : Type*) := { w : Walk α // IsCycle w }
+
+abbrev Cycle.head (c : Cycle α) : α := c.val.head
+abbrev Cycle.tail (c : Cycle α) : α := c.val.tail
+abbrev Cycle.length (c : Cycle α) : ℕ := c.val.length
+abbrev Cycle.support (c : Cycle α) : List α := c.val.support
+
+/-! ## Some more helper lemmas -/
+
+/-- `takeUntil` at the head of a sequence yields just the singleton head. -/
+@[simp, grind .] lemma takeUntil_head [DecidableEq α] (w : VertexSeq α)
+    (h : w.head ∈ w.toList) :
+    w.takeUntil w.head h = VertexSeq.singleton w.head := by
+  induction w <;> grind
+
+/-- `dropUntil` at the head of a sequence returns the whole sequence. -/
+@[simp, grind .] lemma dropUntil_head [DecidableEq α] (w : VertexSeq α)
+    (h : w.head ∈ w.toList) :
+    w.dropUntil w.head h = w := by
+  induction w <;> grind
+
+/-- Splitting a sequence at an interior vertex `v` and rejoining via `append`
+reconstructs the original. -/
+@[simp, grind →] lemma dropTail_takeUntil_append_dropUntil [DecidableEq α]
+    (w : VertexSeq α) (v : α) (h : v ∈ w.toList) (hne : v ≠ w.head) :
+    (w.takeUntil v h).dropTail.append (w.dropUntil v h) = w := by
+  induction w generalizing v <;> grind
+
+/-- A walk can be reconstructed as the `append` of its prefix up to a chosen
+vertex `u ∈ w.support` and its suffix from `u`. -/
+@[simp, grind →] lemma eq_append_takeUntil_dropUntil [DecidableEq α]
+    (w : Walk α) (u : α) (hu : u ∈ w.support) :
+    w = Walk.append
+      ⟨w.val.takeUntil u hu, isWalk_takeUntil w.val u hu w.property⟩
+      ⟨w.val.dropUntil u hu, isWalk_dropUntil w.val u hu w.property⟩
+      (by grind) := by
+  by_cases h : u = w.head
+  · apply Subtype.ext
+    grind
+  · apply Subtype.ext
+    grind
+
+/-! ## Re-rooting a cycle -/
+
+/-- Re-root a cycle at any chosen vertex in its support. -/
+@[simp, grind] def rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
+    (u : α) (hu : u ∈ w.support) : Walk α :=
+  Walk.append
+    ⟨w.val.dropUntil u hu, isWalk_dropUntil w.val u hu w.property⟩
+    ⟨w.val.takeUntil u hu, isWalk_takeUntil w.val u hu w.property⟩
+    (by
+      rcases hcyc with ⟨_, hht, _⟩
+      grind)
+
+/-- `toList` of an `append` concatenates the two lists in order. Because
+`cons` extends on the right, the right operand's vertices follow the left
+operand's. -/
+@[simp, grind =] lemma toList_append (p q : VertexSeq α) :
+    (p.append q).toList = p.toList ++ q.toList := by
+  induction q generalizing p <;> grind
+
+/-- Dropping the tail commutes with `append` as long as the right walk is not
+collapsed to a singleton. -/
+lemma dropTail_append (w1 w2 : Walk α) (h : w1.tail = w2.head)
+    (hlen : w2.head ≠ w2.tail) :
+    (Walk.append w1 w2 h).dropTail = Walk.append w1 w2.dropTail (by grind) := by
+  by_cases h1 : w1.length = 0
+  · grind
+  · apply Subtype.ext
+    obtain ⟨_, hv⟩ := w2
+    induction hv <;> grind
+
+/-- Re-rooting a cycle at any vertex on it yields another cycle. -/
+lemma isCycle_rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
+    (u : α) (hu : u ∈ w.support) :
+    IsCycle (rerootCycle w hcyc u hu) := by
+  have h2 : w.length = (w.rerootCycle hcyc u hu).length := by grind
+  rcases hcyc with ⟨hlen, hht, hpath⟩
+  refine ⟨?_, ?_, ?_⟩
+  · grind
+  · grind
+  · by_cases h : u = w.head
+    · have hz : w.length ≠ 0 := by omega
+      grind
+    · grind [dropTail_append, IsPath, support, Walk.append,
+              VertexSeq.toList, head_dropTail,
+              VertexSeq.tail_takeUntil, VertexSeq.head_dropUntil,
+              VertexSeq.tail_dropUntil, VertexSeq.head_takeUntil,
+              toList_append, dropTail_takeUntil_append_dropUntil]
+
+end Walk
diff --git a/GraphLib/Theory/Walks/InDiGraph.lean b/GraphLib/Theory/Walks/InDiGraph.lean
new file mode 100644
index 0000000..3f7adff
--- /dev/null
+++ b/GraphLib/Theory/Walks/InDiGraph.lean
@@ -0,0 +1,320 @@
+/-
+Copyright (c) 2026 Basil Rohner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner
+-/
+import GraphLib.Theory.Walks.Basic
+import GraphLib.Graph.Subgraph
+
+/-!
+# Walks in a `SimpleDiGraph`
+
+This file specialises the graph-agnostic walk theory of
+`GraphLib.Theory.Walks.Basic` to walks in a simple directed graph. A
+`VertexSeq` or `Walk` is "in `G`" when its starting vertex belongs to
+`V(G)` and every directed edge it traverses — taken in walking order —
+belongs to `E(G)`; this is captured by the predicate
+`VertexSeq.IsVertexSeqInDi`. The file then shows that the predicate is
+preserved under the basic walk operations (`append`, `dropTail`,
+`takeUntil`, `loopErase`/`toPath`) and is monotone with respect to
+passing to a supergraph.
+
+## Main definitions
+
+* `VertexSeq.IsVertexSeqInDi G w` — `w` is a vertex sequence in the
+  simple directed graph `G`.
+* `VertexSeq.dirEdgeSet w` — the directed edges traversed by `w`, as a
+  `Set (α × α)`.
+* `Walk.dirEdgeSet w` — the directed edges traversed by the walk `w`.
+
+## Main statements
+
+* `VertexSeq.isVertexSeqInDi_iff` — `w` is in `G` iff `w.head ∈ V(G)` and
+  `w.dirEdgeSet ⊆ E(G)`.
+* `Walk.isVertexSeqInDi_singleton_append`, `Walk.isVertexSeqInDi_dropTail`,
+  `Walk.isVertexSeqInDi_takeUntil`, `Walk.isVertexSeqInDi_append`,
+  `Walk.isVertexSeqInDi_walkAppend` — the predicate is closed under the
+  corresponding walk operations.
+* `Walk.isVertexSeqInDi_toPath` — loop-erasing a walk preserves the
+  predicate, so every walk in `G` admits a path in `G` between the same
+  endpoints.
+* `Walk.isVertexSeqInDi_mono` — the predicate is monotone in the graph.
+
+## Design choices
+
+* **Mirror of `InSimpleGraph.lean`.** This file is the directed analogue
+  of `GraphLib.Theory.Walks.InSimpleGraph`. The only substantive
+  difference is that edges are ordered pairs `(u, v) : α × α` rather
+  than `Sym2 α`. The underlying combinatorics (`takeUntil`,
+  `loopErase`, …) come from `Basic.lean` and are shared verbatim.
+* **No `reverse` lemma.** Walking is directional, so reversing a walk
+  produces a sequence whose consecutive pairs are the original edges
+  with swapped endpoints; these need not belong to `E(G)`. The
+  `reverse` family of lemmas from `InSimpleGraph.lean` therefore has
+  no analogue here. A statement about walks in the *reverse* digraph
+  would require an `SimpleDiGraph.reverse` constructor first.
+* **`Di` suffix on conflicting names.** `IsVertexSeqInDi` and
+  `dirEdgeSet` are renamed (rather than overloaded in the `VertexSeq`
+  namespace) because Lean cannot dispatch `def`/`inductive` on a
+  parameter type alone. This keeps the simple-graph and simple-digraph
+  specialisations interoperable in a single import.
+* **`grind`-driven proofs.** As in `InSimpleGraph.lean`, most lemmas
+  close by `grind` with the inductive constructors as `@[grind]`
+  patterns; closure lemmas are tagged `@[grind →]` for downstream
+  chaining.
+-/
+
+set_option tactic.hygienic false
+set_option linter.unusedSectionVars false
+
+variable {α : Type*} [DecidableEq α]
+
+open scoped GraphLib
+open GraphLib
+
+namespace VertexSeq
+
+/-- `IsVertexSeqInDi G w` records that the vertex sequence `w` is a
+sequence in the simple directed graph `G`: every vertex of `w` lies in
+`V(G)` and every two consecutive vertices `(u, v)` (in walking order)
+form a directed edge of `G`. Defined inductively matching the
+`singleton`/`cons` shape of `VertexSeq`. -/
+@[grind] inductive IsVertexSeqInDi (G : SimpleDiGraph α) : VertexSeq α → Prop
+  /-- A singleton sequence is in `G` iff its vertex is a vertex of `G`. -/
+  | singleton (v : α) (hv : v ∈ V(G)) : IsVertexSeqInDi G (.singleton v)
+  /-- Right-extending a sequence in `G` by a vertex `u` keeps it in `G`
+  provided the directed edge `(w.tail, u)` is an edge of `G`. -/
+  | cons (w : VertexSeq α) (u : α)
+      (hw : IsVertexSeqInDi G w)
+      (he : (w.tail, u) ∈ E(G)) :
+      IsVertexSeqInDi G (.cons w u)
+
+/-- The set of directed edges traversed by the vertex sequence `w`, in
+walking order. Empty for a singleton; obtained inductively by adjoining
+the new edge `(w.tail, u)` in the `cons` case. -/
+abbrev dirEdgeSet (w : VertexSeq α) : Set (α × α) :=
+  match w with
+  | .singleton _ => ∅
+  | .cons w u => w.dirEdgeSet ∪ {(w.tail, u)}
+
+/-- Working characterisation of `IsVertexSeqInDi`: `w` is a sequence in
+`G` iff its starting vertex belongs to `V(G)` and every directed edge
+it traverses belongs to `E(G)`. -/
+lemma isVertexSeqInDi_iff (G : SimpleDiGraph α) (w : VertexSeq α) :
+    IsVertexSeqInDi G w ↔ w.head ∈ V(G) ∧ w.dirEdgeSet ⊆ E(G) := by
+  induction w <;> grind
+
+/-- Truncating a sequence at the first occurrence of `v` only drops
+directed edges: the dir-edge set of `w.takeUntil v h` is contained in
+the dir-edge set of `w`. -/
+lemma dirEdgeSet_takeUntil_subset (w : VertexSeq α) (v : α) (h : v ∈ w.toList) :
+    (w.takeUntil v h).dirEdgeSet ⊆ w.dirEdgeSet := by
+  induction w generalizing v
+  · intro a ha; simp [takeUntil] at ha
+  · by_cases h2 : v ∈ w_1.toList
+    · grind
+    · simp [takeUntil, h2]
+
+/-- Loop-erasing a sequence only drops directed edges: the dir-edge set
+of `w.loopErase` is contained in the dir-edge set of `w`. Used
+downstream to lift dir-edge-set hypotheses from a walk to its associated
+path. -/
+lemma dirEdgeSet_loopErase_subset (w : VertexSeq α) :
+    w.loopErase.dirEdgeSet ⊆ w.dirEdgeSet := by
+  suffices h : ∀ n : ℕ, ∀ w : VertexSeq α,
+      w.length = n → w.loopErase.dirEdgeSet ⊆ w.dirEdgeSet by grind
+  intro n; refine Nat.strong_induction_on n ?_
+  intro n ih w hlen; cases w
+  · intro a ha; simp [loopErase, dirEdgeSet] at ha
+  · by_cases hmem : v ∈ w_1.toList
+    · grind [dirEdgeSet_takeUntil_subset, length_takeUntil_le]
+    · intro a ha
+      have ha' : a = (w_1.loopErase.tail, v) ∨ a ∈ w_1.loopErase.dirEdgeSet := by
+        simpa [loopErase, hmem] using ha
+      grind [tail_loopErase]
+
+end VertexSeq
+
+namespace Walk
+open VertexSeq
+
+/-- The set of directed edges traversed by the walk `w`, defined to be
+the dir-edge set of its underlying vertex sequence. -/
+abbrev dirEdgeSet (w : Walk α) : Set (α × α) := w.val.dirEdgeSet
+
+/-- Loop-erasing a walk only drops directed edges: the dir-edge set of
+`w.toPath` is contained in the dir-edge set of `w`. -/
+lemma dirEdgeSet_toPath_subset (w : Walk α) :
+    w.toPath.val.dirEdgeSet ⊆ w.dirEdgeSet := by
+  simpa [dirEdgeSet] using VertexSeq.dirEdgeSet_loopErase_subset w.val
+
+/-- Working characterisation of `IsVertexSeqInDi` for a `Walk`: `w` is in
+`G` iff its starting vertex belongs to `V(G)` and every directed edge it
+traverses belongs to `E(G)`. -/
+lemma isVertexSeqInDi_iff (G : SimpleDiGraph α) (w : Walk α) :
+    IsVertexSeqInDi G w.val ↔ w.head ∈ V(G) ∧ w.dirEdgeSet ⊆ E(G) := by
+  grind [VertexSeq.isVertexSeqInDi_iff]
+
+/-- If `w` is a sequence in `G` and there is a directed edge
+`(u, w.head) ∈ E(G)`, then prepending the singleton `u` to `w` yields a
+sequence in `G`. -/
+@[grind →]
+lemma isVertexSeqInDi_singleton_append (G : SimpleDiGraph α) (w : VertexSeq α)
+    (hw : IsVertexSeqInDi G w) (u : α) (hedg : (u, w.head) ∈ E(G)) :
+    IsVertexSeqInDi G ((VertexSeq.singleton u).append w) := by
+  revert hedg
+  induction hw with
+  | singleton v hv =>
+      intro hedg
+      refine IsVertexSeqInDi.cons (VertexSeq.singleton u) v ?_ (by simpa using hedg)
+      have hu : u ∈ V(G) := (G.incidence (by simpa using hedg)).1
+      exact IsVertexSeqInDi.singleton u hu
+  | cons w0 u0 hw0 he ih =>
+      intro hedg
+      have happ : ((VertexSeq.singleton u).append (w0.cons u0))
+          = ((VertexSeq.singleton u).append w0).cons u0 := rfl
+      rw [happ]
+      have hedg' : (u, w0.head) ∈ E(G) := by simpa using hedg
+      refine IsVertexSeqInDi.cons _ _ (ih hedg') ?_
+      simpa using he
+
+/-- Dropping the last vertex of a sequence preserves the "in `G`"
+property. -/
+@[grind →]
+lemma isVertexSeqInDi_dropTail (G : SimpleDiGraph α) (w : VertexSeq α)
+    (hw : IsVertexSeqInDi G w) :
+    IsVertexSeqInDi G w.dropTail := by
+  cases hw with
+  | singleton v hv => simpa [VertexSeq.dropTail] using IsVertexSeqInDi.singleton v hv
+  | cons w0 u hw0 _ => simpa [VertexSeq.dropTail] using hw0
+
+/-- Dropping the last vertex of a walk preserves both the "in `G`"
+property and the `IsWalk` condition. -/
+lemma isVertexSeqInDi_and_isWalk_dropTail (G : SimpleDiGraph α) (w : VertexSeq α)
+    (hw : IsVertexSeqInDi G w ∧ IsWalk w) :
+    IsVertexSeqInDi G w.dropTail ∧ IsWalk w.dropTail := by
+  refine ⟨isVertexSeqInDi_dropTail G w hw.1, ?_⟩
+  cases hw.2 with
+  | singleton v => simpa [VertexSeq.dropTail] using IsWalk.singleton v
+  | cons w0 u hw0 _ => simpa [VertexSeq.dropTail] using hw0
+
+/-- Truncating a sequence at the first occurrence of `v` preserves the
+"in `G`" property. -/
+@[grind →]
+lemma isVertexSeqInDi_takeUntil (G : SimpleDiGraph α)
+    (w : VertexSeq α) (v : α) (h : v ∈ w.toList)
+    (hw_in : IsVertexSeqInDi G w) :
+    IsVertexSeqInDi G (w.takeUntil v h) := by
+  induction w generalizing v with
+  | singleton x =>
+      have hvx : v = x := by simpa [VertexSeq.toList] using h
+      subst hvx
+      exact hw_in
+  | cons w0 x ih =>
+      have hw0_in : IsVertexSeqInDi G w0 := by cases hw_in; assumption
+      by_cases h2 : v ∈ w0.toList
+      · change IsVertexSeqInDi G ((w0.cons x).takeUntil v h)
+        rw [show (w0.cons x).takeUntil v h = w0.takeUntil v h2 by
+          simp [VertexSeq.takeUntil, h2]]
+        exact ih v h2 hw0_in
+      · have hv_eq : v = x := by
+          have hmem : v ∈ (w0.cons x).toList := h
+          simp [VertexSeq.toList] at hmem
+          tauto
+        subst hv_eq
+        change IsVertexSeqInDi G ((w0.cons v).takeUntil v h)
+        rw [show (w0.cons v).takeUntil v h = w0.cons v by
+          simp [VertexSeq.takeUntil, h2]]
+        exact hw_in
+
+/-- Truncating a walk at the first occurrence of `v` preserves both the
+"in `G`" property and the `IsWalk` condition. -/
+lemma isVertexSeqInDi_and_isWalk_takeUntil (G : SimpleDiGraph α)
+    (w : VertexSeq α) (v : α) (h : v ∈ w.toList)
+    (hw : IsVertexSeqInDi G w ∧ IsWalk w) :
+    IsVertexSeqInDi G (w.takeUntil v h) ∧ IsWalk (w.takeUntil v h) :=
+  ⟨isVertexSeqInDi_takeUntil G w v h hw.1, isWalk_takeUntil w v h hw.2⟩
+
+/-- Being a sequence in a subgraph implies being a sequence in the
+ambient graph (monotonicity in the graph argument). -/
+@[grind →]
+lemma isVertexSeqInDi_mono {H G : SimpleDiGraph α} (w : VertexSeq α)
+    (hw : IsVertexSeqInDi H w) (hsub : SimpleDiGraph.subgraphOf H G) :
+    IsVertexSeqInDi G w := by
+  induction hw with
+  | singleton v hv => exact IsVertexSeqInDi.singleton v (hsub.1 hv)
+  | cons w0 u hw0 he ih => exact IsVertexSeqInDi.cons w0 u ih (hsub.2 he)
+
+/-- Monotonicity of "is a walk in `G`" along subgraph inclusion. -/
+lemma isVertexSeqInDi_and_isWalk_mono {H G : SimpleDiGraph α} (w : VertexSeq α)
+    (hw : IsVertexSeqInDi H w ∧ IsWalk w) (hsub : SimpleDiGraph.subgraphOf H G) :
+    IsVertexSeqInDi G w ∧ IsWalk w :=
+  ⟨isVertexSeqInDi_mono w hw.1 hsub, hw.2⟩
+
+/-- Concatenating two sequences in `G` along a connecting directed edge
+gives a sequence in `G`. -/
+lemma isVertexSeqInDi_append (G : SimpleDiGraph α)
+    (w1 w2 : VertexSeq α)
+    (h1 : IsVertexSeqInDi G w1) (h2 : IsVertexSeqInDi G w2)
+    (hedg : (w1.tail, w2.head) ∈ E(G)) :
+    IsVertexSeqInDi G (w1.append w2) := by
+  induction h2 generalizing w1 with
+  | singleton v hv =>
+      rw [show w1.append (VertexSeq.singleton v) = w1.cons v from rfl]
+      refine IsVertexSeqInDi.cons w1 v h1 ?_
+      simpa using hedg
+  | cons w0 u hw0 he ih =>
+      rw [show w1.append (w0.cons u) = (w1.append w0).cons u from rfl]
+      refine IsVertexSeqInDi.cons (w1.append w0) u (ih w1 h1 hedg) ?_
+      have : (w1.append w0).tail = w0.tail := VertexSeq.tail_append w1 w0
+      rw [this]; exact he
+
+/-- Concatenating two walks in `G` meeting at a common vertex gives a
+walk in `G`. -/
+lemma isVertexSeqInDi_walkAppend (G : SimpleDiGraph α)
+    (w1 w2 : Walk α)
+    (h1 : IsVertexSeqInDi G w1.val) (h2 : IsVertexSeqInDi G w2.val)
+    (h : w1.tail = w2.head) :
+    IsVertexSeqInDi G (Walk.append w1 w2 h).val := by
+  unfold Walk.append
+  by_cases hlen : w1.length = 0
+  · simp only [hlen, dite_true]; exact h2
+  · simp only [hlen, dite_false]
+    refine isVertexSeqInDi_append G w1.val.dropTail w2.val
+      (isVertexSeqInDi_dropTail G w1.val h1) h2 ?_
+    obtain ⟨w0, u, hwseq⟩ : ∃ (w0 : VertexSeq α) (u : α), w1.val = w0.cons u := by
+      match hseq : w1.val with
+      | .singleton v =>
+          exfalso
+          apply hlen
+          change w1.val.length = 0
+          rw [hseq]; rfl
+      | .cons w0 u => exact ⟨w0, u, rfl⟩
+    have hh1 : IsVertexSeqInDi G (w0.cons u) := hwseq ▸ h1
+    have hedg' : (w0.tail, u) ∈ E(G) := by
+      cases hh1 with
+      | cons _ _ _ he => exact he
+    have hdrop_tail : w1.val.dropTail.tail = w0.tail := by rw [hwseq]; rfl
+    have hhead_eq : w2.val.head = u := by
+      change w2.head = u
+      rw [← h]
+      change w1.val.tail = u
+      rw [hwseq]; rfl
+    rw [hdrop_tail, hhead_eq]
+    exact hedg'
+
+/-- Loop-erasing a walk preserves the "in `G`" property: every walk in
+`G` yields a path in `G` between the same endpoints. -/
+lemma isVertexSeqInDi_toPath (G : SimpleDiGraph α) (w : Walk α)
+    (hw : IsVertexSeqInDi G w.val) :
+    IsVertexSeqInDi G w.toPath.val.val := by
+  rw [VertexSeq.isVertexSeqInDi_iff] at hw
+  rw [VertexSeq.isVertexSeqInDi_iff]
+  refine ⟨?_, ?_⟩
+  · have : w.toPath.head = w.head := head_toPath w
+    change w.toPath.head ∈ V(G)
+    rw [this]
+    exact hw.1
+  · exact (dirEdgeSet_toPath_subset w).trans hw.2
+
+end Walk
diff --git a/GraphLib/Theory/Walks/InGraph.lean b/GraphLib/Theory/Walks/InGraph.lean
new file mode 100644
index 0000000..2770fec
--- /dev/null
+++ b/GraphLib/Theory/Walks/InGraph.lean
@@ -0,0 +1,342 @@
+/-
+Copyright (c) 2026 Sorrachai Yingchareonthawornchai. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan
+-/
+import GraphLib.Theory.Walks.Basic
+import GraphLib.Graph.Subgraph
+
+/-!
+# Walks in a `SimpleGraph`
+
+This file specialises the graph-agnostic walk theory of
+`GraphLib.Theory.Walks.Basic` to walks in a simple graph. A `VertexSeq`
+or `Walk` is "in `G`" when its starting vertex belongs to `V(G)` and every
+edge it traverses belongs to `E(G)`; this is captured by the predicate
+`VertexSeq.IsVertexSeqIn`. The file then shows that the predicate is
+preserved under all the basic walk operations (`append`, `reverse`,
+`dropTail`, `takeUntil`, `loopErase`/`toPath`) and is monotone with
+respect to passing to a supergraph.
+
+## Main definitions
+
+* `VertexSeq.IsVertexSeqIn G w` — `w` is a vertex sequence in `G`.
+* `VertexSeq.edgeSet w` — the edges traversed by `w`, as a `Set (Sym2 α)`.
+* `Walk.edgeSet w` — the edges traversed by the walk `w`.
+
+The subgraph relation `SimpleGraph.subgraphOf` used in the monotonicity
+results below is defined in `GraphLib.Graph.Subgraph`.
+
+## Main statements
+
+* `VertexSeq.isVertexSeqIn_iff` — `w` is in `G` iff `w.head ∈ V(G)` and
+  `w.edgeSet ⊆ E(G)`. This is the working characterisation used by the
+  rest of the file.
+* `Walk.isVertexSeqIn_singleton_append`, `Walk.isVertexSeqIn_reverse`,
+  `Walk.isVertexSeqIn_dropTail`, `Walk.isVertexSeqIn_takeUntil`,
+  `Walk.isVertexSeqIn_append`, `Walk.isVertexSeqIn_walkAppend` — the
+  predicate is closed under the corresponding walk operations.
+* `Walk.isVertexSeqIn_toPath` — loop-erasing a walk preserves the
+  predicate, so every walk in `G` admits a path in `G` between the same
+  endpoints.
+* `Walk.isVertexSeqIn_mono` — the predicate is monotone in the graph.
+
+## Design choices
+
+* **Specialisation, not duplication.** `GraphLib.Theory.Walks.Basic`
+  develops the combinatorics of `VertexSeq`/`Walk` without reference to
+  any graph. This file adds the simple-graph adjacency layer on top. The
+  same pattern is intended for analogous files (`InGraph.lean`,
+  `InDiGraph.lean`, `InSimpleDiGraph.lean`) that specialise the core
+  walk API to other graph types; sharing the underlying combinatorics
+  keeps the analytic proofs (loop-erasure, reversal, ...) written once.
+* **Predicate, not refinement.** "Walk in `G`" is recorded as a
+  `Prop`-valued predicate on a bare `VertexSeq`/`Walk`, not as a new type
+  bundling the graph hypothesis. Conversions between unrestricted and
+  restricted walks are then free, which is convenient when the graph is
+  modified during a proof (e.g. edge deletion in algorithm correctness).
+* **`edgeSet` parallels `toList`.** Just as `VertexSeq.toList` records
+  the visited vertices, `VertexSeq.edgeSet` records the traversed edges
+  as a set of `Sym2 α`. The membership condition is then phrased
+  uniformly as `w.edgeSet ⊆ E(G)`, mirroring the existing edge-set
+  conventions of `SimpleGraph` in this project.
+* **`Set`, not `Finset`.** Edge sets are taken as `Set (Sym2 α)` to align
+  with `SimpleGraph.edgeSet` (also a `Set`). This avoids gratuitous
+  `Finset` machinery when no finiteness is required; downstream files
+  that need a finite edge set can convert when relevant.
+* **`grind`-driven proofs.** As in `Basic.lean`, most lemmas close by
+  `grind` together with the elementary lemmas already registered as
+  `@[grind]`. Closure lemmas are themselves tagged `@[grind →]` so that
+  later files can chain them automatically.
+-/
+
+set_option tactic.hygienic false
+set_option linter.unusedSectionVars false
+
+variable {α : Type*} [DecidableEq α]
+
+open scoped GraphLib
+open GraphLib
+
+namespace VertexSeq
+
+/-- `IsVertexSeqIn G w` records that the vertex sequence `w` is a sequence
+in the simple graph `G`: every vertex of `w` lies in `V(G)` and every two
+consecutive vertices are joined by an edge of `G`. Defined inductively
+matching the `singleton`/`cons` shape of `VertexSeq`. -/
+@[grind] inductive IsVertexSeqIn (G : SimpleGraph α) : VertexSeq α → Prop
+  /-- A singleton sequence is in `G` iff its vertex is a vertex of `G`. -/
+  | singleton (v : α) (hv : v ∈ V(G)) : IsVertexSeqIn G (.singleton v)
+  /-- Right-extending a sequence in `G` by a vertex `u` keeps it in `G`
+  provided the new edge `s(w.tail, u)` is an edge of `G`. -/
+  | cons (w : VertexSeq α) (u : α)
+      (hw : IsVertexSeqIn G w)
+      (he : s(w.tail, u) ∈ E(G)) :
+      IsVertexSeqIn G (.cons w u)
+
+/-- The set of edges traversed by the vertex sequence `w`. Empty for a
+singleton; obtained inductively by adjoining the new edge `s(w.tail, u)`
+to the previously traversed edges in the `cons` case. -/
+abbrev edgeSet (w : VertexSeq α) : Set (Sym2 α) :=
+  match w with
+  | .singleton _ => ∅
+  | .cons w u => w.edgeSet ∪ {s(w.tail, u)}
+
+/-- Working characterisation of `IsVertexSeqIn`: `w` is a sequence in `G`
+iff its starting vertex belongs to `V(G)` and every edge it traverses
+belongs to `E(G)`. -/
+lemma isVertexSeqIn_iff (G : SimpleGraph α) (w : VertexSeq α) :
+    IsVertexSeqIn G w ↔ w.head ∈ V(G) ∧ w.edgeSet ⊆ E(G) := by
+  induction w <;> grind
+
+/-- Truncating a sequence at the first occurrence of `v` only drops edges:
+the edge set of `w.takeUntil v h` is contained in the edge set of `w`. -/
+lemma edgeSet_takeUntil_subset (w : VertexSeq α) (v : α) (h : v ∈ w.toList) :
+    (w.takeUntil v h).edgeSet ⊆ w.edgeSet := by
+  induction w generalizing v
+  · intro a ha; simp [takeUntil] at ha
+  · by_cases h2 : v ∈ w_1.toList
+    · grind
+    · simp [takeUntil, h2]
+
+/-- Loop-erasing a sequence only drops edges: the edge set of `w.loopErase`
+is contained in the edge set of `w`. Used downstream to lift edge-set
+hypotheses from a walk to its associated path. -/
+lemma edgeSet_loopErase_subset (w : VertexSeq α) :
+    w.loopErase.edgeSet ⊆ w.edgeSet := by
+  suffices h : ∀ n : ℕ, ∀ w : VertexSeq α,
+      w.length = n → w.loopErase.edgeSet ⊆ w.edgeSet by grind
+  intro n; refine Nat.strong_induction_on n ?_
+  intro n ih w hlen; cases w
+  · intro a ha; simp [loopErase, edgeSet] at ha
+  · by_cases hmem : v ∈ w_1.toList
+    · grind [edgeSet_takeUntil_subset, length_takeUntil_le]
+    · intro a ha
+      have ha' : a = s(w_1.loopErase.tail, v) ∨ a ∈ w_1.loopErase.edgeSet := by
+        simpa [loopErase, hmem] using ha
+      grind [tail_loopErase]
+
+end VertexSeq
+
+namespace Walk
+open VertexSeq
+
+/-- The set of edges traversed by the walk `w`, defined to be the edge set
+of its underlying vertex sequence. -/
+abbrev edgeSet (w : Walk α) : Set (Sym2 α) := w.val.edgeSet
+
+/-- Loop-erasing a walk only drops edges: the edge set of `w.toPath` is
+contained in the edge set of `w`. -/
+lemma edgeSet_toPath_subset (w : Walk α) : w.toPath.val.edgeSet ⊆ w.edgeSet := by
+  simpa [edgeSet] using VertexSeq.edgeSet_loopErase_subset w.val
+
+/-- Working characterisation of `IsVertexSeqIn` for a `Walk`: `w` is in `G`
+iff its starting vertex belongs to `V(G)` and every edge it traverses
+belongs to `E(G)`. -/
+lemma isVertexSeqIn_iff (G : SimpleGraph α) (w : Walk α) :
+    IsVertexSeqIn G w.val ↔ w.head ∈ V(G) ∧ w.edgeSet ⊆ E(G) := by
+  grind [VertexSeq.isVertexSeqIn_iff]
+
+/-- If `w` is a sequence in `G` and there is an edge `s(u, w.head) ∈ E(G)`,
+then prepending the singleton `u` to `w` yields a sequence in `G`. -/
+@[grind →]
+lemma isVertexSeqIn_singleton_append (G : SimpleGraph α) (w : VertexSeq α)
+    (hw : IsVertexSeqIn G w) (u : α) (hedg : s(u, w.head) ∈ E(G)) :
+    IsVertexSeqIn G ((VertexSeq.singleton u).append w) := by
+  revert hedg
+  induction hw with
+  | singleton v hv =>
+      intro hedg
+      refine IsVertexSeqIn.cons (VertexSeq.singleton u) v ?_ (by simpa using hedg)
+      exact IsVertexSeqIn.singleton u (G.incidence (by simpa using hedg) (by simp))
+  | cons w0 u0 hw0 he ih =>
+      intro hedg
+      have happ : ((VertexSeq.singleton u).append (w0.cons u0))
+          = ((VertexSeq.singleton u).append w0).cons u0 := rfl
+      rw [happ]
+      have hedg' : s(u, w0.head) ∈ E(G) := by simpa using hedg
+      refine IsVertexSeqIn.cons _ _ (ih hedg') ?_
+      simpa using he
+
+/-- Reversing a sequence preserves the "in `G`" property. -/
+@[grind →]
+lemma isVertexSeqIn_reverse (G : SimpleGraph α) (w : VertexSeq α)
+    (hw : IsVertexSeqIn G w) :
+    IsVertexSeqIn G w.reverse := by
+  induction hw with
+  | singleton v hv => simpa using IsVertexSeqIn.singleton v hv
+  | cons w0 u0 hw0 he ih =>
+      have hrev : (w0.cons u0).reverse
+          = (VertexSeq.singleton u0).append w0.reverse := rfl
+      rw [hrev]
+      refine isVertexSeqIn_singleton_append G w0.reverse ih u0 ?_
+      have hh : w0.reverse.head = w0.tail := VertexSeq.head_reverse w0
+      rw [hh]
+      simpa [Sym2.eq_swap] using he
+
+/-- Reversing a walk preserves both the "in `G`" property and the
+`IsWalk` (non-stalling) condition. -/
+lemma isVertexSeqIn_and_isWalk_reverse (G : SimpleGraph α) (w : VertexSeq α)
+    (hw : IsVertexSeqIn G w ∧ IsWalk w) :
+    IsVertexSeqIn G w.reverse ∧ IsWalk w.reverse :=
+  ⟨isVertexSeqIn_reverse G w hw.1, (isWalk_reverse_iff w).mpr hw.2⟩
+
+/-- Dropping the last vertex of a sequence preserves the "in `G`" property. -/
+@[grind →]
+lemma isVertexSeqIn_dropTail (G : SimpleGraph α) (w : VertexSeq α)
+    (hw : IsVertexSeqIn G w) :
+    IsVertexSeqIn G w.dropTail := by
+  cases hw with
+  | singleton v hv => simpa [VertexSeq.dropTail] using IsVertexSeqIn.singleton v hv
+  | cons w0 u hw0 _ => simpa [VertexSeq.dropTail] using hw0
+
+/-- Dropping the last vertex of a walk preserves both the "in `G`" property
+and the `IsWalk` condition. -/
+lemma isVertexSeqIn_and_isWalk_dropTail (G : SimpleGraph α) (w : VertexSeq α)
+    (hw : IsVertexSeqIn G w ∧ IsWalk w) :
+    IsVertexSeqIn G w.dropTail ∧ IsWalk w.dropTail := by
+  refine ⟨isVertexSeqIn_dropTail G w hw.1, ?_⟩
+  cases hw.2 with
+  | singleton v => simpa [VertexSeq.dropTail] using IsWalk.singleton v
+  | cons w0 u hw0 _ => simpa [VertexSeq.dropTail] using hw0
+
+/-- Truncating a sequence at the first occurrence of `v` preserves the
+"in `G`" property. -/
+@[grind →]
+lemma isVertexSeqIn_takeUntil (G : SimpleGraph α)
+    (w : VertexSeq α) (v : α) (h : v ∈ w.toList)
+    (hw_in : IsVertexSeqIn G w) :
+    IsVertexSeqIn G (w.takeUntil v h) := by
+  induction w generalizing v with
+  | singleton x =>
+      have hvx : v = x := by simpa [VertexSeq.toList] using h
+      subst hvx
+      exact hw_in
+  | cons w0 x ih =>
+      have hw0_in : IsVertexSeqIn G w0 := by cases hw_in; assumption
+      by_cases h2 : v ∈ w0.toList
+      · change IsVertexSeqIn G ((w0.cons x).takeUntil v h)
+        rw [show (w0.cons x).takeUntil v h = w0.takeUntil v h2 by
+          simp [VertexSeq.takeUntil, h2]]
+        exact ih v h2 hw0_in
+      · have hv_eq : v = x := by
+          have hmem : v ∈ (w0.cons x).toList := h
+          simp [VertexSeq.toList] at hmem
+          tauto
+        subst hv_eq
+        change IsVertexSeqIn G ((w0.cons v).takeUntil v h)
+        rw [show (w0.cons v).takeUntil v h = w0.cons v by
+          simp [VertexSeq.takeUntil, h2]]
+        exact hw_in
+
+/-- Truncating a walk at the first occurrence of `v` preserves both the
+"in `G`" property and the `IsWalk` condition. -/
+lemma isVertexSeqIn_and_isWalk_takeUntil (G : SimpleGraph α)
+    (w : VertexSeq α) (v : α) (h : v ∈ w.toList)
+    (hw : IsVertexSeqIn G w ∧ IsWalk w) :
+    IsVertexSeqIn G (w.takeUntil v h) ∧ IsWalk (w.takeUntil v h) :=
+  ⟨isVertexSeqIn_takeUntil G w v h hw.1, isWalk_takeUntil w v h hw.2⟩
+
+/-- Being a sequence in a subgraph implies being a sequence in the ambient
+graph (monotonicity in the graph argument). -/
+@[grind →]
+lemma isVertexSeqIn_mono {H G : SimpleGraph α} (w : VertexSeq α)
+    (hw : IsVertexSeqIn H w) (hsub : SimpleGraph.subgraphOf H G) :
+    IsVertexSeqIn G w := by
+  induction hw with
+  | singleton v hv => exact IsVertexSeqIn.singleton v (hsub.1 hv)
+  | cons w0 u hw0 he ih => exact IsVertexSeqIn.cons w0 u ih (hsub.2 he)
+
+/-- Monotonicity of "is a walk in `G`" along subgraph inclusion. -/
+lemma isVertexSeqIn_and_isWalk_mono {H G : SimpleGraph α} (w : VertexSeq α)
+    (hw : IsVertexSeqIn H w ∧ IsWalk w) (hsub : SimpleGraph.subgraphOf H G) :
+    IsVertexSeqIn G w ∧ IsWalk w :=
+  ⟨isVertexSeqIn_mono w hw.1 hsub, hw.2⟩
+
+/-- Concatenating two sequences in `G` along a connecting edge gives a
+sequence in `G`. -/
+lemma isVertexSeqIn_append (G : SimpleGraph α)
+    (w1 w2 : VertexSeq α)
+    (h1 : IsVertexSeqIn G w1) (h2 : IsVertexSeqIn G w2)
+    (hedg : s(w1.tail, w2.head) ∈ E(G)) :
+    IsVertexSeqIn G (w1.append w2) := by
+  induction h2 generalizing w1 with
+  | singleton v hv =>
+      rw [show w1.append (VertexSeq.singleton v) = w1.cons v from rfl]
+      refine IsVertexSeqIn.cons w1 v h1 ?_
+      simpa using hedg
+  | cons w0 u hw0 he ih =>
+      rw [show w1.append (w0.cons u) = (w1.append w0).cons u from rfl]
+      refine IsVertexSeqIn.cons (w1.append w0) u (ih w1 h1 hedg) ?_
+      have : (w1.append w0).tail = w0.tail := VertexSeq.tail_append w1 w0
+      rw [this]; exact he
+
+/-- Concatenating two walks in `G` meeting at a common vertex gives a walk
+in `G`. -/
+lemma isVertexSeqIn_walkAppend (G : SimpleGraph α)
+    (w1 w2 : Walk α)
+    (h1 : IsVertexSeqIn G w1.val) (h2 : IsVertexSeqIn G w2.val)
+    (h : w1.tail = w2.head) :
+    IsVertexSeqIn G (Walk.append w1 w2 h).val := by
+  unfold Walk.append
+  by_cases hlen : w1.length = 0
+  · simp only [hlen, dite_true]; exact h2
+  · simp only [hlen, dite_false]
+    refine isVertexSeqIn_append G w1.val.dropTail w2.val
+      (isVertexSeqIn_dropTail G w1.val h1) h2 ?_
+    obtain ⟨w0, u, hwseq⟩ : ∃ (w0 : VertexSeq α) (u : α), w1.val = w0.cons u := by
+      match hseq : w1.val with
+      | .singleton v =>
+          exfalso
+          apply hlen
+          change w1.val.length = 0
+          rw [hseq]; rfl
+      | .cons w0 u => exact ⟨w0, u, rfl⟩
+    have hh1 : IsVertexSeqIn G (w0.cons u) := hwseq ▸ h1
+    have hedg' : s(w0.tail, u) ∈ E(G) := by
+      cases hh1 with
+      | cons _ _ _ he => exact he
+    have hdrop_tail : w1.val.dropTail.tail = w0.tail := by rw [hwseq]; rfl
+    have hhead_eq : w2.val.head = u := by
+      change w2.head = u
+      rw [← h]
+      change w1.val.tail = u
+      rw [hwseq]; rfl
+    rw [hdrop_tail, hhead_eq]
+    exact hedg'
+
+/-- Loop-erasing a walk preserves the "in `G`" property: every walk in `G`
+yields a path in `G` between the same endpoints. -/
+lemma isVertexSeqIn_toPath (G : SimpleGraph α) (w : Walk α)
+    (hw : IsVertexSeqIn G w.val) :
+    IsVertexSeqIn G w.toPath.val.val := by
+  rw [VertexSeq.isVertexSeqIn_iff] at hw
+  rw [VertexSeq.isVertexSeqIn_iff]
+  refine ⟨?_, ?_⟩
+  · have : w.toPath.head = w.head := head_toPath w
+    change w.toPath.head ∈ V(G)
+    rw [this]
+    exact hw.1
+  · exact (edgeSet_toPath_subset w).trans hw.2
+
+end Walk