From cce51a62435c697dc35338a6576274cc15a68f7d Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 6 Aug 2026 18:18:18 +0200
Subject: [PATCH 01/20] Results about reachability with repeated visits.

---
 .../Turing/SingleTape/Deterministic.lean      |   2 +-
 Cslib/Foundations/Data/RelatesInSteps.lean    | 126 +++++++++++++++++-
 2 files changed, 120 insertions(+), 8 deletions(-)

diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
index 29f379d5a..77ce68176 100644
--- a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
@@ -445,7 +445,7 @@ def TimeComputable.comp {f g : List Symbol → List Symbol}
         (hg.timeBound (f a).length) hg_outputsFun
     -- Therefore, the computer reduces a to g (f a) in the sum of those times.
     have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
-    apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a
+    refine RelatesWithinSteps.mono ?_ h_a_reducesTo_g_f_a
     refine Nat.add_le_add_left ?_ (hf.timeBound a.length)
     · apply h_mono
       -- Use the lemma about output length being bounded by input length + time
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 052e52c98..33288889a 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -7,6 +7,7 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Init
+public import Mathlib.Data.Set.Card
 public import Mathlib.Logic.Relation
 
 /-! # Relations Across Steps
@@ -14,6 +15,13 @@ public import Mathlib.Logic.Relation
 This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
 These are inductively defines propositions that communicate whether a relation forms a
 chain of length `n` (or at most `n`) between two elements.
+
+The theorem `RelatesInSteps.exists_isPath` allows to obtain a path along the relation of
+transitively related elements and `IsPath.relatesInSteps` is the converse direction.
+
+Another result is `Relation.reflTransGen_iff_relatesWithinSteps_of_finite`, which states that if
+only `n` elements are reachable from `a`, then any element reachable from `a` is reachable in at
+most `n - 1` steps.
 -/
 
 @[expose] public section
@@ -147,6 +155,81 @@ lemma RelatesInSteps.map {α α' : Type*}
   | tail t' t'' m _ hstep ih =>
     exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep)
 
+/-! ## Definition of and results about paths along a relation -/
+
+/--
+`IsPath r f n` means that the first `n` steps of the sequence `f : ℕ → α` form a path along `r`,
+i.e. `r (f i) (f (i + 1))` holds for every `i < n`. The values of `f` beyond index `n` are
+irrelevant.
+-/
+def IsPath (r : α → α → Prop) (f : ℕ → α) (n : ℕ) : Prop := ∀ i < n, r (f i) (f (i + 1))
+
+/-- A path of length `n` is in particular a path of any smaller length. -/
+lemma IsPath.mono {f : ℕ → α} : Antitone (IsPath r f) := by
+  intro m n hle h_path i hi
+  exact h_path i (by omega)
+
+/-- If `a` and `b` are related in `n` steps, then there is a path of length `n` from `a` to `b`. -/
+theorem RelatesInSteps.exists_isPath {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
+    ∃ f : ℕ → α, f 0 = a ∧ f n = b ∧ IsPath r f n := by
+  induction h with
+  | refl => exact ⟨fun _ => a, rfl, rfl, by simp [IsPath]⟩
+  | tail t' t'' m _ hstep ih =>
+    obtain ⟨f, hf0, hfm, hfstep⟩ := ih
+    refine ⟨fun i => if i ≤ m then f i else t'', by simpa using hf0, by simp, fun i hi => ?_⟩
+    rcases Nat.lt_or_ge i m with h' | h'
+    · simpa [h'.le, h'] using hfstep i h'
+    · have : i = m := by lia
+      subst this
+      simpa [hfm] using hstep
+
+/-- Any two positions along a path are related in as many steps as their distance. -/
+theorem IsPath.relatesInSteps {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) (p k : ℕ) (hpk : p + k ≤ n) :
+    RelatesInSteps r (f p) (f (p + k)) k := by
+  induction k with
+  | zero => exact .refl _
+  | succ k ih =>
+    refine .tail _ (f (p + k)) _ k (ih (by lia)) ?_
+    have := hf (p + k) (by lia)
+    rwa [← Nat.add_assoc]
+
+/-- A path that visits the same element at two different positions can be shortened by splicing
+out the loop in between. -/
+theorem IsPath.relatesInSteps_of_eq {f : ℕ → α} {n i j : ℕ}
+    (hf : IsPath r f n)
+    (hij : i < j)
+    (hjn : j ≤ n)
+    (heq : f i = f j) :
+    RelatesInSteps r (f 0) (f n) (i + (n - j)) := by
+  have h₁ : RelatesInSteps r (f 0) (f j) i := by grind [hf.relatesInSteps 0 i (by lia)]
+  have h₂ : RelatesInSteps r (f j) (f n) (n - j) := by grind [hf.relatesInSteps j (n - j) (by lia)]
+  exact h₁.trans h₂
+
+/-- Every element visited by a path is reachable from its starting point. -/
+theorem IsPath.reflTransGen {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) {i : ℕ} (hi : i ≤ n) :
+    ReflTransGen r (f 0) (f i) := by
+  have := (hf.relatesInSteps 0 i (by lia)).reflTransGen
+  rwa [Nat.zero_add] at this
+
+/-- A path visiting more positions than there are elements reachable from its starting point must
+visit some element twice. -/
+theorem IsPath.exists_eq_of_ncard_le {f : ℕ → α} {n : ℕ}
+    (hf : IsPath r f n)
+    (hfin : Set.Finite (ReflTransGen r (f 0)))
+    (hn : Set.ncard (ReflTransGen r (f 0)) ≤ n) :
+    ∃ i j, i < j ∧ j ≤ n ∧ f i = f j := by
+  have hmaps : ∀ i ∈ Finset.range (n + 1), f i ∈ hfin.toFinset := fun i hi =>
+    hfin.mem_toFinset.mpr (hf.reflTransGen (by simpa [Nat.lt_succ_iff] using hi))
+  have hcard : hfin.toFinset.card < (Finset.range (n + 1)).card := by
+    grind [Set.ncard_eq_toFinset_card _ hfin]
+  obtain ⟨i, hi, j, hj, hij, hfij⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard hmaps
+  simp only [Finset.mem_range, Nat.lt_succ_iff] at hi hj
+  rcases Nat.lt_or_ge i j with hlt | hge
+  · exact ⟨i, j, hlt, hj, hfij⟩
+  · exact ⟨j, i, by lia, hi, hfij.symm⟩
+
+/-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
+
 /--
 `RelatesWithinSteps` is a variant of `RelatesInSteps` that allows for a loose bound.
 It states that `a` relates to `b` in *at most* `n` steps.
@@ -191,17 +274,18 @@ lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ}
   · lia
   · exact RelatesInSteps.trans hevals₁ hevals₂
 
-lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ}
-    (h : RelatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) :
-    RelatesWithinSteps r a b n₂ := by
-  obtain ⟨m, hm, hevals⟩ := h
+/-- If two elements `a` and `b` are related in at most `n₁` steps in the relation `r` and
+`n₁ ≤ n₂`, then they are also related in at most `n₂` steps. -/
+lemma RelatesWithinSteps.mono {a b : α} : Monotone (RelatesWithinSteps r a b ·) := by
+  intro n₁ n₂ hn ⟨m, hm, hevals⟩
   exact ⟨m, Nat.le_trans hm hn, hevals⟩
 
 /-- If `h : α → ℕ` increases by at most 1 on each step of `r`,
 then the value of `h` at the output is at most `h` at the input plus the step bound. -/
-lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ} (hevals : RelatesWithinSteps r a b m)
-    (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1)
-    :
+lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ}
+    (hevals : RelatesWithinSteps r a b m)
+    (h : α → ℕ)
+    (h_step : ∀ a b, r a b → h b ≤ h a + 1) :
     h b ≤ h a + m := by
   obtain ⟨m, hm, hevals_m⟩ := hevals
   have := RelatesInSteps.apply_le_apply_add hevals_m h h_step
@@ -218,4 +302,32 @@ lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α'
   obtain ⟨m, hm, hevals⟩ := h
   exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩
 
+/-! ### Reachability under a bound on the number of reachable elements -/
+
+/-- An `r`-chain from `a` to `b` visiting at least as many positions as there are elements
+(transitively) related to `a` must visit some element twice, and can therefore be shortened. -/
+theorem RelatesInSteps.exists_lt_of_ncard_le {b : α} {n : ℕ}
+    (hfin : Set.Finite (ReflTransGen r a))
+    (h : RelatesInSteps r a b n)
+    (hn : Set.ncard (ReflTransGen r a) ≤ n) :
+    ∃ m < n, RelatesInSteps r a b m := by
+  obtain ⟨f, rfl, rfl, hpath⟩ := h.exists_isPath
+  obtain ⟨i, j, hij, hjn, heq⟩ := hpath.exists_eq_of_ncard_le hfin hn
+  exact ⟨i + (n - j), by lia, hpath.relatesInSteps_of_eq hij hjn heq⟩
+
+/-- If only a finite number of elements are (transitively) related to `a`, then any such element
+is related to `a` in at most `k - 1` steps, where `k` is the cardinality of that set. -/
+theorem reflTransGen_iff_relatesWithinSteps_of_finite {b : α}
+    (hfin : Set.Finite (ReflTransGen r a)) :
+    ReflTransGen r a b ↔ RelatesWithinSteps r a b (Set.ncard (ReflTransGen r a) - 1) := by
+  classical
+  simp only [RelatesWithinSteps]
+  constructor
+  · intro h_reach
+    have hex : ∃ n, RelatesInSteps r a b n := ReflTransGen.relatesInSteps h_reach
+    -- A chain of minimal length cannot be shortened, so it is short enough.
+    have hmin : ∀ m < Nat.find hex, ¬ RelatesInSteps r a b m := fun m hm => Nat.find_min hex hm
+    grind [RelatesInSteps.exists_lt_of_ncard_le]
+  · grind [RelatesInSteps.reflTransGen]
+
 end Relation

From c462faa6c5934b1a6455cd6c4d3c2e60ae86648d Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 12 Aug 2026 17:05:02 +0200
Subject: [PATCH 02/20] Use isChain.

---
 Cslib/Foundations/Data/RelatesInSteps.lean | 236 +++++++++------------
 1 file changed, 99 insertions(+), 137 deletions(-)

diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 33288889a..14c58fa58 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -13,20 +13,19 @@ public import Mathlib.Logic.Relation
 /-! # Relations Across Steps
 
 This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
-These are inductively defines propositions that communicate whether a relation forms a
+These are inductively defined propositions that communicate whether a relation forms a
 chain of length `n` (or at most `n`) between two elements.
 
-The theorem `RelatesInSteps.exists_isPath` allows to obtain a path along the relation of
-transitively related elements and `IsPath.relatesInSteps` is the converse direction.
+The theorem `RelatesInSteps.exists_isChain` allows to obtain a chain (`List.IsChain`) along the
+relation of transitively related elements and `RelatesInSteps.of_isChain` is the converse direction.
 
-Another result is `Relation.reflTransGen_iff_relatesWithinSteps_of_finite`, which states that if
-only `n` elements are reachable from `a`, then any element reachable from `a` is reachable in at
-most `n - 1` steps.
+Another result is `Relation.ReflTransGen.relatesInSteps_lt_encard`, which states that any element
+reachable from `a` is reachable in fewer steps than there are elements reachable from `a`.
 -/
 
 @[expose] public section
 
-variable {α : Type*} {r : α → α → Prop} {a b c : α}
+variable {α : Type*} {r : α → α → Prop} {a b c : α} {n m : ℕ}
 
 namespace Relation
 
@@ -45,6 +44,9 @@ theorem RelatesInSteps.reflTransGen (h : RelatesInSteps r a b n) : ReflTransGen
   | refl => rfl
   | tail _ _ _ _ h ih => exact .tail ih h
 
+/-- If `b` is reachable from `a` via `r`, then they relate to each other for some number
+of steps.
+See `ReflTransGen.relatesInSteps_lt_encard` for a bound on the number of steps. -/
 theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInSteps r a b n := by
   induction h with
   | refl => exact ⟨0, .refl a⟩
@@ -81,11 +83,8 @@ lemma RelatesInSteps.zero {a b : α} (h : RelatesInSteps r a b 0) : a = b := by
   rfl
 
 @[simp]
-lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b := by
-  constructor
-  · exact RelatesInSteps.zero
-  · intro rfl
-    exact RelatesInSteps.refl a
+lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b :=
+  ⟨RelatesInSteps.zero, fun h => h ▸ .refl a⟩
 
 lemma RelatesInSteps.trans {a b c : α} {n m : ℕ}
     (h₁ : RelatesInSteps r a b n) (h₂ : RelatesInSteps r b c m) :
@@ -102,31 +101,23 @@ lemma RelatesInSteps.succ {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
   | tail t' _ _ hsteps hstep => exact ⟨t', hsteps, hstep⟩
 
 lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} :
-    RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b := by
-  constructor
-  · exact RelatesInSteps.succ
-  · rintro ⟨t', h_steps, h_red⟩
-    exact .tail _ t' b n h_steps h_red
+    RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b :=
+  ⟨RelatesInSteps.succ, fun ⟨t', h_steps, h_red⟩ => .tail _ t' b n h_steps h_red⟩
 
-lemma RelatesInSteps.succ' {a b : α} : ∀ {n : ℕ}, RelatesInSteps r a b (n + 1) →
+lemma RelatesInSteps.succ' {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
     ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
-  intro n h
-  obtain ⟨t', hsteps, hstep⟩ := succ h
-  cases n with
+  induction n generalizing b with
   | zero =>
-    rw [zero_iff] at hsteps
-    subst hsteps
-    exact ⟨b, hstep, .refl _⟩
-  | succ k' =>
-    obtain ⟨t''', h_red''', h_steps'''⟩ := succ' hsteps
-    exact ⟨t''', h_red''', .tail _ _ b k' h_steps''' hstep⟩
+    obtain ⟨t', hsteps, hstep⟩ := succ h
+    exact ⟨b, hsteps.zero ▸ hstep, .refl _⟩
+  | succ k ih =>
+    obtain ⟨t', hsteps, hstep⟩ := succ h
+    obtain ⟨t'', h_red, h_steps⟩ := ih hsteps
+    exact ⟨t'', h_red, .tail _ t' b k h_steps hstep⟩
 
 lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} :
-    RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
-  constructor
-  · exact succ'
-  · rintro ⟨t', h_red, h_steps⟩
-    exact h_steps.head a t' b n h_red
+    RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n :=
+  ⟨succ', fun ⟨t', h_red, h_steps⟩ => h_steps.head a t' b n h_red⟩
 
 /--
 If `h : α → ℕ` increases by at most 1 on each step of `r`,
@@ -155,78 +146,49 @@ lemma RelatesInSteps.map {α α' : Type*}
   | tail t' t'' m _ hstep ih =>
     exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep)
 
-/-! ## Definition of and results about paths along a relation -/
-
-/--
-`IsPath r f n` means that the first `n` steps of the sequence `f : ℕ → α` form a path along `r`,
-i.e. `r (f i) (f (i + 1))` holds for every `i < n`. The values of `f` beyond index `n` are
-irrelevant.
--/
-def IsPath (r : α → α → Prop) (f : ℕ → α) (n : ℕ) : Prop := ∀ i < n, r (f i) (f (i + 1))
-
-/-- A path of length `n` is in particular a path of any smaller length. -/
-lemma IsPath.mono {f : ℕ → α} : Antitone (IsPath r f) := by
-  intro m n hle h_path i hi
-  exact h_path i (by omega)
+/-! ## Lemmas to translate between RelatesInSteps and the existence of a chain (`List.IsChain`) -/
 
-/-- If `a` and `b` are related in `n` steps, then there is a path of length `n` from `a` to `b`. -/
-theorem RelatesInSteps.exists_isPath {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
-    ∃ f : ℕ → α, f 0 = a ∧ f n = b ∧ IsPath r f n := by
+/-- If `a` and `b` are related in `n` steps, then there is an `r`-chain of `n + 1` elements
+starting at `a` and ending at `b`.
+This is similar to `List.exists_isChain_ne_nil_of_relationReflTransGen`, but also provides
+a length guarantee. -/
+lemma RelatesInSteps.exists_isChain {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
+    ∃ chain : List α,
+      chain.IsChain r ∧ ∃ h_len : chain.length = n + 1, chain[0] = a ∧ chain[n] = b := by
   induction h with
-  | refl => exact ⟨fun _ => a, rfl, rfl, by simp [IsPath]⟩
+  | refl => use [a]; simp
   | tail t' t'' m _ hstep ih =>
-    obtain ⟨f, hf0, hfm, hfstep⟩ := ih
-    refine ⟨fun i => if i ≤ m then f i else t'', by simpa using hf0, by simp, fun i hi => ?_⟩
-    rcases Nat.lt_or_ge i m with h' | h'
-    · simpa [h'.le, h'] using hfstep i h'
-    · have : i = m := by lia
-      subst this
-      simpa [hfm] using hstep
-
-/-- Any two positions along a path are related in as many steps as their distance. -/
-theorem IsPath.relatesInSteps {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) (p k : ℕ) (hpk : p + k ≤ n) :
-    RelatesInSteps r (f p) (f (p + k)) k := by
+    obtain ⟨l, hchain, _, _, _⟩ := ih
+    use l ++ [t'']
+    constructor
+    · apply hchain.append (by simp) (by grind)
+    · grind
+
+/-- Any two elements along an `r`-chain are related in as many steps as their distance in the
+chain. -/
+lemma RelatesInSteps.of_isChain {chain : List α}
+    (hc : chain.IsChain r)
+    (p k : ℕ)
+    (hpk : p + k < chain.length) :
+    RelatesInSteps r chain[p] chain[p + k] k := by
   induction k with
   | zero => exact .refl _
   | succ k ih =>
-    refine .tail _ (f (p + k)) _ k (ih (by lia)) ?_
-    have := hf (p + k) (by lia)
-    rwa [← Nat.add_assoc]
-
-/-- A path that visits the same element at two different positions can be shortened by splicing
-out the loop in between. -/
-theorem IsPath.relatesInSteps_of_eq {f : ℕ → α} {n i j : ℕ}
-    (hf : IsPath r f n)
+    refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
+    apply List.IsChain.getElem hc
+
+/-- A chain that visits the same element at two different positions can be shortened by splicing
+out the loop in between, i.e. the first and last elements are also related to each other
+by fewer steps. -/
+lemma RelatesInSteps.of_isChain_eq {chain : List α} {i j : ℕ}
+    (hc : chain.IsChain r)
     (hij : i < j)
-    (hjn : j ≤ n)
-    (heq : f i = f j) :
-    RelatesInSteps r (f 0) (f n) (i + (n - j)) := by
-  have h₁ : RelatesInSteps r (f 0) (f j) i := by grind [hf.relatesInSteps 0 i (by lia)]
-  have h₂ : RelatesInSteps r (f j) (f n) (n - j) := by grind [hf.relatesInSteps j (n - j) (by lia)]
-  exact h₁.trans h₂
-
-/-- Every element visited by a path is reachable from its starting point. -/
-theorem IsPath.reflTransGen {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) {i : ℕ} (hi : i ≤ n) :
-    ReflTransGen r (f 0) (f i) := by
-  have := (hf.relatesInSteps 0 i (by lia)).reflTransGen
-  rwa [Nat.zero_add] at this
-
-/-- A path visiting more positions than there are elements reachable from its starting point must
-visit some element twice. -/
-theorem IsPath.exists_eq_of_ncard_le {f : ℕ → α} {n : ℕ}
-    (hf : IsPath r f n)
-    (hfin : Set.Finite (ReflTransGen r (f 0)))
-    (hn : Set.ncard (ReflTransGen r (f 0)) ≤ n) :
-    ∃ i j, i < j ∧ j ≤ n ∧ f i = f j := by
-  have hmaps : ∀ i ∈ Finset.range (n + 1), f i ∈ hfin.toFinset := fun i hi =>
-    hfin.mem_toFinset.mpr (hf.reflTransGen (by simpa [Nat.lt_succ_iff] using hi))
-  have hcard : hfin.toFinset.card < (Finset.range (n + 1)).card := by
-    grind [Set.ncard_eq_toFinset_card _ hfin]
-  obtain ⟨i, hi, j, hj, hij, hfij⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard hmaps
-  simp only [Finset.mem_range, Nat.lt_succ_iff] at hi hj
-  rcases Nat.lt_or_ge i j with hlt | hge
-  · exact ⟨i, j, hlt, hj, hfij⟩
-  · exact ⟨j, i, by lia, hi, hfij.symm⟩
+    (hjn : j < chain.length)
+    (heq : chain[i] = chain[j]) :
+    RelatesInSteps r chain[0] chain[chain.length - 1] (i + (chain.length - 1 - j)) := by
+  have h₁ := RelatesInSteps.of_isChain hc 0 i (by omega)
+  have h₂ := RelatesInSteps.of_isChain hc j (chain.length - 1 - j) (by omega)
+  grind [RelatesInSteps.trans]
 
 /-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
 
@@ -249,18 +211,12 @@ lemma RelatesWithinSteps.single {a b : α} (h : r a b) : RelatesWithinSteps r a
   RelatesWithinSteps.of_relatesInSteps (RelatesInSteps.single h)
 
 lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a = b := by
-  obtain ⟨m, hm, hevals⟩ := h
-  have : m = 0 := Nat.le_zero.mp hm
-  subst this
-  exact RelatesInSteps.zero hevals
+  obtain ⟨_, hm, hevals⟩ := h
+  simp_all
 
 @[simp]
-lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b := by
-  constructor
-  · exact RelatesWithinSteps.zero
-  · intro h
-    subst h
-    exact RelatesWithinSteps.refl a
+lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b :=
+  ⟨RelatesWithinSteps.zero, fun h => h ▸ .refl a⟩
 
 /-- Transitivity of `RelatesWithinSteps` in the sum of the step bounds. -/
 @[trans]
@@ -269,10 +225,7 @@ lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ}
     RelatesWithinSteps r a c (n₁ + n₂) := by
   obtain ⟨m₁, hm₁, hevals₁⟩ := h₁
   obtain ⟨m₂, hm₂, hevals₂⟩ := h₂
-  use m₁ + m₂
-  constructor
-  · lia
-  · exact RelatesInSteps.trans hevals₁ hevals₂
+  exact ⟨m₁ + m₂, by lia, hevals₁.trans hevals₂⟩
 
 /-- If two elements `a` and `b` are related in at most `n₁` steps in the relation `r` and
 `n₁ ≤ n₂`, then they are also related in at most `n₂` steps. -/
@@ -287,8 +240,8 @@ lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ}
     (h : α → ℕ)
     (h_step : ∀ a b, r a b → h b ≤ h a + 1) :
     h b ≤ h a + m := by
-  obtain ⟨m, hm, hevals_m⟩ := hevals
-  have := RelatesInSteps.apply_le_apply_add hevals_m h h_step
+  obtain ⟨_, hm, hevals_m⟩ := hevals
+  have := hevals_m.apply_le_apply_add h h_step
   lia
 
 /--
@@ -304,30 +257,39 @@ lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α'
 
 /-! ### Reachability under a bound on the number of reachable elements -/
 
-/-- An `r`-chain from `a` to `b` visiting at least as many positions as there are elements
-(transitively) related to `a` must visit some element twice, and can therefore be shortened. -/
-theorem RelatesInSteps.exists_lt_of_ncard_le {b : α} {n : ℕ}
-    (hfin : Set.Finite (ReflTransGen r a))
-    (h : RelatesInSteps r a b n)
-    (hn : Set.ncard (ReflTransGen r a) ≤ n) :
-    ∃ m < n, RelatesInSteps r a b m := by
-  obtain ⟨f, rfl, rfl, hpath⟩ := h.exists_isPath
-  obtain ⟨i, j, hij, hjn, heq⟩ := hpath.exists_eq_of_ncard_le hfin hn
-  exact ⟨i + (n - j), by lia, hpath.relatesInSteps_of_eq hij hjn heq⟩
-
-/-- If only a finite number of elements are (transitively) related to `a`, then any such element
-is related to `a` in at most `k - 1` steps, where `k` is the cardinality of that set. -/
-theorem reflTransGen_iff_relatesWithinSteps_of_finite {b : α}
-    (hfin : Set.Finite (ReflTransGen r a)) :
-    ReflTransGen r a b ↔ RelatesWithinSteps r a b (Set.ncard (ReflTransGen r a) - 1) := by
+/-- A more precise version of `ReflTransGen.relatesInSteps`: if `b` is reachable from `a`, then it
+is related to `a` in fewer steps than there are elements reachable from `a`.
+Note that this cardinality is an `ℕ∞`, and if it is infinite, no bound on the number of steps
+is stated. -/
+theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b) :
+    ∃ n, RelatesInSteps r a b n ∧ (n : ℕ∞) < {x | ReflTransGen r a x}.encard := by
   classical
-  simp only [RelatesWithinSteps]
-  constructor
-  · intro h_reach
-    have hex : ∃ n, RelatesInSteps r a b n := ReflTransGen.relatesInSteps h_reach
-    -- A chain of minimal length cannot be shortened, so it is short enough.
-    have hmin : ∀ m < Nat.find hex, ¬ RelatesInSteps r a b m := fun m hm => Nat.find_min hex hm
-    grind [RelatesInSteps.exists_lt_of_ncard_le]
-  · grind [RelatesInSteps.reflTransGen]
+  -- Let us use the shortest chain from `a` to `b`.
+  have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
+  refine ⟨Nat.find hex, Nat.find_spec hex, ?_⟩
+  obtain ⟨chain, hc, hlen, h0, hb⟩ := (Nat.find_spec hex).exists_isChain
+  -- All elements in the chain are reachable from `a`.
+  have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := by
+    simp only [Set.subset_def, Set.mem_ofPred_eq]
+    intro y hy
+    obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
+    simpa [h0] using (RelatesInSteps.of_isChain hc 0 i (by omega)).reflTransGen
+  -- Now assume, for the sake of contradiction, that the minimal chain has at least as many
+  -- elements as there are reachable elements.
+  by_contra hcard
+  push Not at hcard
+  -- Then there is at least one duplicate element.
+  have h_dup : ¬chain.Nodup := by
+    intro h_nodup
+    have hle := (Set.encard_le_encard hsub).trans hcard
+    rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
+    grind [List.toFinset_card_of_nodup, Nat.cast_le]
+  -- But then we can shorten the chain which contradicts the fact that it is minimal.
+  rw [List.nodup_iff_getElem?_ne_getElem?] at h_dup
+  push Not at h_dup
+  obtain ⟨i, j, hij, hjn, heq⟩ := h_dup
+  have heq' : chain[i] = chain[j] := by grind [List.getElem?_eq_getElem]
+  have hshort := RelatesInSteps.of_isChain_eq hc hij hjn heq'
+  exact Nat.find_min hex (m := i + (chain.length - 1 - j)) (by omega) (by grind)
 
 end Relation

From 877f6d5533d9fbd6ddea2553408ec780d3e5b6cc Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 12 Aug 2026 17:26:47 +0200
Subject: [PATCH 03/20] Extract a lemma and clean up.

---
 Cslib/Foundations/Data/RelatesInSteps.lean | 31 +++++++++++++++-------
 1 file changed, 22 insertions(+), 9 deletions(-)

diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 14c58fa58..7e3f2dd25 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -16,9 +16,12 @@ This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
 These are inductively defined propositions that communicate whether a relation forms a
 chain of length `n` (or at most `n`) between two elements.
 
-The theorem `RelatesInSteps.exists_isChain` allows to obtain a chain (`List.IsChain`) along the
+The lemma `RelatesInSteps.exists_isChain` allows to obtain a chain (`List.IsChain`) along the
 relation of transitively related elements and `RelatesInSteps.of_isChain` is the converse direction.
 
+If a chain has duplicates, the lemmas `RelatesInSteps.of_isChain_eq` and `RelatesInSteps.of_dup`
+show that the start and end point are reachable in fewer steps by removing the "loop".
+
 Another result is `Relation.ReflTransGen.relatesInSteps_lt_encard`, which states that any element
 reachable from `a` is reachable in fewer steps than there are elements reachable from `a`.
 -/
@@ -185,11 +188,25 @@ lemma RelatesInSteps.of_isChain_eq {chain : List α} {i j : ℕ}
     (hij : i < j)
     (hjn : j < chain.length)
     (heq : chain[i] = chain[j]) :
-    RelatesInSteps r chain[0] chain[chain.length - 1] (i + (chain.length - 1 - j)) := by
+    RelatesInSteps r (chain.head (by grind)) (chain.getLast (by grind))
+      (i + (chain.length - 1 - j)) := by
+  rw [List.head_eq_getElem, List.getLast_eq_getElem]
   have h₁ := RelatesInSteps.of_isChain hc 0 i (by omega)
   have h₂ := RelatesInSteps.of_isChain hc j (chain.length - 1 - j) (by omega)
   grind [RelatesInSteps.trans]
 
+/-- If a chain has duplicates, there is a shorter version with the same start and end point.
+This is a less explicit version of `RelatesInSteps.of_isChain_eq`. -/
+lemma RelatesInSteps.of_isChain_neg_nodup {chain : List α}
+    (hc : chain.IsChain r)
+    (hne : chain ≠ [])
+    (hdup : ¬ chain.Nodup) :
+    ∃ n < chain.length - 1, RelatesInSteps r (chain.head hne) (chain.getLast hne) n := by
+  rw [List.nodup_iff_getElem?_ne_getElem?] at hdup
+  push Not at hdup
+  obtain ⟨i, j, hij, hjn, heq⟩ := hdup
+  exact ⟨_, by omega, RelatesInSteps.of_isChain_eq hc hij hjn (by grind)⟩
+
 /-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
 
 /--
@@ -255,7 +272,7 @@ lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α'
   obtain ⟨m, hm, hevals⟩ := h
   exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩
 
-/-! ### Reachability under a bound on the number of reachable elements -/
+/-! ## Reachability under a bound on the number of reachable elements -/
 
 /-- A more precise version of `ReflTransGen.relatesInSteps`: if `b` is reachable from `a`, then it
 is related to `a` in fewer steps than there are elements reachable from `a`.
@@ -285,11 +302,7 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
     rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
     grind [List.toFinset_card_of_nodup, Nat.cast_le]
   -- But then we can shorten the chain which contradicts the fact that it is minimal.
-  rw [List.nodup_iff_getElem?_ne_getElem?] at h_dup
-  push Not at h_dup
-  obtain ⟨i, j, hij, hjn, heq⟩ := h_dup
-  have heq' : chain[i] = chain[j] := by grind [List.getElem?_eq_getElem]
-  have hshort := RelatesInSteps.of_isChain_eq hc hij hjn heq'
-  exact Nat.find_min hex (m := i + (chain.length - 1 - j)) (by omega) (by grind)
+  obtain ⟨n, hn, hshort⟩ := RelatesInSteps.of_isChain_neg_nodup hc (by grind) h_dup
+  exact Nat.find_min hex (m := n) (by omega) (by grind)
 
 end Relation

From ba0c2b5be69c206cdf116364fb32c71f3afb08db Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 12 Aug 2026 17:29:45 +0200
Subject: [PATCH 04/20] Undo some golfing.

---
 Cslib/Foundations/Data/RelatesInSteps.lean | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 7e3f2dd25..8445bae5a 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -86,8 +86,11 @@ lemma RelatesInSteps.zero {a b : α} (h : RelatesInSteps r a b 0) : a = b := by
   rfl
 
 @[simp]
-lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b :=
-  ⟨RelatesInSteps.zero, fun h => h ▸ .refl a⟩
+lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b := by
+  constructor
+  · exact RelatesInSteps.zero
+  · intro rfl
+    exact RelatesInSteps.refl a
 
 lemma RelatesInSteps.trans {a b c : α} {n m : ℕ}
     (h₁ : RelatesInSteps r a b n) (h₂ : RelatesInSteps r b c m) :
@@ -104,8 +107,11 @@ lemma RelatesInSteps.succ {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
   | tail t' _ _ hsteps hstep => exact ⟨t', hsteps, hstep⟩
 
 lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} :
-    RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b :=
-  ⟨RelatesInSteps.succ, fun ⟨t', h_steps, h_red⟩ => .tail _ t' b n h_steps h_red⟩
+    RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b := by
+  constructor
+  · exact RelatesInSteps.succ
+  · rintro ⟨t', h_steps, h_red⟩
+    exact .tail _ t' b n h_steps h_red
 
 lemma RelatesInSteps.succ' {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
     ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
@@ -119,9 +125,11 @@ lemma RelatesInSteps.succ' {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1
     exact ⟨t'', h_red, .tail _ t' b k h_steps hstep⟩
 
 lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} :
-    RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n :=
-  ⟨succ', fun ⟨t', h_red, h_steps⟩ => h_steps.head a t' b n h_red⟩
-
+    RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
+  constructor
+  · exact succ'
+  · rintro ⟨t', h_red, h_steps⟩
+    exact h_steps.head a t' b n h_red
 /--
 If `h : α → ℕ` increases by at most 1 on each step of `r`,
 then the value of `h` at the output is at most `h` at the input plus the number of steps.

From cd5c63f5a1eca67d5934fe267b2d88f5371cca9a Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 12 Aug 2026 17:32:43 +0200
Subject: [PATCH 05/20] Undo some more golfing.

---
 Cslib/Foundations/Data/RelatesInSteps.lean | 28 +++++++++++++---------
 1 file changed, 17 insertions(+), 11 deletions(-)

diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 8445bae5a..f4020165a 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -115,14 +115,15 @@ lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} :
 
 lemma RelatesInSteps.succ' {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
     ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
-  induction n generalizing b with
+  obtain ⟨t', hsteps, hstep⟩ := succ h
+  cases n with
   | zero =>
-    obtain ⟨t', hsteps, hstep⟩ := succ h
-    exact ⟨b, hsteps.zero ▸ hstep, .refl _⟩
-  | succ k ih =>
-    obtain ⟨t', hsteps, hstep⟩ := succ h
-    obtain ⟨t'', h_red, h_steps⟩ := ih hsteps
-    exact ⟨t'', h_red, .tail _ t' b k h_steps hstep⟩
+    rw [zero_iff] at hsteps
+    subst hsteps
+    exact ⟨b, hstep, .refl _⟩
+  | succ k' =>
+    obtain ⟨t''', h_red''', h_steps'''⟩ := succ' hsteps
+    exact ⟨t''', h_red''', .tail _ _ b k' h_steps''' hstep⟩
 
 lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} :
     RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
@@ -130,6 +131,7 @@ lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} :
   · exact succ'
   · rintro ⟨t', h_red, h_steps⟩
     exact h_steps.head a t' b n h_red
+
 /--
 If `h : α → ℕ` increases by at most 1 on each step of `r`,
 then the value of `h` at the output is at most `h` at the input plus the number of steps.
@@ -240,8 +242,12 @@ lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a =
   simp_all
 
 @[simp]
-lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b :=
-  ⟨RelatesWithinSteps.zero, fun h => h ▸ .refl a⟩
+lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b := by
+  constructor
+  · exact RelatesWithinSteps.zero
+  · intro h
+    subst h
+    exact RelatesWithinSteps.refl a
 
 /-- Transitivity of `RelatesWithinSteps` in the sum of the step bounds. -/
 @[trans]
@@ -265,8 +271,8 @@ lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ}
     (h : α → ℕ)
     (h_step : ∀ a b, r a b → h b ≤ h a + 1) :
     h b ≤ h a + m := by
-  obtain ⟨_, hm, hevals_m⟩ := hevals
-  have := hevals_m.apply_le_apply_add h h_step
+  obtain ⟨m, hm, hevals_m⟩ := hevals
+  have := RelatesInSteps.apply_le_apply_add hevals_m h h_step
   lia
 
 /--

From c4c92c1ae8f91cf7915b5fa8d954823708171561 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Mon, 17 Aug 2026 15:28:22 +0200
Subject: [PATCH 06/20] Extract results related to List.isChain into their own
 file.

---
 Cslib.lean                                 |  1 +
 Cslib/Foundations/Data/List.lean           | 65 ++++++++++++++++++++++
 Cslib/Foundations/Data/RelatesInSteps.lean | 63 +++++++++------------
 3 files changed, 91 insertions(+), 38 deletions(-)
 create mode 100644 Cslib/Foundations/Data/List.lean

diff --git a/Cslib.lean b/Cslib.lean
index a4da6b124..648f8453a 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -71,6 +71,7 @@ public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Data.List
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
 public import Cslib.Foundations.Data.OmegaSequence.Flatten
diff --git a/Cslib/Foundations/Data/List.lean b/Cslib/Foundations/Data/List.lean
new file mode 100644
index 000000000..b725f1d18
--- /dev/null
+++ b/Cslib/Foundations/Data/List.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.List.Chain
+public import Mathlib.Data.List.Nodup
+
+/-! # Results related to List.IsChain
+
+This file defines `List.IsChainFromTo`, a variant of `List.IsChain` that also fixes the first and
+last element of the chain.
+
+The lemma `List.IsChainFromTo.exists_length_lt_of_not_nodup` shows that a chain with duplicates can
+always be shortened.
+-/
+
+@[expose] public section
+
+variable {α : Type*} {r : α → α → Prop} {a b : α}
+
+/-- A "chain from to" is a list of elements where adjacent elements relate to each other
+(cf. `List.IsChain`) and start and end with specific elements. -/
+structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List α) (a b : α) : Prop where
+  isChain : chain.IsChain r
+  ne_nil : chain ≠ []
+  head_eq : chain.head ne_nil = a
+  getLast_eq : chain.getLast ne_nil = b
+
+@[simp, grind →]
+lemma List.IsChainFromTo_head_eq {chain : List α} (hc : chain.IsChainFromTo r a b) :
+    chain.head hc.ne_nil = a :=
+  hc.head_eq
+
+@[simp, grind →]
+lemma List.IsChainFromTo_getLast_eq {chain : List α} (hc : chain.IsChainFromTo r a b) :
+    chain.getLast hc.ne_nil = b :=
+  hc.getLast_eq
+
+@[simp, grind ←]
+lemma List.IsChainFromTo_singleton {a : α} : List.IsChainFromTo r [a] a a :=
+  ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
+
+/-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
+from `a` to `b` (the one that skips the part between the duplicates).
+Note that applying this method iteratively does not necessarily lead to the shortest `r`-chain
+from `a` to `b`, since we always keep the initial and final segment. -/
+lemma List.IsChainFromTo.exists_length_lt_of_not_nodup {chain : List α}
+    (hc : chain.IsChainFromTo r a b)
+    (h_dup : ¬ chain.Nodup) :
+    ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.length < chain.length := by
+  rw [nodup_iff_getElem?_ne_getElem?] at h_dup
+  push Not at h_dup
+  obtain ⟨i, j, h_ij, h_lt, h_eq⟩ := h_dup
+  use chain.take i ++ chain.drop j
+  refine ⟨⟨?_, by simp; omega, by grind, by grind⟩, by grind⟩
+  · refine (hc.isChain.take _).append (hc.isChain.drop _) ?_
+    intro x hx y hy
+    rw [List.head?_drop] at hy
+    have := hc.isChain.getElem (i := i - 1) (by omega)
+    grind
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index f4020165a..6ae91b73b 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -7,6 +7,7 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Data.List
 public import Mathlib.Data.Set.Card
 public import Mathlib.Logic.Relation
 
@@ -161,20 +162,19 @@ lemma RelatesInSteps.map {α α' : Type*}
 
 /-! ## Lemmas to translate between RelatesInSteps and the existence of a chain (`List.IsChain`) -/
 
-/-- If `a` and `b` are related in `n` steps, then there is an `r`-chain of `n + 1` elements
+/-- If `b` is related to `a` via `r` in `n` steps, then there is an `r`-chain of `n + 1` elements
 starting at `a` and ending at `b`.
 This is similar to `List.exists_isChain_ne_nil_of_relationReflTransGen`, but also provides
 a length guarantee. -/
-lemma RelatesInSteps.exists_isChain {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
-    ∃ chain : List α,
-      chain.IsChain r ∧ ∃ h_len : chain.length = n + 1, chain[0] = a ∧ chain[n] = b := by
+lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
+    ∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 := by
   induction h with
-  | refl => use [a]; simp
+  | refl => exact ⟨[a], by simp, rfl⟩
   | tail t' t'' m _ hstep ih =>
-    obtain ⟨l, hchain, _, _, _⟩ := ih
+    obtain ⟨l, hchain, hlen⟩ := ih
     use l ++ [t'']
-    constructor
-    · apply hchain.append (by simp) (by grind)
+    refine ⟨⟨?_, by simp, ?_, by simp⟩, by grind⟩
+    · exact hchain.isChain.append (by simp) (by grind)
     · grind
 
 /-- Any two elements along an `r`-chain are related in as many steps as their distance in the
@@ -190,32 +190,17 @@ lemma RelatesInSteps.of_isChain {chain : List α}
     refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
     apply List.IsChain.getElem hc
 
-/-- A chain that visits the same element at two different positions can be shortened by splicing
-out the loop in between, i.e. the first and last elements are also related to each other
-by fewer steps. -/
-lemma RelatesInSteps.of_isChain_eq {chain : List α} {i j : ℕ}
-    (hc : chain.IsChain r)
-    (hij : i < j)
-    (hjn : j < chain.length)
-    (heq : chain[i] = chain[j]) :
-    RelatesInSteps r (chain.head (by grind)) (chain.getLast (by grind))
-      (i + (chain.length - 1 - j)) := by
-  rw [List.head_eq_getElem, List.getLast_eq_getElem]
-  have h₁ := RelatesInSteps.of_isChain hc 0 i (by omega)
-  have h₂ := RelatesInSteps.of_isChain hc j (chain.length - 1 - j) (by omega)
-  grind [RelatesInSteps.trans]
-
-/-- If a chain has duplicates, there is a shorter version with the same start and end point.
-This is a less explicit version of `RelatesInSteps.of_isChain_eq`. -/
-lemma RelatesInSteps.of_isChain_neg_nodup {chain : List α}
-    (hc : chain.IsChain r)
-    (hne : chain ≠ [])
-    (hdup : ¬ chain.Nodup) :
-    ∃ n < chain.length - 1, RelatesInSteps r (chain.head hne) (chain.getLast hne) n := by
-  rw [List.nodup_iff_getElem?_ne_getElem?] at hdup
-  push Not at hdup
-  obtain ⟨i, j, hij, hjn, heq⟩ := hdup
-  exact ⟨_, by omega, RelatesInSteps.of_isChain_eq hc hij hjn (by grind)⟩
+
+/-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
+a number of steps equal to the length of the chain minus one. -/
+lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromTo r a b) :
+    RelatesInSteps r a b (chain.length - 1) := by
+  have h_ne : chain.length > 0 := by grind
+  have hrel := RelatesInSteps.of_isChain hc.isChain 0 (chain.length - 1) (by omega)
+  have h0 : chain[0] = a := by grind
+  have hl : chain[chain.length - 1] = b := by grind
+  simpa [h0, hl] using hrel
+
 
 /-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
 
@@ -298,13 +283,14 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
   -- Let us use the shortest chain from `a` to `b`.
   have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
   refine ⟨Nat.find hex, Nat.find_spec hex, ?_⟩
-  obtain ⟨chain, hc, hlen, h0, hb⟩ := (Nat.find_spec hex).exists_isChain
+  obtain ⟨chain, hc, hlen⟩ := (Nat.find_spec hex).exists_isChainFromTo
   -- All elements in the chain are reachable from `a`.
   have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := by
     simp only [Set.subset_def, Set.mem_ofPred_eq]
     intro y hy
     obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
-    simpa [h0] using (RelatesInSteps.of_isChain hc 0 i (by omega)).reflTransGen
+    have := RelatesInSteps.of_isChain hc.isChain 0 i (by omega)
+    grind [RelatesInSteps.reflTransGen]
   -- Now assume, for the sake of contradiction, that the minimal chain has at least as many
   -- elements as there are reachable elements.
   by_contra hcard
@@ -316,7 +302,8 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
     rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
     grind [List.toFinset_card_of_nodup, Nat.cast_le]
   -- But then we can shorten the chain which contradicts the fact that it is minimal.
-  obtain ⟨n, hn, hshort⟩ := RelatesInSteps.of_isChain_neg_nodup hc (by grind) h_dup
-  exact Nat.find_min hex (m := n) (by omega) (by grind)
+  obtain ⟨chain', hc', hlt⟩ := hc.exists_length_lt_of_not_nodup h_dup
+  have := List.length_pos_iff.mpr hc'.ne_nil
+  exact Nat.find_min hex (m := chain'.length - 1) (by omega) (RelatesInSteps.of_isChainFromTo hc')
 
 end Relation

From af70d3bdc90e12bf14fc8bc5f6151e4dd49159e9 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Mon, 17 Aug 2026 15:40:48 +0200
Subject: [PATCH 07/20] Minor tweaks.

---
 Cslib/Foundations/Data/List.lean           | 14 ++++++++------
 Cslib/Foundations/Data/RelatesInSteps.lean | 10 +++-------
 2 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/Cslib/Foundations/Data/List.lean b/Cslib/Foundations/Data/List.lean
index b725f1d18..559d97141 100644
--- a/Cslib/Foundations/Data/List.lean
+++ b/Cslib/Foundations/Data/List.lean
@@ -10,7 +10,7 @@ public import Cslib.Init
 public import Mathlib.Data.List.Chain
 public import Mathlib.Data.List.Nodup
 
-/-! # Results related to List.IsChain
+/-! # Chains with a designated start and end
 
 This file defines `List.IsChainFromTo`, a variant of `List.IsChain` that also fixes the first and
 last element of the chain.
@@ -21,7 +21,7 @@ always be shortened.
 
 @[expose] public section
 
-variable {α : Type*} {r : α → α → Prop} {a b : α}
+variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b : α}
 
 /-- A "chain from to" is a list of elements where adjacent elements relate to each other
 (cf. `List.IsChain`) and start and end with specific elements. -/
@@ -31,25 +31,27 @@ structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List
   head_eq : chain.head ne_nil = a
   getLast_eq : chain.getLast ne_nil = b
 
+/-- Restatement of `head_eq`, but tagged with simp and grind. -/
 @[simp, grind →]
-lemma List.IsChainFromTo_head_eq {chain : List α} (hc : chain.IsChainFromTo r a b) :
+lemma List.IsChainFromTo_head_eq (hc : chain.IsChainFromTo r a b) :
     chain.head hc.ne_nil = a :=
   hc.head_eq
 
+/-- Restatement of `getLast_eq`, but tagged with simp and grind. -/
 @[simp, grind →]
-lemma List.IsChainFromTo_getLast_eq {chain : List α} (hc : chain.IsChainFromTo r a b) :
+lemma List.IsChainFromTo_getLast_eq (hc : chain.IsChainFromTo r a b) :
     chain.getLast hc.ne_nil = b :=
   hc.getLast_eq
 
 @[simp, grind ←]
-lemma List.IsChainFromTo_singleton {a : α} : List.IsChainFromTo r [a] a a :=
+lemma List.IsChainFromTo.singleton {a : α} : List.IsChainFromTo r [a] a a :=
   ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
 
 /-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
 from `a` to `b` (the one that skips the part between the duplicates).
 Note that applying this method iteratively does not necessarily lead to the shortest `r`-chain
 from `a` to `b`, since we always keep the initial and final segment. -/
-lemma List.IsChainFromTo.exists_length_lt_of_not_nodup {chain : List α}
+lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
     (hc : chain.IsChainFromTo r a b)
     (h_dup : ¬ chain.Nodup) :
     ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.length < chain.length := by
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 6ae91b73b..7c0bc1c01 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -17,11 +17,9 @@ This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
 These are inductively defined propositions that communicate whether a relation forms a
 chain of length `n` (or at most `n`) between two elements.
 
-The lemma `RelatesInSteps.exists_isChain` allows to obtain a chain (`List.IsChain`) along the
-relation of transitively related elements and `RelatesInSteps.of_isChain` is the converse direction.
-
-If a chain has duplicates, the lemmas `RelatesInSteps.of_isChain_eq` and `RelatesInSteps.of_dup`
-show that the start and end point are reachable in fewer steps by removing the "loop".
+The lemma `RelatesInSteps.exists_isChainFromTo` allows to obtain a chain
+(`List.IsChainFromTo`) of related elements that witness the reachability, and
+`RelatesInSteps.of_isChainFromTo` is the converse direction.
 
 Another result is `Relation.ReflTransGen.relatesInSteps_lt_encard`, which states that any element
 reachable from `a` is reachable in fewer steps than there are elements reachable from `a`.
@@ -190,7 +188,6 @@ lemma RelatesInSteps.of_isChain {chain : List α}
     refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
     apply List.IsChain.getElem hc
 
-
 /-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
 a number of steps equal to the length of the chain minus one. -/
 lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromTo r a b) :
@@ -201,7 +198,6 @@ lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromT
   have hl : chain[chain.length - 1] = b := by grind
   simpa [h0, hl] using hrel
 
-
 /-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
 
 /--

From f03aca6139fb3a94e2e9b358a9ea6d487ef018a5 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Mon, 17 Aug 2026 18:25:33 +0200
Subject: [PATCH 08/20] Remove simp.

---
 Cslib/Foundations/Data/List.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cslib/Foundations/Data/List.lean b/Cslib/Foundations/Data/List.lean
index 559d97141..b2e247d94 100644
--- a/Cslib/Foundations/Data/List.lean
+++ b/Cslib/Foundations/Data/List.lean
@@ -31,14 +31,14 @@ structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List
   head_eq : chain.head ne_nil = a
   getLast_eq : chain.getLast ne_nil = b
 
-/-- Restatement of `head_eq`, but tagged with simp and grind. -/
-@[simp, grind →]
+/-- Restatement of `head_eq`, but tagged with grind. -/
+@[grind →]
 lemma List.IsChainFromTo_head_eq (hc : chain.IsChainFromTo r a b) :
     chain.head hc.ne_nil = a :=
   hc.head_eq
 
-/-- Restatement of `getLast_eq`, but tagged with simp and grind. -/
-@[simp, grind →]
+/-- Restatement of `getLast_eq`, but tagged with grind. -/
+@[grind →]
 lemma List.IsChainFromTo_getLast_eq (hc : chain.IsChainFromTo r a b) :
     chain.getLast hc.ne_nil = b :=
   hc.getLast_eq

From f85d8ed268ffc51c2e9e597fb7f6d946b6a76d78 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 20 Aug 2026 10:50:23 +0200
Subject: [PATCH 09/20] Move file.

---
 Cslib/Foundations/Data/{List.lean => IsChainFromTo.lean} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename Cslib/Foundations/Data/{List.lean => IsChainFromTo.lean} (100%)

diff --git a/Cslib/Foundations/Data/List.lean b/Cslib/Foundations/Data/IsChainFromTo.lean
similarity index 100%
rename from Cslib/Foundations/Data/List.lean
rename to Cslib/Foundations/Data/IsChainFromTo.lean

From bd393f3c463f3c266da7d41e0d68048db227f216 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 20 Aug 2026 11:15:08 +0200
Subject: [PATCH 10/20] Review comments.

---
 Cslib.lean                                    |  2 +-
 .../Data/{ => List}/IsChainFromTo.lean        | 26 ++++++++++++-------
 Cslib/Foundations/Data/RelatesInSteps.lean    | 23 +++++++---------
 3 files changed, 28 insertions(+), 23 deletions(-)
 rename Cslib/Foundations/Data/{ => List}/IsChainFromTo.lean (74%)

diff --git a/Cslib.lean b/Cslib.lean
index 5cb58db9d..2482c4312 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -74,7 +74,7 @@ public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.HasFresh
-public import Cslib.Foundations.Data.List
+public import Cslib.Foundations.Data.List.IsChainFromTo
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
 public import Cslib.Foundations.Data.OmegaSequence.Flatten
diff --git a/Cslib/Foundations/Data/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
similarity index 74%
rename from Cslib/Foundations/Data/IsChainFromTo.lean
rename to Cslib/Foundations/Data/List/IsChainFromTo.lean
index b2e247d94..35a44fea7 100644
--- a/Cslib/Foundations/Data/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -28,20 +28,26 @@ variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b : α}
 structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List α) (a b : α) : Prop where
   isChain : chain.IsChain r
   ne_nil : chain ≠ []
-  head_eq : chain.head ne_nil = a
-  getLast_eq : chain.getLast ne_nil = b
+  head : chain.head ne_nil = a
+  last : chain.getLast ne_nil = b
+
+/-- Create a `List.IsChainFromTo` from a non-empty `List.IsChain`. -/
+theorem List.IsChainFromTo.of_isChain_ne_nil
+    (chain : List α) (hc : chain.IsChain r) (h_ne_nil : chain ≠ []) :
+    List.IsChainFromTo r chain (chain.head h_ne_nil) (chain.getLast h_ne_nil) :=
+  ⟨hc, h_ne_nil, rfl, rfl⟩
 
 /-- Restatement of `head_eq`, but tagged with grind. -/
 @[grind →]
-lemma List.IsChainFromTo_head_eq (hc : chain.IsChainFromTo r a b) :
+lemma List.IsChainFromTo.head_eq (hc : chain.IsChainFromTo r a b) :
     chain.head hc.ne_nil = a :=
-  hc.head_eq
+  hc.head
 
 /-- Restatement of `getLast_eq`, but tagged with grind. -/
 @[grind →]
-lemma List.IsChainFromTo_getLast_eq (hc : chain.IsChainFromTo r a b) :
+lemma List.IsChainFromTo.last_eq (hc : chain.IsChainFromTo r a b) :
     chain.getLast hc.ne_nil = b :=
-  hc.getLast_eq
+  hc.last
 
 @[simp, grind ←]
 lemma List.IsChainFromTo.singleton {a : α} : List.IsChainFromTo r [a] a a :=
@@ -59,9 +65,11 @@ lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
   push Not at h_dup
   obtain ⟨i, j, h_ij, h_lt, h_eq⟩ := h_dup
   use chain.take i ++ chain.drop j
-  refine ⟨⟨?_, by simp; omega, by grind, by grind⟩, by grind⟩
-  · refine (hc.isChain.take _).append (hc.isChain.drop _) ?_
+  constructor
+  · apply IsChainFromTo.mk ((hc.isChain.take _).append (hc.isChain.drop _) ?_)
+      (by simp; omega) (by grind) (by grind)
     intro x hx y hy
     rw [List.head?_drop] at hy
-    have := hc.isChain.getElem (i := i - 1) (by omega)
+    have := hc.isChain.getElem (i := i - 1)
     grind
+  · grind
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 7c0bc1c01..efbc79d85 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -7,7 +7,7 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Init
-public import Cslib.Foundations.Data.List
+public import Cslib.Foundations.Data.List.IsChainFromTo
 public import Mathlib.Data.Set.Card
 public import Mathlib.Logic.Relation
 
@@ -171,9 +171,10 @@ lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSte
   | tail t' t'' m _ hstep ih =>
     obtain ⟨l, hchain, hlen⟩ := ih
     use l ++ [t'']
-    refine ⟨⟨?_, by simp, ?_, by simp⟩, by grind⟩
-    · exact hchain.isChain.append (by simp) (by grind)
-    · grind
+    constructor
+    · apply List.IsChainFromTo.mk (hchain.isChain.append (by simp) (by grind))
+        (by simp) (by grind) (by simp)
+    · simp [hlen]
 
 /-- Any two elements along an `r`-chain are related in as many steps as their distance in the
 chain. -/
@@ -185,7 +186,7 @@ lemma RelatesInSteps.of_isChain {chain : List α}
   induction k with
   | zero => exact .refl _
   | succ k ih =>
-    refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
+    apply RelatesInSteps.tail _ (chain[p + k]) _ k (ih (by lia))
     apply List.IsChain.getElem hc
 
 /-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
@@ -278,28 +279,24 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
   classical
   -- Let us use the shortest chain from `a` to `b`.
   have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
-  refine ⟨Nat.find hex, Nat.find_spec hex, ?_⟩
+  use Nat.find hex, Nat.find_spec hex
   obtain ⟨chain, hc, hlen⟩ := (Nat.find_spec hex).exists_isChainFromTo
   -- All elements in the chain are reachable from `a`.
   have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := by
-    simp only [Set.subset_def, Set.mem_ofPred_eq]
     intro y hy
     obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
-    have := RelatesInSteps.of_isChain hc.isChain 0 i (by omega)
+    have := RelatesInSteps.of_isChain hc.isChain 0 i
     grind [RelatesInSteps.reflTransGen]
   -- Now assume, for the sake of contradiction, that the minimal chain has at least as many
   -- elements as there are reachable elements.
-  by_contra hcard
-  push Not at hcard
+  by_contra! hcard
   -- Then there is at least one duplicate element.
   have h_dup : ¬chain.Nodup := by
-    intro h_nodup
     have hle := (Set.encard_le_encard hsub).trans hcard
     rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
     grind [List.toFinset_card_of_nodup, Nat.cast_le]
   -- But then we can shorten the chain which contradicts the fact that it is minimal.
   obtain ⟨chain', hc', hlt⟩ := hc.exists_length_lt_of_not_nodup h_dup
-  have := List.length_pos_iff.mpr hc'.ne_nil
-  exact Nat.find_min hex (m := chain'.length - 1) (by omega) (RelatesInSteps.of_isChainFromTo hc')
+  grind [Nat.find_min hex (m := chain'.length - 1), RelatesInSteps.of_isChainFromTo hc']
 
 end Relation

From 6f018c3ac3f275daade1f46b61f0b14c1d435a19 Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <crei.github@gmail.com>
Date: Tue, 25 Aug 2026 11:18:40 +0200
Subject: [PATCH 11/20] Update Cslib/Foundations/Data/List/IsChainFromTo.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Foundations/Data/List/IsChainFromTo.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index 35a44fea7..3b473f70c 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -28,8 +28,10 @@ variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b : α}
 structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List α) (a b : α) : Prop where
   isChain : chain.IsChain r
   ne_nil : chain ≠ []
-  head : chain.head ne_nil = a
-  last : chain.getLast ne_nil = b
+  head_eq : chain.head ne_nil = a
+  getLast_eq : chain.getLast ne_nil = b
+  
+attribute [grind →] List.IsChainFromTo.head_eq List.IsChainFromTo.getLast_eq
 
 /-- Create a `List.IsChainFromTo` from a non-empty `List.IsChain`. -/
 theorem List.IsChainFromTo.of_isChain_ne_nil

From cdff1eed1dc1e1ac7e3b78cf637d904a6bfeb25e Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 25 Aug 2026 11:27:05 +0200
Subject: [PATCH 12/20] Fix and apply suggestions.

---
 .../Foundations/Data/List/IsChainFromTo.lean  | 35 ++++++-------------
 1 file changed, 10 insertions(+), 25 deletions(-)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index 3b473f70c..8d1f09b1e 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -30,7 +30,7 @@ structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List
   ne_nil : chain ≠ []
   head_eq : chain.head ne_nil = a
   getLast_eq : chain.getLast ne_nil = b
-  
+
 attribute [grind →] List.IsChainFromTo.head_eq List.IsChainFromTo.getLast_eq
 
 /-- Create a `List.IsChainFromTo` from a non-empty `List.IsChain`. -/
@@ -39,39 +39,24 @@ theorem List.IsChainFromTo.of_isChain_ne_nil
     List.IsChainFromTo r chain (chain.head h_ne_nil) (chain.getLast h_ne_nil) :=
   ⟨hc, h_ne_nil, rfl, rfl⟩
 
-/-- Restatement of `head_eq`, but tagged with grind. -/
-@[grind →]
-lemma List.IsChainFromTo.head_eq (hc : chain.IsChainFromTo r a b) :
-    chain.head hc.ne_nil = a :=
-  hc.head
-
-/-- Restatement of `getLast_eq`, but tagged with grind. -/
-@[grind →]
-lemma List.IsChainFromTo.last_eq (hc : chain.IsChainFromTo r a b) :
-    chain.getLast hc.ne_nil = b :=
-  hc.last
-
 @[simp, grind ←]
 lemma List.IsChainFromTo.singleton {a : α} : List.IsChainFromTo r [a] a a :=
   ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
 
 /-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
-from `a` to `b` (the one that skips the part between the duplicates).
-Note that applying this method iteratively does not necessarily lead to the shortest `r`-chain
-from `a` to `b`, since we always keep the initial and final segment. -/
+from `a` to `b` (the one that skips the part between the duplicates). -/
 lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
     (hc : chain.IsChainFromTo r a b)
     (h_dup : ¬ chain.Nodup) :
     ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.length < chain.length := by
-  rw [nodup_iff_getElem?_ne_getElem?] at h_dup
-  push Not at h_dup
+  simp only [nodup_iff_getElem?_ne_getElem?, not_forall, not_not] at h_dup
   obtain ⟨i, j, h_ij, h_lt, h_eq⟩ := h_dup
   use chain.take i ++ chain.drop j
-  constructor
-  · apply IsChainFromTo.mk ((hc.isChain.take _).append (hc.isChain.drop _) ?_)
-      (by simp; omega) (by grind) (by grind)
-    intro x hx y hy
-    rw [List.head?_drop] at hy
-    have := hc.isChain.getElem (i := i - 1)
-    grind
+  split_ands
+  · apply IsChainFromTo.mk ..
+    · apply (hc.isChain.take _).append (hc.isChain.drop _)
+      grind [List.head?_drop, hc.isChain.getElem (i := i - 1)]
+    · grind [append_eq_nil_iff, drop_eq_nil_iff]
+    · grind
+    · grind
   · grind

From ca19e4fd133664ee1684d0b82f49d9e805de45d6 Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <crei.github@gmail.com>
Date: Tue, 25 Aug 2026 11:28:27 +0200
Subject: [PATCH 13/20] Update Cslib/Foundations/Data/List/IsChainFromTo.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Foundations/Data/List/IsChainFromTo.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index 8d1f09b1e..3be6ce38c 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -60,3 +60,12 @@ lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
     · grind
     · grind
   · grind
+
+lemma List.IsChainFromTo.exists_noDup (hc : chain.IsChainFromTo r a b) :
+    ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.Nodup := by
+  induction hn : chain.length using Nat.strong_induction_on generalizing chain with
+  | h n ih =>
+    by_cases h_dup : chain.Nodup
+    · use chain, hc, h_dup
+    · obtain ⟨chain', hc', hlen⟩ := hc.exists_length_lt_of_not_nodup h_dup
+      exact ih chain'.length (hn ▸ hlen) hc' rfl

From 9d1ea108d05dd930d9400e6afbbad5be733ef1d2 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 25 Aug 2026 13:23:10 +0200
Subject: [PATCH 14/20] Review comments and many more lemmas.

---
 .../Foundations/Data/List/IsChainFromTo.lean  | 92 ++++++++++++++++++-
 Cslib/Foundations/Data/RelatesInSteps.lean    | 62 +++++--------
 2 files changed, 115 insertions(+), 39 deletions(-)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index 3be6ce38c..09e7500a9 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -9,6 +9,7 @@ module
 public import Cslib.Init
 public import Mathlib.Data.List.Chain
 public import Mathlib.Data.List.Nodup
+public import Mathlib.Logic.Relation
 
 /-! # Chains with a designated start and end
 
@@ -33,16 +34,102 @@ structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List
 
 attribute [grind →] List.IsChainFromTo.head_eq List.IsChainFromTo.getLast_eq
 
+theorem relationReflTransGen_of_isChainFromTo (hc : chain.IsChainFromTo r a b) :
+    Relation.ReflTransGen r a b := by
+  simpa [hc.head_eq, hc.getLast_eq] using
+    List.relationReflTransGen_of_exists_isChain chain hc.isChain hc.ne_nil
+
 /-- Create a `List.IsChainFromTo` from a non-empty `List.IsChain`. -/
-theorem List.IsChainFromTo.of_isChain_ne_nil
+theorem List.IsChain.isChainFromTo_of_ne_nil
     (chain : List α) (hc : chain.IsChain r) (h_ne_nil : chain ≠ []) :
     List.IsChainFromTo r chain (chain.head h_ne_nil) (chain.getLast h_ne_nil) :=
   ⟨hc, h_ne_nil, rfl, rfl⟩
 
 @[simp, grind ←]
-lemma List.IsChainFromTo.singleton {a : α} : List.IsChainFromTo r [a] a a :=
+lemma List.IsChainFromTo.singleton : List.IsChainFromTo r [a] a a :=
   ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
 
+/-- Append an `r`-related element to the start of the chain. -/
+lemma List.IsChainFromTo.cons (h : r a b) (hc : chain.IsChainFromTo r b c) :
+    (a :: chain).IsChainFromTo r a c where
+  isChain := hc.isChain.cons_of_ne_nil hc.ne_nil (hc.head_eq.symm ▸ h)
+  ne_nil := cons_ne_nil a chain
+  head_eq := head_cons
+  getLast_eq := hc.getLast_eq ▸ chain.getLast_cons hc.ne_nil
+
+@[simp, grind ←]
+lemma List.IsChain.isChainFromTo_of_pair (h : r a b) : List.IsChainFromTo r [a, b] a b :=
+  ⟨by simp [h], by simp, rfl, rfl⟩
+
+/-- Removing the head yields a valid chain. -/
+lemma List.IsChainFromTo.of_cons_cons {x y : α} (hc : (x :: y :: chain).IsChainFromTo r a b) :
+    (y :: chain).IsChainFromTo r y b :=
+  ⟨hc.isChain.of_cons, cons_ne_nil _ _, head_cons, by grind⟩
+
+/-- Appending a chain and the tail of a second one whose start point equals the end point of the
+first yields a valid chain. -/
+lemma List.IsChainFromTo.append_tail (hc : chain.IsChainFromTo r a b) {chain' : List α}
+    (hc' : chain'.IsChainFromTo r b c) : (chain ++ chain'.tail).IsChainFromTo r a c where
+  isChain := by
+    have hb : chain.dropLast ++ [b] = chain :=
+      hc.getLast_eq ▸ chain.dropLast_append_getLast hc.ne_nil
+    have hb' : [b] ++ chain'.tail = chain' := by simp [←hc'.head_eq]
+    rw [←hb] at hc ⊢
+    exact hc.isChain.append_overlap (l₃ := chain'.tail) (hb'.symm ▸ hc'.isChain) (cons_ne_nil b [])
+  ne_nil := append_ne_nil_of_left_ne_nil hc.ne_nil _
+  head_eq := head_append_left hc.ne_nil |>.trans hc.head_eq
+  getLast_eq := by grind
+
+/-- Add an `r`-related element to the end of the chain. -/
+lemma List.IsChainFromTo.snoc (hc : chain.IsChainFromTo r a b) (h : r b c) :
+    (chain ++ [c]).IsChainFromTo r a c :=
+  append_tail hc (chain' := [b, c]) (by simp [h])
+
+/-- Appending a chain, dropping its last element and another chain whose start point equals
+the end point of the first chain yields a valid chain. -/
+lemma List.IsChainFromTo.append_dropLast (hc : chain.IsChainFromTo r a b) {chain' : List α}
+    (hc' : chain'.IsChainFromTo r b c) : (chain.dropLast ++ chain').IsChainFromTo r a c := by
+  convert hc.append_tail hc' using 1
+  nth_rw 1 [←chain'.cons_head_tail hc'.ne_nil, hc'.head_eq, append_cons, ←hc.getLast_eq,
+    dropLast_concat_getLast hc.ne_nil]
+
+/-- Applying `List.take` to a chain yields a chain from the same start point to the end of the
+new lits. -/
+lemma List.IsChainFromTo.take (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
+    (chain.take (i + 1)).IsChainFromTo r a chain[i] := by
+  have : chain.take (i + 1) ≠ [] := by grind [ne_nil_iff_length_pos, length_take]
+  exact ⟨hc.isChain.take _, this, by grind, by grind [chain.getLast_take this]⟩
+
+/-- Applying `List.drop` to a chain yields a chain from the first element of the resulting list
+to the same end point. -/
+lemma List.IsChainFromTo.drop (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
+    (chain.drop i).IsChainFromTo r chain[i] b := by
+  have : chain.drop i ≠ [] := ne_nil_iff_length_pos.mpr <| chain.lt_length_drop hi
+  refine ⟨hc.isChain.drop _, this, chain.head_drop this, hc.getLast_eq ▸ chain.getLast_drop this⟩
+
+lemma List.IsChainFromTo.head_induction_on
+    {motive : ∀ {chain : List α} {a b : α}, chain.IsChainFromTo r a b → Prop}
+    (h_refl : ∀ {a : α}, motive (IsChainFromTo.singleton (a := a)))
+    (h_head : ∀ {a b c : α} {chain : List α} (hab : r a b) (hc : chain.IsChainFromTo r b c),
+      motive hc → motive (hc.cons hab))
+    {chain : List α} {a b : α} (hc : chain.IsChainFromTo r a b) : motive hc := by
+  induction htail : chain.tail generalizing chain a with
+  | nil =>
+    obtain rfl : chain = [a] := by grind
+    grind
+  | cons a' tail ih =>
+    obtain rfl : chain = a :: a' :: tail := by grind
+    obtain ⟨hrel, hchain⟩ := isChain_cons_cons.mp hc.isChain
+    have : (a' :: tail).IsChainFromTo r a' b := hc.of_cons_cons
+    exact h_head hrel this (ih this rfl)
+
+/-- Any element of an `r`-chain from `a` to `b` is reflexively-transitively related from `a`. -/
+lemma relationReflTransGen_of_isChainFromTo_mem (hc : chain.IsChainFromTo r a b) {x : α}
+    (mem : x ∈ chain) :
+    Relation.ReflTransGen r a x := by
+  obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem mem
+  exact relationReflTransGen_of_isChainFromTo (hc.take hi)
+
 /-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
 from `a` to `b` (the one that skips the part between the duplicates). -/
 lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
@@ -61,6 +148,7 @@ lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
     · grind
   · grind
 
+/-- For any `r`-chain from `a` to `b` there is one without duplicates. -/
 lemma List.IsChainFromTo.exists_noDup (hc : chain.IsChainFromTo r a b) :
     ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.Nodup := by
   induction hn : chain.length using Nat.strong_induction_on generalizing chain with
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index efbc79d85..5dd22c902 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -47,8 +47,7 @@ theorem RelatesInSteps.reflTransGen (h : RelatesInSteps r a b n) : ReflTransGen
   | tail _ _ _ _ h ih => exact .tail ih h
 
 /-- If `b` is reachable from `a` via `r`, then they relate to each other for some number
-of steps.
-See `ReflTransGen.relatesInSteps_lt_encard` for a bound on the number of steps. -/
+of steps. -/
 theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInSteps r a b n := by
   induction h with
   | refl => exact ⟨0, .refl a⟩
@@ -166,22 +165,17 @@ This is similar to `List.exists_isChain_ne_nil_of_relationReflTransGen`, but als
 a length guarantee. -/
 lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
     ∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 := by
-  induction h with
-  | refl => exact ⟨[a], by simp, rfl⟩
-  | tail t' t'' m _ hstep ih =>
+  induction h using RelatesInSteps.head_induction_on with
+  | hrefl => exact ⟨[b], List.IsChainFromTo.singleton, rfl⟩
+  | @hhead a c n h' h ih =>
     obtain ⟨l, hchain, hlen⟩ := ih
-    use l ++ [t'']
-    constructor
-    · apply List.IsChainFromTo.mk (hchain.isChain.append (by simp) (by grind))
-        (by simp) (by grind) (by simp)
-    · simp [hlen]
+    use a :: l, hchain.cons h'
+    simpa
 
 /-- Any two elements along an `r`-chain are related in as many steps as their distance in the
 chain. -/
-lemma RelatesInSteps.of_isChain {chain : List α}
-    (hc : chain.IsChain r)
-    (p k : ℕ)
-    (hpk : p + k < chain.length) :
+lemma _root_.List.IsChain.relatesInSteps_getElem {chain : List α} (hc : chain.IsChain r)
+    (p k : ℕ) (hpk : p + k < chain.length) :
     RelatesInSteps r chain[p] chain[p + k] k := by
   induction k with
   | zero => exact .refl _
@@ -191,10 +185,10 @@ lemma RelatesInSteps.of_isChain {chain : List α}
 
 /-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
 a number of steps equal to the length of the chain minus one. -/
-lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromTo r a b) :
+lemma _root_.IsChainFromTo.relatesInSteps {chain : List α} (hc : chain.IsChainFromTo r a b) :
     RelatesInSteps r a b (chain.length - 1) := by
   have h_ne : chain.length > 0 := by grind
-  have hrel := RelatesInSteps.of_isChain hc.isChain 0 (chain.length - 1) (by omega)
+  have hrel := _root_.List.IsChain.relatesInSteps_getElem hc.isChain 0 (chain.length - 1) (by omega)
   have h0 : chain[0] = a := by grind
   have hl : chain[chain.length - 1] = b := by grind
   simpa [h0, hl] using hrel
@@ -277,26 +271,20 @@ is stated. -/
 theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b) :
     ∃ n, RelatesInSteps r a b n ∧ (n : ℕ∞) < {x | ReflTransGen r a x}.encard := by
   classical
-  -- Let us use the shortest chain from `a` to `b`.
-  have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
-  use Nat.find hex, Nat.find_spec hex
-  obtain ⟨chain, hc, hlen⟩ := (Nat.find_spec hex).exists_isChainFromTo
-  -- All elements in the chain are reachable from `a`.
-  have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := by
-    intro y hy
-    obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
-    have := RelatesInSteps.of_isChain hc.isChain 0 i
-    grind [RelatesInSteps.reflTransGen]
-  -- Now assume, for the sake of contradiction, that the minimal chain has at least as many
-  -- elements as there are reachable elements.
-  by_contra! hcard
-  -- Then there is at least one duplicate element.
-  have h_dup : ¬chain.Nodup := by
-    have hle := (Set.encard_le_encard hsub).trans hcard
-    rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
-    grind [List.toFinset_card_of_nodup, Nat.cast_le]
-  -- But then we can shorten the chain which contradicts the fact that it is minimal.
-  obtain ⟨chain', hc', hlt⟩ := hc.exists_length_lt_of_not_nodup h_dup
-  grind [Nat.find_min hex (m := chain'.length - 1), RelatesInSteps.of_isChainFromTo hc']
+  -- Take any chain from `a` to `b` and remove its duplicates.
+  obtain ⟨n, hn⟩ := h.relatesInSteps
+  obtain ⟨chain, hc, -⟩ := hn.exists_isChainFromTo
+  obtain ⟨chain, hc, h_nodup⟩ := hc.exists_noDup
+  refine ⟨chain.length - 1, _root_.IsChainFromTo.relatesInSteps hc, ?_⟩
+  -- All elements of the chain are reachable from `a`, and they are pairwise distinct,
+  -- so the chain has at most as many elements as there are reachable elements.
+  have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} :=
+    fun _ hx => relationReflTransGen_of_isChainFromTo_mem hc hx
+  have h_le : (chain.length : ℕ∞) ≤ {x | ReflTransGen r a x}.encard := by
+    rw [← List.coe_toFinset] at hsub
+    have := Set.encard_le_encard hsub
+    rwa [Set.encard_coe_eq_coe_finsetCard, List.toFinset_card_of_nodup h_nodup] at this
+  -- The number of steps is one less than the number of elements of the chain.
+  exact lt_of_lt_of_le (by grind [List.length_pos_iff, Nat.cast_lt]) h_le
 
 end Relation

From d66f76ac9634be538245516aa1ffe7d64be8c548 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 25 Aug 2026 13:40:45 +0200
Subject: [PATCH 15/20] Cleanup.

---
 .../Foundations/Data/List/IsChainFromTo.lean  | 34 +++++++-----
 Cslib/Foundations/Data/RelatesInSteps.lean    | 55 +++++++++++--------
 2 files changed, 51 insertions(+), 38 deletions(-)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index 09e7500a9..7d4d8398b 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -17,12 +17,13 @@ This file defines `List.IsChainFromTo`, a variant of `List.IsChain` that also fi
 last element of the chain.
 
 The lemma `List.IsChainFromTo.exists_length_lt_of_not_nodup` shows that a chain with duplicates can
-always be shortened.
+always be shortened, and `List.IsChainFromTo.exists_nodup` iterates this to obtain a chain
+without duplicates.
 -/
 
 @[expose] public section
 
-variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b : α}
+variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b c : α}
 
 /-- A "chain from to" is a list of elements where adjacent elements relate to each other
 (cf. `List.IsChain`) and start and end with specific elements. -/
@@ -34,22 +35,24 @@ structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List
 
 attribute [grind →] List.IsChainFromTo.head_eq List.IsChainFromTo.getLast_eq
 
-theorem relationReflTransGen_of_isChainFromTo (hc : chain.IsChainFromTo r a b) :
+/-- The start and the end of an `r`-chain are reflexively-transitively related by `r`. -/
+theorem List.IsChainFromTo.reflTransGen (hc : chain.IsChainFromTo r a b) :
     Relation.ReflTransGen r a b := by
   simpa [hc.head_eq, hc.getLast_eq] using
     List.relationReflTransGen_of_exists_isChain chain hc.isChain hc.ne_nil
 
 /-- Create a `List.IsChainFromTo` from a non-empty `List.IsChain`. -/
 theorem List.IsChain.isChainFromTo_of_ne_nil
-    (chain : List α) (hc : chain.IsChain r) (h_ne_nil : chain ≠ []) :
+    {chain : List α} (hc : chain.IsChain r) (h_ne_nil : chain ≠ []) :
     List.IsChainFromTo r chain (chain.head h_ne_nil) (chain.getLast h_ne_nil) :=
   ⟨hc, h_ne_nil, rfl, rfl⟩
 
+/-- A one-element list is an `r`-chain from that element to itself. -/
 @[simp, grind ←]
-lemma List.IsChainFromTo.singleton : List.IsChainFromTo r [a] a a :=
+lemma List.isChainFromTo_singleton : List.IsChainFromTo r [a] a a :=
   ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
 
-/-- Append an `r`-related element to the start of the chain. -/
+/-- Prepend an `r`-related element to the start of the chain. -/
 lemma List.IsChainFromTo.cons (h : r a b) (hc : chain.IsChainFromTo r b c) :
     (a :: chain).IsChainFromTo r a c where
   isChain := hc.isChain.cons_of_ne_nil hc.ne_nil (hc.head_eq.symm ▸ h)
@@ -57,8 +60,9 @@ lemma List.IsChainFromTo.cons (h : r a b) (hc : chain.IsChainFromTo r b c) :
   head_eq := head_cons
   getLast_eq := hc.getLast_eq ▸ chain.getLast_cons hc.ne_nil
 
+/-- A two-element list of `r`-related elements is an `r`-chain from the first to the second. -/
 @[simp, grind ←]
-lemma List.IsChain.isChainFromTo_of_pair (h : r a b) : List.IsChainFromTo r [a, b] a b :=
+lemma List.isChainFromTo_pair (h : r a b) : List.IsChainFromTo r [a, b] a b :=
   ⟨by simp [h], by simp, rfl, rfl⟩
 
 /-- Removing the head yields a valid chain. -/
@@ -93,15 +97,15 @@ lemma List.IsChainFromTo.append_dropLast (hc : chain.IsChainFromTo r a b) {chain
   nth_rw 1 [←chain'.cons_head_tail hc'.ne_nil, hc'.head_eq, append_cons, ←hc.getLast_eq,
     dropLast_concat_getLast hc.ne_nil]
 
-/-- Applying `List.take` to a chain yields a chain from the same start point to the end of the
-new lits. -/
+/-- Taking the first `i + 1` elements of a chain yields a chain from the same start point to
+`chain[i]`. -/
 lemma List.IsChainFromTo.take (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
     (chain.take (i + 1)).IsChainFromTo r a chain[i] := by
   have : chain.take (i + 1) ≠ [] := by grind [ne_nil_iff_length_pos, length_take]
   exact ⟨hc.isChain.take _, this, by grind, by grind [chain.getLast_take this]⟩
 
-/-- Applying `List.drop` to a chain yields a chain from the first element of the resulting list
-to the same end point. -/
+/-- Dropping the first `i` elements of a chain yields a chain from `chain[i]` to the same end
+point. -/
 lemma List.IsChainFromTo.drop (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
     (chain.drop i).IsChainFromTo r chain[i] b := by
   have : chain.drop i ≠ [] := ne_nil_iff_length_pos.mpr <| chain.lt_length_drop hi
@@ -109,7 +113,7 @@ lemma List.IsChainFromTo.drop (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i
 
 lemma List.IsChainFromTo.head_induction_on
     {motive : ∀ {chain : List α} {a b : α}, chain.IsChainFromTo r a b → Prop}
-    (h_refl : ∀ {a : α}, motive (IsChainFromTo.singleton (a := a)))
+    (h_refl : ∀ {a : α}, motive (isChainFromTo_singleton (r := r) (a := a)))
     (h_head : ∀ {a b c : α} {chain : List α} (hab : r a b) (hc : chain.IsChainFromTo r b c),
       motive hc → motive (hc.cons hab))
     {chain : List α} {a b : α} (hc : chain.IsChainFromTo r a b) : motive hc := by
@@ -124,11 +128,11 @@ lemma List.IsChainFromTo.head_induction_on
     exact h_head hrel this (ih this rfl)
 
 /-- Any element of an `r`-chain from `a` to `b` is reflexively-transitively related from `a`. -/
-lemma relationReflTransGen_of_isChainFromTo_mem (hc : chain.IsChainFromTo r a b) {x : α}
+lemma List.IsChainFromTo.reflTransGen_of_mem (hc : chain.IsChainFromTo r a b) {x : α}
     (mem : x ∈ chain) :
     Relation.ReflTransGen r a x := by
   obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem mem
-  exact relationReflTransGen_of_isChainFromTo (hc.take hi)
+  exact (hc.take hi).reflTransGen
 
 /-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
 from `a` to `b` (the one that skips the part between the duplicates). -/
@@ -149,7 +153,7 @@ lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
   · grind
 
 /-- For any `r`-chain from `a` to `b` there is one without duplicates. -/
-lemma List.IsChainFromTo.exists_noDup (hc : chain.IsChainFromTo r a b) :
+lemma List.IsChainFromTo.exists_nodup (hc : chain.IsChainFromTo r a b) :
     ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.Nodup := by
   induction hn : chain.length using Nat.strong_induction_on generalizing chain with
   | h n ih =>
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 5dd22c902..2030f6b72 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -19,7 +19,8 @@ chain of length `n` (or at most `n`) between two elements.
 
 The lemma `RelatesInSteps.exists_isChainFromTo` allows to obtain a chain
 (`List.IsChainFromTo`) of related elements that witness the reachability, and
-`RelatesInSteps.of_isChainFromTo` is the converse direction.
+`List.IsChainFromTo.relatesInSteps` is the converse direction.
+`Relation.relatesInSteps_iff_exists_isChainFromTo` combines both.
 
 Another result is `Relation.ReflTransGen.relatesInSteps_lt_encard`, which states that any element
 reachable from `a` is reachable in fewer steps than there are elements reachable from `a`.
@@ -157,7 +158,7 @@ lemma RelatesInSteps.map {α α' : Type*}
   | tail t' t'' m _ hstep ih =>
     exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep)
 
-/-! ## Lemmas to translate between RelatesInSteps and the existence of a chain (`List.IsChain`) -/
+/-! ## Translating between `RelatesInSteps` and chains (`List.IsChainFromTo`) -/
 
 /-- If `b` is related to `a` via `r` in `n` steps, then there is an `r`-chain of `n + 1` elements
 starting at `a` and ending at `b`.
@@ -166,7 +167,7 @@ a length guarantee. -/
 lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
     ∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 := by
   induction h using RelatesInSteps.head_induction_on with
-  | hrefl => exact ⟨[b], List.IsChainFromTo.singleton, rfl⟩
+  | hrefl => exact ⟨[b], List.isChainFromTo_singleton, rfl⟩
   | @hhead a c n h' h ih =>
     obtain ⟨l, hchain, hlen⟩ := ih
     use a :: l, hchain.cons h'
@@ -175,23 +176,30 @@ lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSte
 /-- Any two elements along an `r`-chain are related in as many steps as their distance in the
 chain. -/
 lemma _root_.List.IsChain.relatesInSteps_getElem {chain : List α} (hc : chain.IsChain r)
-    (p k : ℕ) (hpk : p + k < chain.length) :
-    RelatesInSteps r chain[p] chain[p + k] k := by
+    (i k : ℕ) (hik : i + k < chain.length) :
+    RelatesInSteps r chain[i] chain[i + k] k := by
   induction k with
   | zero => exact .refl _
   | succ k ih =>
-    apply RelatesInSteps.tail _ (chain[p + k]) _ k (ih (by lia))
+    apply RelatesInSteps.tail _ (chain[i + k]) _ k (ih (by lia))
     apply List.IsChain.getElem hc
 
-/-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
-a number of steps equal to the length of the chain minus one. -/
-lemma _root_.IsChainFromTo.relatesInSteps {chain : List α} (hc : chain.IsChainFromTo r a b) :
-    RelatesInSteps r a b (chain.length - 1) := by
-  have h_ne : chain.length > 0 := by grind
-  have hrel := _root_.List.IsChain.relatesInSteps_getElem hc.isChain 0 (chain.length - 1) (by omega)
-  have h0 : chain[0] = a := by grind
-  have hl : chain[chain.length - 1] = b := by grind
-  simpa [h0, hl] using hrel
+/-- If there is an `r`-chain of `n + 1` elements from `a` to `b`, then `a` and `b` are related
+to each other in `n` steps. -/
+lemma _root_.List.IsChainFromTo.relatesInSteps {chain : List α} {n : ℕ}
+    (hc : chain.IsChainFromTo r a b) (hlen : chain.length = n + 1) :
+    RelatesInSteps r a b n := by
+  have hrel := _root_.List.IsChain.relatesInSteps_getElem hc.isChain 0 n (by lia)
+  simp only [Nat.zero_add] at hrel
+  have h0 : chain[0]'(by lia) = a := by grind
+  have hl : chain[n]'(by lia) = b := by grind
+  rwa [h0, hl] at hrel
+
+/-- `a` and `b` are related in `n` steps exactly when there is an `r`-chain of `n + 1` elements
+from `a` to `b`. -/
+lemma relatesInSteps_iff_exists_isChainFromTo :
+    RelatesInSteps r a b n ↔ ∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 :=
+  ⟨RelatesInSteps.exists_isChainFromTo, fun ⟨_, hc, hlen⟩ => hc.relatesInSteps hlen⟩
 
 /-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
 
@@ -272,19 +280,20 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
     ∃ n, RelatesInSteps r a b n ∧ (n : ℕ∞) < {x | ReflTransGen r a x}.encard := by
   classical
   -- Take any chain from `a` to `b` and remove its duplicates.
-  obtain ⟨n, hn⟩ := h.relatesInSteps
-  obtain ⟨chain, hc, -⟩ := hn.exists_isChainFromTo
-  obtain ⟨chain, hc, h_nodup⟩ := hc.exists_noDup
-  refine ⟨chain.length - 1, _root_.IsChainFromTo.relatesInSteps hc, ?_⟩
+  obtain ⟨n₀, hn₀⟩ := h.relatesInSteps
+  obtain ⟨chain₀, hc₀, -⟩ := hn₀.exists_isChainFromTo
+  obtain ⟨chain, hc, h_nodup⟩ := hc₀.exists_nodup
+  obtain ⟨n, hlen⟩ : ∃ n, chain.length = n + 1 :=
+    ⟨chain.length - 1, by grind [List.length_pos_iff]⟩
+  refine ⟨n, hc.relatesInSteps hlen, ?_⟩
   -- All elements of the chain are reachable from `a`, and they are pairwise distinct,
   -- so the chain has at most as many elements as there are reachable elements.
-  have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} :=
-    fun _ hx => relationReflTransGen_of_isChainFromTo_mem hc hx
+  have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := fun _ hx => hc.reflTransGen_of_mem hx
   have h_le : (chain.length : ℕ∞) ≤ {x | ReflTransGen r a x}.encard := by
     rw [← List.coe_toFinset] at hsub
     have := Set.encard_le_encard hsub
     rwa [Set.encard_coe_eq_coe_finsetCard, List.toFinset_card_of_nodup h_nodup] at this
-  -- The number of steps is one less than the number of elements of the chain.
-  exact lt_of_lt_of_le (by grind [List.length_pos_iff, Nat.cast_lt]) h_le
+  -- The chain has one more element than the number of steps.
+  exact lt_of_lt_of_le (by rw [hlen]; exact_mod_cast Nat.lt_succ_self n) h_le
 
 end Relation

From 4f2cd1bb72dd3000aaec4aa455647825a6511f6b Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Tue, 25 Aug 2026 13:55:11 +0200
Subject: [PATCH 16/20] Add some more grind lemmas and update the module
 docstring.

---
 .../Foundations/Data/List/IsChainFromTo.lean  | 39 +++++++++++++++++--
 Cslib/Foundations/Data/RelatesInSteps.lean    |  8 ++--
 2 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index 7d4d8398b..cb39d18b7 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -14,11 +14,22 @@ public import Mathlib.Logic.Relation
 /-! # Chains with a designated start and end
 
 This file defines `List.IsChainFromTo`, a variant of `List.IsChain` that also fixes the first and
-last element of the chain.
+last element of the chain. Such a chain is an explicit witness for the fact that its end point is
+reachable from its start point, and its length bounds the number of steps that are needed.
 
-The lemma `List.IsChainFromTo.exists_length_lt_of_not_nodup` shows that a chain with duplicates can
-always be shortened, and `List.IsChainFromTo.exists_nodup` iterates this to obtain a chain
-without duplicates.
+## Main definitions
+
+* `List.IsChainFromTo r chain a b`: `chain` is a non-empty list whose adjacent elements are related
+  by `r`, whose first element is `a` and whose last element is `b`.
+
+## Main results
+
+* `List.IsChainFromTo.reflTransGen`: the start and the end of a chain are related by
+  `Relation.ReflTransGen`.
+* `List.IsChainFromTo.head_induction_on`: induction on a chain, peeling off elements at the start.
+* `List.IsChainFromTo.exists_length_lt_of_not_nodup`: a chain with duplicates can always be
+  shortened.
+* `List.IsChainFromTo.exists_nodup`: iterating the above yields a chain without duplicates.
 -/
 
 @[expose] public section
@@ -35,6 +46,25 @@ structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List
 
 attribute [grind →] List.IsChainFromTo.head_eq List.IsChainFromTo.getLast_eq
 
+/-- A chain has at least one element. -/
+@[grind →]
+lemma List.IsChainFromTo.length_pos (hc : chain.IsChainFromTo r a b) : 0 < chain.length :=
+  List.length_pos_iff.mpr hc.ne_nil
+
+/-- The first element of an `r`-chain from `a` to `b` is `a`. -/
+@[grind →]
+lemma List.IsChainFromTo.getElem_zero (hc : chain.IsChainFromTo r a b) :
+    chain[0]'hc.length_pos = a := by
+  rw [List.getElem_zero]
+  exact hc.head_eq
+
+/-- The last element of an `r`-chain from `a` to `b` is `b`. -/
+@[grind →]
+lemma List.IsChainFromTo.getElem_length_sub_one (hc : chain.IsChainFromTo r a b) :
+    chain[chain.length - 1]'(by have := hc.length_pos; lia) = b := by
+  rw [List.getElem_length_sub_one_eq_getLast]
+  exact hc.getLast_eq
+
 /-- The start and the end of an `r`-chain are reflexively-transitively related by `r`. -/
 theorem List.IsChainFromTo.reflTransGen (hc : chain.IsChainFromTo r a b) :
     Relation.ReflTransGen r a b := by
@@ -111,6 +141,7 @@ lemma List.IsChainFromTo.drop (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i
   have : chain.drop i ≠ [] := ne_nil_iff_length_pos.mpr <| chain.lt_length_drop hi
   refine ⟨hc.isChain.drop _, this, chain.head_drop this, hc.getLast_eq ▸ chain.getLast_drop this⟩
 
+@[elab_as_elim]
 lemma List.IsChainFromTo.head_induction_on
     {motive : ∀ {chain : List α} {a b : α}, chain.IsChainFromTo r a b → Prop}
     (h_refl : ∀ {a : α}, motive (isChainFromTo_singleton (r := r) (a := a)))
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 2030f6b72..2d896c2db 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -191,9 +191,8 @@ lemma _root_.List.IsChainFromTo.relatesInSteps {chain : List α} {n : ℕ}
     RelatesInSteps r a b n := by
   have hrel := _root_.List.IsChain.relatesInSteps_getElem hc.isChain 0 n (by lia)
   simp only [Nat.zero_add] at hrel
-  have h0 : chain[0]'(by lia) = a := by grind
-  have hl : chain[n]'(by lia) = b := by grind
-  rwa [h0, hl] at hrel
+  have hlast : chain[n]'(by lia) = b := by simpa [hlen] using hc.getElem_length_sub_one
+  rwa [hc.getElem_zero, hlast] at hrel
 
 /-- `a` and `b` are related in `n` steps exactly when there is an `r`-chain of `n + 1` elements
 from `a` to `b`. -/
@@ -283,8 +282,7 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
   obtain ⟨n₀, hn₀⟩ := h.relatesInSteps
   obtain ⟨chain₀, hc₀, -⟩ := hn₀.exists_isChainFromTo
   obtain ⟨chain, hc, h_nodup⟩ := hc₀.exists_nodup
-  obtain ⟨n, hlen⟩ : ∃ n, chain.length = n + 1 :=
-    ⟨chain.length - 1, by grind [List.length_pos_iff]⟩
+  obtain ⟨n, hlen⟩ : ∃ n, chain.length = n + 1 := ⟨chain.length - 1, by have := hc.length_pos; lia⟩
   refine ⟨n, hc.relatesInSteps hlen, ?_⟩
   -- All elements of the chain are reachable from `a`, and they are pairwise distinct,
   -- so the chain has at most as many elements as there are reachable elements.

From 2a892a112ebd3a190a6f2c4a6a0dc9223eb226da Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 26 Aug 2026 10:47:27 +0200
Subject: [PATCH 17/20] Move into List namespace, review suggestions

---
 .../Foundations/Data/List/IsChainFromTo.lean  | 73 +++++++++++--------
 Cslib/Foundations/Data/RelatesInSteps.lean    |  6 +-
 2 files changed, 46 insertions(+), 33 deletions(-)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index cb39d18b7..6e32e807c 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Christian Reitwiessner
+Authors: Christian Reitwiessner, Thomas Waring
 -/
 
 module
@@ -34,75 +34,81 @@ reachable from its start point, and its length bounds the number of steps that a
 
 @[expose] public section
 
+namespace List
+
 variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b c : α}
 
 /-- A "chain from to" is a list of elements where adjacent elements relate to each other
 (cf. `List.IsChain`) and start and end with specific elements. -/
-structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List α) (a b : α) : Prop where
+structure IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List α) (a b : α) : Prop where
   isChain : chain.IsChain r
   ne_nil : chain ≠ []
   head_eq : chain.head ne_nil = a
   getLast_eq : chain.getLast ne_nil = b
 
-attribute [grind →] List.IsChainFromTo.head_eq List.IsChainFromTo.getLast_eq
+attribute [scoped grind →] IsChainFromTo.head_eq IsChainFromTo.getLast_eq
 
 /-- A chain has at least one element. -/
-@[grind →]
-lemma List.IsChainFromTo.length_pos (hc : chain.IsChainFromTo r a b) : 0 < chain.length :=
+@[scoped grind →]
+lemma IsChainFromTo.length_pos (hc : chain.IsChainFromTo r a b) : 0 < chain.length :=
   List.length_pos_iff.mpr hc.ne_nil
 
 /-- The first element of an `r`-chain from `a` to `b` is `a`. -/
-@[grind →]
-lemma List.IsChainFromTo.getElem_zero (hc : chain.IsChainFromTo r a b) :
+@[scoped grind →]
+lemma IsChainFromTo.getElem_zero (hc : chain.IsChainFromTo r a b) :
     chain[0]'hc.length_pos = a := by
   rw [List.getElem_zero]
   exact hc.head_eq
 
 /-- The last element of an `r`-chain from `a` to `b` is `b`. -/
-@[grind →]
-lemma List.IsChainFromTo.getElem_length_sub_one (hc : chain.IsChainFromTo r a b) :
+@[scoped grind →]
+lemma IsChainFromTo.getElem_length_sub_one (hc : chain.IsChainFromTo r a b) :
     chain[chain.length - 1]'(by have := hc.length_pos; lia) = b := by
   rw [List.getElem_length_sub_one_eq_getLast]
   exact hc.getLast_eq
 
 /-- The start and the end of an `r`-chain are reflexively-transitively related by `r`. -/
-theorem List.IsChainFromTo.reflTransGen (hc : chain.IsChainFromTo r a b) :
+theorem IsChainFromTo.reflTransGen (hc : chain.IsChainFromTo r a b) :
     Relation.ReflTransGen r a b := by
   simpa [hc.head_eq, hc.getLast_eq] using
     List.relationReflTransGen_of_exists_isChain chain hc.isChain hc.ne_nil
 
 /-- Create a `List.IsChainFromTo` from a non-empty `List.IsChain`. -/
-theorem List.IsChain.isChainFromTo_of_ne_nil
+theorem IsChain.isChainFromTo_of_ne_nil
     {chain : List α} (hc : chain.IsChain r) (h_ne_nil : chain ≠ []) :
     List.IsChainFromTo r chain (chain.head h_ne_nil) (chain.getLast h_ne_nil) :=
   ⟨hc, h_ne_nil, rfl, rfl⟩
 
 /-- A one-element list is an `r`-chain from that element to itself. -/
-@[simp, grind ←]
-lemma List.isChainFromTo_singleton : List.IsChainFromTo r [a] a a :=
+@[simp, scoped grind ←]
+lemma isChainFromTo_singleton : List.IsChainFromTo r [a] a a :=
   ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
 
 /-- Prepend an `r`-related element to the start of the chain. -/
-lemma List.IsChainFromTo.cons (h : r a b) (hc : chain.IsChainFromTo r b c) :
+lemma IsChainFromTo.cons (h : r a b) (hc : chain.IsChainFromTo r b c) :
     (a :: chain).IsChainFromTo r a c where
   isChain := hc.isChain.cons_of_ne_nil hc.ne_nil (hc.head_eq.symm ▸ h)
   ne_nil := cons_ne_nil a chain
   head_eq := head_cons
   getLast_eq := hc.getLast_eq ▸ chain.getLast_cons hc.ne_nil
 
-/-- A two-element list of `r`-related elements is an `r`-chain from the first to the second. -/
-@[simp, grind ←]
-lemma List.isChainFromTo_pair (h : r a b) : List.IsChainFromTo r [a, b] a b :=
-  ⟨by simp [h], by simp, rfl, rfl⟩
+@[simp, scoped grind =]
+lemma isChainFromTo_pair_iff {a a' b b' : α} :
+    List.IsChainFromTo r [a, b] a' b' ↔ r a b ∧ a = a' ∧ b = b' := by
+  constructor
+  · rintro ⟨hc, _, rfl, rfl⟩
+    simpa using hc
+  · rintro ⟨h, rfl, rfl⟩
+    constructor <;> simp_all
 
 /-- Removing the head yields a valid chain. -/
-lemma List.IsChainFromTo.of_cons_cons {x y : α} (hc : (x :: y :: chain).IsChainFromTo r a b) :
+lemma IsChainFromTo.of_cons_cons {x y : α} (hc : (x :: y :: chain).IsChainFromTo r a b) :
     (y :: chain).IsChainFromTo r y b :=
   ⟨hc.isChain.of_cons, cons_ne_nil _ _, head_cons, by grind⟩
 
 /-- Appending a chain and the tail of a second one whose start point equals the end point of the
 first yields a valid chain. -/
-lemma List.IsChainFromTo.append_tail (hc : chain.IsChainFromTo r a b) {chain' : List α}
+lemma IsChainFromTo.append_tail (hc : chain.IsChainFromTo r a b) {chain' : List α}
     (hc' : chain'.IsChainFromTo r b c) : (chain ++ chain'.tail).IsChainFromTo r a c where
   isChain := by
     have hb : chain.dropLast ++ [b] = chain :=
@@ -115,13 +121,13 @@ lemma List.IsChainFromTo.append_tail (hc : chain.IsChainFromTo r a b) {chain' :
   getLast_eq := by grind
 
 /-- Add an `r`-related element to the end of the chain. -/
-lemma List.IsChainFromTo.snoc (hc : chain.IsChainFromTo r a b) (h : r b c) :
+lemma IsChainFromTo.snoc (hc : chain.IsChainFromTo r a b) (h : r b c) :
     (chain ++ [c]).IsChainFromTo r a c :=
-  append_tail hc (chain' := [b, c]) (by simp [h])
+  append_tail hc (chain' := [b, c]) (by simpa)
 
 /-- Appending a chain, dropping its last element and another chain whose start point equals
 the end point of the first chain yields a valid chain. -/
-lemma List.IsChainFromTo.append_dropLast (hc : chain.IsChainFromTo r a b) {chain' : List α}
+lemma IsChainFromTo.append_dropLast (hc : chain.IsChainFromTo r a b) {chain' : List α}
     (hc' : chain'.IsChainFromTo r b c) : (chain.dropLast ++ chain').IsChainFromTo r a c := by
   convert hc.append_tail hc' using 1
   nth_rw 1 [←chain'.cons_head_tail hc'.ne_nil, hc'.head_eq, append_cons, ←hc.getLast_eq,
@@ -129,20 +135,20 @@ lemma List.IsChainFromTo.append_dropLast (hc : chain.IsChainFromTo r a b) {chain
 
 /-- Taking the first `i + 1` elements of a chain yields a chain from the same start point to
 `chain[i]`. -/
-lemma List.IsChainFromTo.take (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
+lemma IsChainFromTo.take (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
     (chain.take (i + 1)).IsChainFromTo r a chain[i] := by
   have : chain.take (i + 1) ≠ [] := by grind [ne_nil_iff_length_pos, length_take]
   exact ⟨hc.isChain.take _, this, by grind, by grind [chain.getLast_take this]⟩
 
 /-- Dropping the first `i` elements of a chain yields a chain from `chain[i]` to the same end
 point. -/
-lemma List.IsChainFromTo.drop (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
+lemma IsChainFromTo.drop (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
     (chain.drop i).IsChainFromTo r chain[i] b := by
   have : chain.drop i ≠ [] := ne_nil_iff_length_pos.mpr <| chain.lt_length_drop hi
   refine ⟨hc.isChain.drop _, this, chain.head_drop this, hc.getLast_eq ▸ chain.getLast_drop this⟩
 
 @[elab_as_elim]
-lemma List.IsChainFromTo.head_induction_on
+lemma IsChainFromTo.head_induction_on
     {motive : ∀ {chain : List α} {a b : α}, chain.IsChainFromTo r a b → Prop}
     (h_refl : ∀ {a : α}, motive (isChainFromTo_singleton (r := r) (a := a)))
     (h_head : ∀ {a b c : α} {chain : List α} (hab : r a b) (hc : chain.IsChainFromTo r b c),
@@ -159,15 +165,22 @@ lemma List.IsChainFromTo.head_induction_on
     exact h_head hrel this (ih this rfl)
 
 /-- Any element of an `r`-chain from `a` to `b` is reflexively-transitively related from `a`. -/
-lemma List.IsChainFromTo.reflTransGen_of_mem (hc : chain.IsChainFromTo r a b) {x : α}
+lemma IsChainFromTo.reflTransGen_of_mem (hc : chain.IsChainFromTo r a b) {x : α}
     (mem : x ∈ chain) :
     Relation.ReflTransGen r a x := by
   obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem mem
   exact (hc.take hi).reflTransGen
 
+/-- Any element of an `r`-chain from `a` to `b` is reflexively-transitively related to `b`. -/
+lemma IsChainFromTo.reflTransGen_of_mem' (hc : chain.IsChainFromTo r a b) {x : α}
+    (mem : x ∈ chain) :
+    Relation.ReflTransGen r x b := by
+  obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem mem
+  exact (hc.drop hi).reflTransGen
+
 /-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
 from `a` to `b` (the one that skips the part between the duplicates). -/
-lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
+lemma IsChainFromTo.exists_length_lt_of_not_nodup
     (hc : chain.IsChainFromTo r a b)
     (h_dup : ¬ chain.Nodup) :
     ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.length < chain.length := by
@@ -184,7 +197,7 @@ lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
   · grind
 
 /-- For any `r`-chain from `a` to `b` there is one without duplicates. -/
-lemma List.IsChainFromTo.exists_nodup (hc : chain.IsChainFromTo r a b) :
+lemma IsChainFromTo.exists_nodup (hc : chain.IsChainFromTo r a b) :
     ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.Nodup := by
   induction hn : chain.length using Nat.strong_induction_on generalizing chain with
   | h n ih =>
@@ -192,3 +205,5 @@ lemma List.IsChainFromTo.exists_nodup (hc : chain.IsChainFromTo r a b) :
     · use chain, hc, h_dup
     · obtain ⟨chain', hc', hlen⟩ := hc.exists_length_lt_of_not_nodup h_dup
       exact ih chain'.length (hn ▸ hlen) hc' rfl
+
+end List
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 2d896c2db..921b4e922 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -190,9 +190,8 @@ lemma _root_.List.IsChainFromTo.relatesInSteps {chain : List α} {n : ℕ}
     (hc : chain.IsChainFromTo r a b) (hlen : chain.length = n + 1) :
     RelatesInSteps r a b n := by
   have hrel := _root_.List.IsChain.relatesInSteps_getElem hc.isChain 0 n (by lia)
-  simp only [Nat.zero_add] at hrel
   have hlast : chain[n]'(by lia) = b := by simpa [hlen] using hc.getElem_length_sub_one
-  rwa [hc.getElem_zero, hlast] at hrel
+  simpa [hc.getElem_zero, hlast] using hrel
 
 /-- `a` and `b` are related in `n` steps exactly when there is an `r`-chain of `n + 1` elements
 from `a` to `b`. -/
@@ -228,8 +227,7 @@ lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a =
 lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b := by
   constructor
   · exact RelatesWithinSteps.zero
-  · intro h
-    subst h
+  · rintro rfl
     exact RelatesWithinSteps.refl a
 
 /-- Transitivity of `RelatesWithinSteps` in the sum of the step bounds. -/

From 6833eb1c179959bdcb12eaff15e5c267b27e737e Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <crei.github@gmail.com>
Date: Thu, 27 Aug 2026 12:30:14 +0200
Subject: [PATCH 18/20] Update Cslib/Foundations/Data/List/IsChainFromTo.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 Cslib/Foundations/Data/List/IsChainFromTo.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index 6e32e807c..998ae187b 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -137,7 +137,7 @@ lemma IsChainFromTo.append_dropLast (hc : chain.IsChainFromTo r a b) {chain' : L
 `chain[i]`. -/
 lemma IsChainFromTo.take (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
     (chain.take (i + 1)).IsChainFromTo r a chain[i] := by
-  have : chain.take (i + 1) ≠ [] := by grind [ne_nil_iff_length_pos, length_take]
+  have : chain.take (i + 1) ≠ [] := by grind only [length_nil, min_def, length_take]
   exact ⟨hc.isChain.take _, this, by grind, by grind [chain.getLast_take this]⟩
 
 /-- Dropping the first `i` elements of a chain yields a chain from `chain[i]` to the same end

From 3ecf3e06a7c58a39dc85a2f4344872fae0c77e6e Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <crei.github@gmail.com>
Date: Thu, 27 Aug 2026 12:30:31 +0200
Subject: [PATCH 19/20] Update Cslib/Foundations/Data/List/IsChainFromTo.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 Cslib/Foundations/Data/List/IsChainFromTo.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index 998ae187b..08f95e069 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -165,8 +165,7 @@ lemma IsChainFromTo.head_induction_on
     exact h_head hrel this (ih this rfl)
 
 /-- Any element of an `r`-chain from `a` to `b` is reflexively-transitively related from `a`. -/
-lemma IsChainFromTo.reflTransGen_of_mem (hc : chain.IsChainFromTo r a b) {x : α}
-    (mem : x ∈ chain) :
+lemma IsChainFromTo.reflTransGen_of_mem (hc : chain.IsChainFromTo r a b) {x : α} (mem : x ∈ chain) :
     Relation.ReflTransGen r a x := by
   obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem mem
   exact (hc.take hi).reflTransGen

From da3cec467e10b496afdac180a9c6db9412638d03 Mon Sep 17 00:00:00 2001
From: Christian Reitwiessner <crei.github@gmail.com>
Date: Thu, 27 Aug 2026 12:30:57 +0200
Subject: [PATCH 20/20] Update Cslib/Foundations/Data/List/IsChainFromTo.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 Cslib/Foundations/Data/List/IsChainFromTo.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
index 08f95e069..07383e01b 100644
--- a/Cslib/Foundations/Data/List/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -155,9 +155,7 @@ lemma IsChainFromTo.head_induction_on
       motive hc → motive (hc.cons hab))
     {chain : List α} {a b : α} (hc : chain.IsChainFromTo r a b) : motive hc := by
   induction htail : chain.tail generalizing chain a with
-  | nil =>
-    obtain rfl : chain = [a] := by grind
-    grind
+  | nil => grind => have : chain = [a]; finish
   | cons a' tail ih =>
     obtain rfl : chain = a :: a' :: tail := by grind
     obtain ⟨hrel, hchain⟩ := isChain_cons_cons.mp hc.isChain