From a50ccd5df090eca215de54b41870874ccad99401 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 11 May 2026 04:33:34 -0400
Subject: [PATCH 01/20] {left,right}Total_equiv

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

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 29635bee6..3972f88b2 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -105,6 +105,10 @@ theorem antisymm_rightUnique [Std.Antisymm r] : Relator.RightUnique r := by
 theorem rightUnique_antisymm (h : Relator.RightUnique r) : Std.Antisymm r where
   antisymm _ _ ab ba := h ba (refl_range ab)
 
+theorem rightTotal_equiv (h : Relator.RightTotal r) : IsEquiv α r := by
+  have : Std.Refl r := ⟨fun a => refl_range (h a).choose_spec⟩
+  exact {toIsTrans := ⟨fun _ _ _ ab bc => rightEuclidean (symm ab) bc⟩}
+
 end RightEuclidean
 
 namespace LeftEuclidean
@@ -135,6 +139,10 @@ theorem antisymm_leftUnique [Std.Antisymm r] : Relator.LeftUnique r := by
 theorem leftUnique_antisymm (h : Relator.LeftUnique r) : Std.Antisymm r where
   antisymm _ _ ab ba := h ab (refl_dom ba)
 
+theorem leftTotal_equiv (h : Relator.LeftTotal r) : IsEquiv α r := by
+  have : Std.Refl r := ⟨fun a => refl_dom (h a).choose_spec⟩
+  exact {toIsTrans := ⟨fun _ _ _ ab bc => leftEuclidean ab (symm bc)⟩}
+
 end LeftEuclidean
 
 section euclidean_symm

From 7bac1f4629530fe9a791c338acfc62e5b1fad091 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 12 May 2026 11:47:02 -0400
Subject: [PATCH 02/20] fintype_trichotomous_antisymm_card

---
 Cslib/Foundations/Data/Relation.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 3972f88b2..30f9b1e4c 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -11,6 +11,7 @@ public import Mathlib.Data.List.TFAE
 public import Mathlib.Order.Comparable
 public import Mathlib.Order.WellFounded
 public import Mathlib.Order.BooleanAlgebra.Basic
+public import Mathlib.Data.Fintype.Card
 
 /-! # Relations
 
@@ -109,6 +110,17 @@ theorem rightTotal_equiv (h : Relator.RightTotal r) : IsEquiv α r := by
   have : Std.Refl r := ⟨fun a => refl_range (h a).choose_spec⟩
   exact {toIsTrans := ⟨fun _ _ _ ab bc => rightEuclidean (symm ab) bc⟩}
 
+theorem fintype_trichotomous_antisymm_card [Fintype α] [Std.Trichotomous r] [Std.Antisymm r] :
+    Fintype.card α ≤ 2 := by
+  by_contra! h
+  have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a b
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a c
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b c
+  have := antisymm_rightUnique (r := r) 
+  have := @refl_range (r := r)
+  grind [Relator.RightUnique]
+
 end RightEuclidean
 
 namespace LeftEuclidean
@@ -143,6 +155,17 @@ theorem leftTotal_equiv (h : Relator.LeftTotal r) : IsEquiv α r := by
   have : Std.Refl r := ⟨fun a => refl_dom (h a).choose_spec⟩
   exact {toIsTrans := ⟨fun _ _ _ ab bc => leftEuclidean ab (symm bc)⟩}
 
+theorem fintype_trichotomous_antisymm_card [Fintype α] [Std.Trichotomous r] [Std.Antisymm r] :
+    Fintype.card α ≤ 2 := by
+  by_contra! h
+  have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a b
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a c
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b c
+  have := antisymm_leftUnique (r := r) 
+  have := @refl_dom (r := r)
+  grind [Relator.LeftUnique]
+
 end LeftEuclidean
 
 section euclidean_symm

From e62c9564165ad4eb2768a9c67b3ff1d235457c7c Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 17 May 2026 12:45:40 -0400
Subject: [PATCH 03/20] move apart fintype and finite

---
 Cslib/Foundations/Data/Relation.lean | 46 ++++++++++++++++++++++------
 1 file changed, 37 insertions(+), 9 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 30f9b1e4c..eeef0d3cd 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -11,7 +11,7 @@ public import Mathlib.Data.List.TFAE
 public import Mathlib.Order.Comparable
 public import Mathlib.Order.WellFounded
 public import Mathlib.Order.BooleanAlgebra.Basic
-public import Mathlib.Data.Fintype.Card
+public import Mathlib.Data.Fintype.EquivFin
 
 /-! # Relations
 
@@ -110,10 +110,9 @@ theorem rightTotal_equiv (h : Relator.RightTotal r) : IsEquiv α r := by
   have : Std.Refl r := ⟨fun a => refl_range (h a).choose_spec⟩
   exact {toIsTrans := ⟨fun _ _ _ ab bc => rightEuclidean (symm ab) bc⟩}
 
-theorem fintype_trichotomous_antisymm_card [Fintype α] [Std.Trichotomous r] [Std.Antisymm r] :
-    Fintype.card α ≤ 2 := by
-  by_contra! h
-  have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
+private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
+    ¬ ∃ (a b c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c := by
+  rintro ⟨a, b, c, _⟩
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a b
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a c
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b c
@@ -121,6 +120,21 @@ theorem fintype_trichotomous_antisymm_card [Fintype α] [Std.Trichotomous r] [St
   have := @refl_range (r := r)
   grind [Relator.RightUnique]
 
+theorem trichotomous_antisymm_finite [Std.Trichotomous r] [Std.Antisymm r] : Finite α := by
+  classical
+  by_contra! h
+  apply three_contra (r := r)
+  have ⟨_, hcard⟩ := Infinite.exists_subset_card_eq α 3
+  have ⟨a, b, c, _, _, _, _⟩ := Finset.card_eq_three.mp hcard
+  use a, b, c
+
+theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintype α] :
+    Fintype.card α ≤ 2 := by
+  by_contra! h
+  apply three_contra (r := r)
+  have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
+  use a, b, c
+
 end RightEuclidean
 
 namespace LeftEuclidean
@@ -155,10 +169,9 @@ theorem leftTotal_equiv (h : Relator.LeftTotal r) : IsEquiv α r := by
   have : Std.Refl r := ⟨fun a => refl_dom (h a).choose_spec⟩
   exact {toIsTrans := ⟨fun _ _ _ ab bc => leftEuclidean ab (symm bc)⟩}
 
-theorem fintype_trichotomous_antisymm_card [Fintype α] [Std.Trichotomous r] [Std.Antisymm r] :
-    Fintype.card α ≤ 2 := by
-  by_contra! h
-  have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
+private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
+    ¬ ∃ (a b c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c := by
+  rintro ⟨a, b, c, _⟩
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a b
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a c
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b c
@@ -166,6 +179,21 @@ theorem fintype_trichotomous_antisymm_card [Fintype α] [Std.Trichotomous r] [St
   have := @refl_dom (r := r)
   grind [Relator.LeftUnique]
 
+theorem trichotomous_antisymm_finite [Std.Trichotomous r] [Std.Antisymm r] : Finite α := by
+  classical
+  by_contra! h
+  apply three_contra (r := r)
+  have ⟨_, hcard⟩ := Infinite.exists_subset_card_eq α 3
+  have ⟨a, b, c, _, _, _, _⟩ := Finset.card_eq_three.mp hcard
+  use a, b, c
+
+theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintype α] :
+    Fintype.card α ≤ 2 := by
+  by_contra! h
+  apply three_contra (r := r)
+  have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
+  use a, b, c
+
 end LeftEuclidean
 
 section euclidean_symm

From 7d27d480946bccb5948eee227e250ababa473100 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 17 May 2026 12:58:44 -0400
Subject: [PATCH 04/20] cod rename, subset theorems

---
 Cslib/Foundations/Data/Relation.lean | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index eeef0d3cd..523259acc 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -83,7 +83,7 @@ namespace RightEuclidean
 variable [RightEuclidean r]
 
 /-- A `RightEuclidean` relation is reflexive on its range -/
-theorem refl_range (ab : r a b) : r b b := rightEuclidean ab ab
+theorem refl_cod (ab : r a b) : r b b := rightEuclidean ab ab
 
 /-- The converse of a `RightEuclidean` relation is `LeftEuclidean` -/
 theorem leftEuclidean_swap : LeftEuclidean (fun a b => r b a) where
@@ -95,7 +95,7 @@ instance [Std.Refl r] : Std.Symm r where
 theorem trichotomous_trans [Std.Trichotomous r] : IsTrans α r where
   trans a b c ab bc := by
     have := Std.Trichotomous.trichotomous (r := r) a c
-    have cc := refl_range bc
+    have cc := refl_cod bc
     have (ca : r c a) := rightEuclidean ca cc
     grind
 
@@ -104,10 +104,10 @@ theorem antisymm_rightUnique [Std.Antisymm r] : Relator.RightUnique r := by
   exact antisymm (rightEuclidean ab ac) (rightEuclidean ac ab)
 
 theorem rightUnique_antisymm (h : Relator.RightUnique r) : Std.Antisymm r where
-  antisymm _ _ ab ba := h ba (refl_range ab)
+  antisymm _ _ ab ba := h ba (refl_cod ab)
 
 theorem rightTotal_equiv (h : Relator.RightTotal r) : IsEquiv α r := by
-  have : Std.Refl r := ⟨fun a => refl_range (h a).choose_spec⟩
+  have : Std.Refl r := ⟨fun a => refl_cod (h a).choose_spec⟩
   exact {toIsTrans := ⟨fun _ _ _ ab bc => rightEuclidean (symm ab) bc⟩}
 
 private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
@@ -117,7 +117,7 @@ private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a c
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b c
   have := antisymm_rightUnique (r := r) 
-  have := @refl_range (r := r)
+  have := @refl_cod (r := r)
   grind [Relator.RightUnique]
 
 theorem trichotomous_antisymm_finite [Std.Trichotomous r] [Std.Antisymm r] : Finite α := by
@@ -135,6 +135,12 @@ theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintyp
   have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
   use a, b, c
 
+theorem cod_subset_dom : {b | ∃ a, r a b} ⊆ {a | ∃ b, r a b} := by
+  simp only [Set.setOf_subset_setOf, forall_exists_index]
+  intro a b ba
+  use a
+  exact refl_cod ba
+
 end RightEuclidean
 
 namespace LeftEuclidean
@@ -194,6 +200,12 @@ theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintyp
   have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
   use a, b, c
 
+theorem dom_subset_cod : {a | ∃ b, r a b} ⊆ {b | ∃ a, r a b} := by
+  simp only [Set.setOf_subset_setOf, forall_exists_index]
+  intro a b ba
+  use a
+  exact refl_dom ba
+
 end LeftEuclidean
 
 section euclidean_symm

From 717d19b9d14acca521c78dc169a1be4f76edbc36 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 17 May 2026 15:44:53 -0400
Subject: [PATCH 05/20] better proofs

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

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 523259acc..03a6522ac 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -136,10 +136,8 @@ theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintyp
   use a, b, c
 
 theorem cod_subset_dom : {b | ∃ a, r a b} ⊆ {a | ∃ b, r a b} := by
-  simp only [Set.setOf_subset_setOf, forall_exists_index]
-  intro a b ba
-  use a
-  exact refl_cod ba
+  rintro b ⟨a, ab⟩
+  exact ⟨b, refl_cod ab⟩
 
 end RightEuclidean
 
@@ -201,10 +199,8 @@ theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintyp
   use a, b, c
 
 theorem dom_subset_cod : {a | ∃ b, r a b} ⊆ {b | ∃ a, r a b} := by
-  simp only [Set.setOf_subset_setOf, forall_exists_index]
-  intro a b ba
-  use a
-  exact refl_dom ba
+  rintro a ⟨b, ab⟩
+  refine ⟨a, refl_dom ab⟩
 
 end LeftEuclidean
 

From 4dfc1b09dc5012ee20173be0085daf83d1bc5cb7 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 17 May 2026 17:28:15 -0400
Subject: [PATCH 06/20] don't duplicate Relator.LeftTotal

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

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 03a6522ac..57adc3491 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -318,9 +318,9 @@ theorem Confluent_of_unique_end {x : α} (h : ∀ y : α, ReflTransGen r y x) :
 /-- An element is reducible with respect to a relation if there is a value it is related to. -/
 abbrev Reducible (r : α → α → Prop) (x : α) : Prop := ∃ y, r x y
 
-/-- A relation `r` is serial if every element is `Reducible`. -/
+/-- A relation `r` is serial if every element is `Reducible`, i.e. `Relator.LeftTotal`. -/
 class Serial (r : α → α → Prop) where
-  serial a : Reducible r a
+  serial : Relator.LeftTotal r
 
 @[scoped grind →]
 lemma refl_serial (r : α → α → Prop) (h : Std.Refl r) : Relation.Serial r where

From fb43aaab1c75f9deb071494420eb1b0c8fc5a2b0 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 17 May 2026 17:57:07 -0400
Subject: [PATCH 07/20] Std.Trichotomous.{dom,cod}_eq

---
 Cslib/Foundations/Data/Relation.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 57adc3491..276048a08 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -25,6 +25,18 @@ public import Mathlib.Data.Fintype.EquivFin
 
 variable {α : Type*} {r : α → α → Prop}
 
+theorem Std.Trichotomous.cod_eq [Std.Trichotomous r] : Subsingleton {b | ∀ a, ¬ r a b} := by
+  constructor
+  rintro ⟨b₁, _⟩ ⟨b₂, _⟩
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b₁ b₂
+  grind
+
+theorem Std.Trichotomous.dom_eq [Std.Trichotomous r] : Subsingleton {a | ∀ b, ¬ r a b} := by
+  constructor
+  rintro ⟨a₁, _⟩ ⟨a₂, _⟩
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a₁ a₂
+  grind
+
 theorem WellFounded.ofTransGen (trans_wf : WellFounded (Relation.TransGen r)) : WellFounded r := by
   grind [WellFounded.wellFounded_iff_has_min, Relation.TransGen]
 

From 3d0a8163ac752ef56d30c52c4e84cae708f90a2f Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 18 May 2026 11:42:11 -0400
Subject: [PATCH 08/20] dom and cod

---
 Cslib/Foundations/Data/Relation.lean | 46 ++++++++++++++++++++++++++--
 1 file changed, 43 insertions(+), 3 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 276048a08..198469fef 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -23,7 +23,7 @@ public import Mathlib.Data.Fintype.EquivFin
 
 @[expose] public section
 
-variable {α : Type*} {r : α → α → Prop}
+variable {α : Type*} {r r₁ r₂ : α → α → Prop}
 
 theorem Std.Trichotomous.cod_eq [Std.Trichotomous r] : Subsingleton {b | ∀ a, ¬ r a b} := by
   constructor
@@ -46,6 +46,46 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou
 
 namespace Relation
 
+/-- Domain of a relation. -/
+def dom (r : α → α → Prop) : Set α := {a | ∃ b, r a b}
+
+/-- Codomain of a relation, aka range. -/
+def cod (r : α → α → Prop) : Set α := {b | ∃ a, r a b}
+
+@[simp, grind =] lemma mem_dom : a ∈ dom r ↔ ∃ b, r a b := .rfl
+@[simp, grind =] lemma mem_cod : b ∈ cod r ↔ ∃ a, r a b := .rfl
+
+@[gcongr] lemma dom_mono (h : r₁ ≤ r₂) : dom r₁ ⊆ dom r₂ := fun a ⟨b, hab⟩ => ⟨b, h a b hab⟩
+@[gcongr] lemma cod_mono (h : r₁ ≤ r₂) : cod r₁ ⊆ cod r₂ := fun b ⟨a, hab⟩ => ⟨a, h a b hab⟩
+
+@[simp, grind =]
+lemma dom_empty : dom (emptyRelation : α → α → Prop) = ∅ := by grind [emptyRelation, dom]
+
+@[simp, grind =]
+lemma cod_empty : cod (emptyRelation : α → α → Prop) = ∅ := by grind [emptyRelation, cod]
+
+@[simp, grind =]
+lemma dom_eq_empty_iff : dom r = ∅ ↔ r = emptyRelation where
+  mp h := by
+    ext a b
+    simp
+    grind => have : a ∈ dom r; finish
+  mpr := by grind
+
+@[simp, grind =]
+lemma cod_eq_empty_iff : cod r = ∅ ↔ r = emptyRelation where
+  mp h := by
+    ext a b
+    simp
+    grind => have : b ∈ cod r; finish
+  mpr h := by grind
+
+@[simp]
+lemma cod_inv : cod (fun a b => r b a) = dom r := rfl
+
+@[simp]
+lemma dom_inv : dom (fun a b => r b a) = cod r := rfl
+
 /-- The empty (heterogeneous) relation, which always returns `False`. -/
 @[nolint unusedArguments]
 def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False
@@ -147,7 +187,7 @@ theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintyp
   have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
   use a, b, c
 
-theorem cod_subset_dom : {b | ∃ a, r a b} ⊆ {a | ∃ b, r a b} := by
+theorem cod_subset_dom : cod r ⊆ dom r := by
   rintro b ⟨a, ab⟩
   exact ⟨b, refl_cod ab⟩
 
@@ -210,7 +250,7 @@ theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintyp
   have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
   use a, b, c
 
-theorem dom_subset_cod : {a | ∃ b, r a b} ⊆ {b | ∃ a, r a b} := by
+theorem dom_subset_cod : dom r ⊆ cod r := by
   rintro a ⟨b, ab⟩
   refine ⟨a, refl_dom ab⟩
 

From 0e2da096dbd1bdf7debf793bdebd3edca665e511 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 18 May 2026 12:43:58 -0400
Subject: [PATCH 09/20] use complement

---
 Cslib/Foundations/Data/Relation.lean | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 198469fef..f20945129 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -25,18 +25,6 @@ public import Mathlib.Data.Fintype.EquivFin
 
 variable {α : Type*} {r r₁ r₂ : α → α → Prop}
 
-theorem Std.Trichotomous.cod_eq [Std.Trichotomous r] : Subsingleton {b | ∀ a, ¬ r a b} := by
-  constructor
-  rintro ⟨b₁, _⟩ ⟨b₂, _⟩
-  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b₁ b₂
-  grind
-
-theorem Std.Trichotomous.dom_eq [Std.Trichotomous r] : Subsingleton {a | ∀ b, ¬ r a b} := by
-  constructor
-  rintro ⟨a₁, _⟩ ⟨a₂, _⟩
-  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a₁ a₂
-  grind
-
 theorem WellFounded.ofTransGen (trans_wf : WellFounded (Relation.TransGen r)) : WellFounded r := by
   grind [WellFounded.wellFounded_iff_has_min, Relation.TransGen]
 
@@ -86,6 +74,20 @@ lemma cod_inv : cod (fun a b => r b a) = dom r := rfl
 @[simp]
 lemma dom_inv : dom (fun a b => r b a) = cod r := rfl
 
+theorem _root_.Std.Trichotomous.subsingleton_cod [Std.Trichotomous r] :
+    Subsingleton <| ((cod r)ᶜ : Set α) := by
+  constructor
+  rintro ⟨b₁, _⟩ ⟨b₂, _⟩
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b₁ b₂
+  grind
+
+theorem _root_.Std.Trichotomous.subsingleton_dom [Std.Trichotomous r] :
+    Subsingleton <| ((dom r)ᶜ : Set α) := by
+  constructor
+  rintro ⟨a₁, _⟩ ⟨a₂, _⟩
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a₁ a₂
+  grind
+
 /-- The empty (heterogeneous) relation, which always returns `False`. -/
 @[nolint unusedArguments]
 def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False

From 0daab4481cd13034890ae6b5c6b55f3334abfbff Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 18 May 2026 15:25:06 -0400
Subject: [PATCH 10/20] equiv_{dom,cod}

---
 Cslib/Foundations/Data/Relation.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index f20945129..ec39cd560 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -193,6 +193,17 @@ theorem cod_subset_dom : cod r ⊆ dom r := by
   rintro b ⟨a, ab⟩
   exact ⟨b, refl_cod ab⟩
 
+instance : RightEuclidean fun a b : cod r => r a b where
+  rightEuclidean := rightEuclidean
+
+instance : RightEuclidean fun a b : dom r => r a b where
+  rightEuclidean := rightEuclidean
+
+theorem rightTotal_cod : Relator.RightTotal (fun a b : cod r => r a b) :=
+  fun ⟨_, _, h⟩ => ⟨_, refl_cod h⟩
+
+theorem equiv_cod : IsEquiv (cod r) (fun a b => r a b) := rightTotal_equiv rightTotal_cod
+
 end RightEuclidean
 
 namespace LeftEuclidean
@@ -256,6 +267,17 @@ theorem dom_subset_cod : dom r ⊆ cod r := by
   rintro a ⟨b, ab⟩
   refine ⟨a, refl_dom ab⟩
 
+instance : LeftEuclidean fun a b : dom r => r a b where
+  leftEuclidean := leftEuclidean
+
+instance : LeftEuclidean fun a b : dom r => r a b where
+  leftEuclidean := leftEuclidean
+
+theorem leftTotal_dom : Relator.LeftTotal (fun a b : dom r => r a b) :=
+  fun ⟨_, _, h⟩ => ⟨_, refl_dom h⟩
+
+theorem equiv_dom : IsEquiv (dom r) (fun a b => r a b) := leftTotal_equiv leftTotal_dom
+
 end LeftEuclidean
 
 section euclidean_symm

From b83f4e0670cf46c99290bf361fcc6bd72e1dfe6b Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 18 May 2026 19:21:51 -0400
Subject: [PATCH 11/20] leftEuclidean_rightEuclidean_iff_dom_cod

---
 Cslib/Foundations/Data/Relation.lean | 47 +++++++++++++++++++++++-----
 1 file changed, 39 insertions(+), 8 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index ec39cd560..64414d18f 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -40,6 +40,12 @@ def dom (r : α → α → Prop) : Set α := {a | ∃ b, r a b}
 /-- Codomain of a relation, aka range. -/
 def cod (r : α → α → Prop) : Set α := {b | ∃ a, r a b}
 
+instance : CoeDep (α → α → Prop) r (dom r → dom r → Prop) where
+  coe a b := r a b
+
+instance : CoeDep (α → α → Prop) r (cod r → cod r → Prop) where
+  coe a b := r a b
+
 @[simp, grind =] lemma mem_dom : a ∈ dom r ↔ ∃ b, r a b := .rfl
 @[simp, grind =] lemma mem_cod : b ∈ cod r ↔ ∃ a, r a b := .rfl
 
@@ -193,16 +199,16 @@ theorem cod_subset_dom : cod r ⊆ dom r := by
   rintro b ⟨a, ab⟩
   exact ⟨b, refl_cod ab⟩
 
-instance : RightEuclidean fun a b : cod r => r a b where
+instance : RightEuclidean (α := cod r) r where
   rightEuclidean := rightEuclidean
 
-instance : RightEuclidean fun a b : dom r => r a b where
+instance : RightEuclidean (α := dom r) r where
   rightEuclidean := rightEuclidean
 
-theorem rightTotal_cod : Relator.RightTotal (fun a b : cod r => r a b) :=
+theorem rightTotal_cod : Relator.RightTotal (α := cod r) (β := cod r) r :=
   fun ⟨_, _, h⟩ => ⟨_, refl_cod h⟩
 
-theorem equiv_cod : IsEquiv (cod r) (fun a b => r a b) := rightTotal_equiv rightTotal_cod
+theorem equiv_cod : IsEquiv (cod r) r := rightTotal_equiv rightTotal_cod
 
 end RightEuclidean
 
@@ -267,16 +273,16 @@ theorem dom_subset_cod : dom r ⊆ cod r := by
   rintro a ⟨b, ab⟩
   refine ⟨a, refl_dom ab⟩
 
-instance : LeftEuclidean fun a b : dom r => r a b where
+instance : LeftEuclidean (α := cod r) r where
   leftEuclidean := leftEuclidean
 
-instance : LeftEuclidean fun a b : dom r => r a b where
+instance : LeftEuclidean (α := dom r) r where
   leftEuclidean := leftEuclidean
 
-theorem leftTotal_dom : Relator.LeftTotal (fun a b : dom r => r a b) :=
+theorem leftTotal_dom : Relator.LeftTotal (α := dom r) (β := dom r) r :=
   fun ⟨_, _, h⟩ => ⟨_, refl_dom h⟩
 
-theorem equiv_dom : IsEquiv (dom r) (fun a b => r a b) := leftTotal_equiv leftTotal_dom
+theorem equiv_dom : IsEquiv (dom r) r := leftTotal_equiv leftTotal_dom
 
 end LeftEuclidean
 
@@ -315,6 +321,31 @@ theorem symm_rightEuclidean_iff_trans : RightEuclidean r ↔ IsTrans α r :=
 
 end euclidean_symm
 
+theorem leftEuclidean_rightEuclidean_dom_cod_eq [LeftEuclidean r] [RightEuclidean r] :
+    dom r = cod r := by
+  have : dom r ⊆ cod r := LeftEuclidean.dom_subset_cod
+  have : cod r ⊆ dom r := RightEuclidean.cod_subset_dom
+  grind
+
+theorem dom_cod_leftEuclidean (eq : dom r = cod r) [equiv_dom : IsEquiv (dom r) r] :
+    LeftEuclidean r where
+  leftEuclidean {a b c} ac bc := by
+    have cb : r c b := equiv_dom.symm ⟨_, _, bc⟩ ⟨c, by grind⟩ bc
+    exact equiv_dom.trans ⟨_, _, ac⟩ ⟨_, _, cb⟩ ⟨_, by grind⟩ ac cb
+
+lemma dom_cod_rightEuclidean (eq : dom r = cod r) [equiv_dom : IsEquiv (dom r) r] :
+    RightEuclidean r where
+  rightEuclidean {a b c} ab ac := by
+    have ba : r b a := equiv_dom.symm ⟨a, _, ab⟩ ⟨b, by grind⟩ ab
+    exact equiv_dom.trans ⟨_, _, ba⟩ ⟨_, _, ac⟩ ⟨c, by grind⟩ ba ac
+
+/-- A relation is both left and right Euclidean if and only if the relation is an equivalence on
+  coinciding domain and codomain. -/
+theorem leftEuclidean_rightEuclidean_iff_dom_cod :
+    LeftEuclidean r ∧ RightEuclidean r ↔ dom r = cod r ∧ IsEquiv (dom r) r where
+  mp := fun ⟨_, _⟩ ↦ ⟨leftEuclidean_rightEuclidean_dom_cod_eq, LeftEuclidean.equiv_dom⟩
+  mpr := fun ⟨eq, _⟩ ↦ ⟨dom_cod_leftEuclidean eq, dom_cod_rightEuclidean eq⟩
+
 /-- A relation has the diamond property when all reductions with a common origin are joinable -/
 abbrev Diamond (r : α → α → Prop) := ∀ {a b c : α}, r a b → r a c → Join r b c
 

From 69773f58fc1aab4fb2bdc6c078c11db68de80b87 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 18 May 2026 19:59:10 -0400
Subject: [PATCH 12/20] {left,right}Unique_trans

---
 Cslib/Foundations/Data/Relation.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 64414d18f..9659256e7 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -166,6 +166,11 @@ theorem antisymm_rightUnique [Std.Antisymm r] : Relator.RightUnique r := by
 theorem rightUnique_antisymm (h : Relator.RightUnique r) : Std.Antisymm r where
   antisymm _ _ ab ba := h ba (refl_cod ab)
 
+theorem rightUnique_trans (h : Relator.RightUnique r) : IsTrans α r where
+  trans a b c ab bc := by
+    have eq : c = b := h bc (refl_cod ab)
+    simpa [eq]
+
 theorem rightTotal_equiv (h : Relator.RightTotal r) : IsEquiv α r := by
   have : Std.Refl r := ⟨fun a => refl_cod (h a).choose_spec⟩
   exact {toIsTrans := ⟨fun _ _ _ ab bc => rightEuclidean (symm ab) bc⟩}
@@ -240,6 +245,11 @@ theorem antisymm_leftUnique [Std.Antisymm r] : Relator.LeftUnique r := by
 theorem leftUnique_antisymm (h : Relator.LeftUnique r) : Std.Antisymm r where
   antisymm _ _ ab ba := h ab (refl_dom ba)
 
+theorem leftUnique_trans (h : Relator.LeftUnique r) : IsTrans α r where
+  trans a b c ab bc := by
+    have eq : a = b := h ab (refl_dom bc)
+    simpa [eq]
+
 theorem leftTotal_equiv (h : Relator.LeftTotal r) : IsEquiv α r := by
   have : Std.Refl r := ⟨fun a => refl_dom (h a).choose_spec⟩
   exact {toIsTrans := ⟨fun _ _ _ ab bc => leftEuclidean ab (symm bc)⟩}

From cf58fe4dd582ffc36cb9ca35c1e60d6da4af6718 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 18 May 2026 21:09:36 -0400
Subject: [PATCH 13/20] total unique trans

---
 Cslib/Foundations/Data/Relation.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 9659256e7..3a9ff17a4 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -23,6 +23,8 @@ public import Mathlib.Data.Fintype.EquivFin
 
 @[expose] public section
 
+open Relator
+
 variable {α : Type*} {r r₁ r₂ : α → α → Prop}
 
 theorem WellFounded.ofTransGen (trans_wf : WellFounded (Relation.TransGen r)) : WellFounded r := by
@@ -175,6 +177,16 @@ theorem rightTotal_equiv (h : Relator.RightTotal r) : IsEquiv α r := by
   have : Std.Refl r := ⟨fun a => refl_cod (h a).choose_spec⟩
   exact {toIsTrans := ⟨fun _ _ _ ab bc => rightEuclidean (symm ab) bc⟩}
 
+omit [RightEuclidean r] in
+theorem leftTotal_rightUnique_trans (h₁ : LeftTotal r) (h₂ : RightUnique r) [IsTrans α r] :
+    RightEuclidean r where
+  rightEuclidean {a b c} ab ac := by
+    obtain ⟨d, dc⟩ := h₁ c
+    have : r a d := _root_.trans ac dc
+    have : b = c := h₂ ab ac
+    have : d = c := h₂ (_root_.trans ac dc) ac
+    grind
+
 private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
     ¬ ∃ (a b c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c := by
   rintro ⟨a, b, c, _⟩
@@ -254,6 +266,15 @@ theorem leftTotal_equiv (h : Relator.LeftTotal r) : IsEquiv α r := by
   have : Std.Refl r := ⟨fun a => refl_dom (h a).choose_spec⟩
   exact {toIsTrans := ⟨fun _ _ _ ab bc => leftEuclidean ab (symm bc)⟩}
 
+omit [LeftEuclidean r] in
+theorem rightTotal_leftUnique_trans (h₁ : RightTotal r) (h₂ : LeftUnique r) [IsTrans α r] :
+    LeftEuclidean r where
+  leftEuclidean {a b c} ac bc := by
+    obtain ⟨d, da⟩ := h₁ a
+    have : a = b := h₂ ac bc
+    have : a = d := h₂ ac (_root_.trans da ac)
+    grind
+
 private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
     ¬ ∃ (a b c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c := by
   rintro ⟨a, b, c, _⟩

From 2a9bd537250b7a92c4500f4367c285bd6c11ecd2 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 19 May 2026 00:50:10 -0400
Subject: [PATCH 14/20] reference

---
 Cslib/Foundations/Data/Relation.lean |  1 +
 references.bib                       | 12 ++++++++++++
 2 files changed, 13 insertions(+)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 3a9ff17a4..0348beaba 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -18,6 +18,7 @@ public import Mathlib.Data.Fintype.EquivFin
 ## References
 
 * [*Term Rewriting and All That*][Baader1998]
+* [*Simple Laws about Nonprominent Properties of Binary Relations*][Burghardt2018]
 
 -/
 
diff --git a/references.bib b/references.bib
index f0db1a781..47ae2c4e4 100644
--- a/references.bib
+++ b/references.bib
@@ -49,6 +49,18 @@ @book{Blackburn2001
   collection={Cambridge Tracts in Theoretical Computer Science}
 }
 
+@misc{Burghardt2018,
+	title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}},
+	url = {https://arxiv.org/abs/1806.05036v2},
+	abstract = {We checked each binary relation on a 5-element set for a given set of properties, including usual ones like asymmetry and less known ones like Euclideanness. Using a poor man's Quine-McCluskey algorithm, we computed prime implicants of non-occurring property combinations, like "not irreflexive, but asymmetric". We considered the non-trivial laws obtained this way, and manually proved them true for binary relations on arbitrary sets, thus contributing to the encyclopedic knowledge about less known properties.},
+	language = {en},
+	urldate = {2026-05-19},
+	journal = {arXiv.org},
+	author = {Burghardt, Jochen},
+	month = jun,
+	year = {2018},
+}
+
 @inproceedings{Danielsson2008,
 author = {Danielsson, Nils Anders},
 title = {Lightweight semiformal time complexity analysis for purely functional data structures},

From 16602f0d1a46c0b3846c549da27d421376cbd3ea Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 19 May 2026 10:14:03 -0400
Subject: [PATCH 15/20] primed refl theorems

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

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 0348beaba..58235dbe9 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -148,6 +148,8 @@ variable [RightEuclidean r]
 /-- A `RightEuclidean` relation is reflexive on its range -/
 theorem refl_cod (ab : r a b) : r b b := rightEuclidean ab ab
 
+theorem refl_cod' : b ∈ cod r → r b b := fun ⟨_, ab⟩ ↦ refl_cod ab
+
 /-- The converse of a `RightEuclidean` relation is `LeftEuclidean` -/
 theorem leftEuclidean_swap : LeftEuclidean (fun a b => r b a) where
   leftEuclidean ca cb := rightEuclidean cb ca
@@ -237,6 +239,8 @@ variable [LeftEuclidean r]
 /-- A `LeftEuclidean` relation is reflexive on its domain -/
 theorem refl_dom (ab : r a b) : r a a := leftEuclidean ab ab
 
+theorem refl_dom' : a ∈ dom r → r a a := fun ⟨_, ab⟩ ↦ refl_dom ab
+
 /-- The converse of a `LeftEuclidean` relation is `RightEuclidean` -/
 theorem rightEuclidean_swap : RightEuclidean (fun a b => r b a) where
   rightEuclidean ab ac := leftEuclidean ac ab

From c9babf45d4b6861b16bfd83f3f530331b897918c Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 19 May 2026 10:21:49 -0400
Subject: [PATCH 16/20] small golf

---
 Cslib/Foundations/Data/Relation.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 58235dbe9..a071174fe 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -185,7 +185,6 @@ theorem leftTotal_rightUnique_trans (h₁ : LeftTotal r) (h₂ : RightUnique r)
     RightEuclidean r where
   rightEuclidean {a b c} ab ac := by
     obtain ⟨d, dc⟩ := h₁ c
-    have : r a d := _root_.trans ac dc
     have : b = c := h₂ ab ac
     have : d = c := h₂ (_root_.trans ac dc) ac
     grind
@@ -215,9 +214,7 @@ theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintyp
   have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
   use a, b, c
 
-theorem cod_subset_dom : cod r ⊆ dom r := by
-  rintro b ⟨a, ab⟩
-  exact ⟨b, refl_cod ab⟩
+theorem cod_subset_dom : cod r ⊆ dom r := fun b ⟨_, ab⟩ ↦ ⟨b, refl_cod ab⟩
 
 instance : RightEuclidean (α := cod r) r where
   rightEuclidean := rightEuclidean
@@ -305,9 +302,7 @@ theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintyp
   have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
   use a, b, c
 
-theorem dom_subset_cod : dom r ⊆ cod r := by
-  rintro a ⟨b, ab⟩
-  refine ⟨a, refl_dom ab⟩
+theorem dom_subset_cod : dom r ⊆ cod r := fun a ⟨_, ab⟩ ↦ ⟨a, refl_dom ab⟩
 
 instance : LeftEuclidean (α := cod r) r where
   leftEuclidean := leftEuclidean

From fac69edec53d7718dd289871aa907c38ccafa401 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 19 May 2026 12:40:54 -0400
Subject: [PATCH 17/20] whitespace

---
 Cslib/Foundations/Data/Relation.lean | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index a071174fe..dc8ca9a5b 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -195,7 +195,7 @@ private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a b
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a c
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b c
-  have := antisymm_rightUnique (r := r) 
+  have := antisymm_rightUnique (r := r)
   have := @refl_cod (r := r)
   grind [Relator.RightUnique]
 
@@ -227,6 +227,29 @@ theorem rightTotal_cod : Relator.RightTotal (α := cod r) (β := cod r) r :=
 
 theorem equiv_cod : IsEquiv (cod r) r := rightTotal_equiv rightTotal_cod
 
+def dom_at (r : α → α → Prop) (x : α) : Set α := {y | r x y}
+def cod_at (r : α → α → Prop) (y : α) : Set α := {x | r x y}
+
+omit [RightEuclidean r] in
+theorem foo [Nonempty (cod r)] : RightEuclidean r ↔ IsEquiv (cod r) r ∧ (∀ x ∈ (cod r)ᶜ, ∃ y : cod r, cod_at r x ⊆ cod_at r y) := by
+  constructor
+  · intro _
+    constructor
+    · exact equiv_cod
+    · intro _ _
+      use Classical.arbitrary (cod r)
+      grind [cod_at]
+  · rintro ⟨equiv_cod, h⟩
+    constructor
+    intro x y z xy xz
+    by_cases codₓ : x ∈ cod r
+    · have := @equiv_cod.symm
+      have := @equiv_cod.trans
+      have : y ∈ cod r := by grind
+      have : z ∈ cod r := by grind
+
+    · sorry
+
 end RightEuclidean
 
 namespace LeftEuclidean
@@ -283,7 +306,7 @@ private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a b
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a c
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b c
-  have := antisymm_leftUnique (r := r) 
+  have := antisymm_leftUnique (r := r)
   have := @refl_dom (r := r)
   grind [Relator.LeftUnique]
 

From 24f1e8ae30eeb21364f21f80c4effcb129d12e36 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 19 May 2026 12:46:51 -0400
Subject: [PATCH 18/20] rm accidentally commited WIP

---
 Cslib/Foundations/Data/Relation.lean | 23 -----------------------
 1 file changed, 23 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index dc8ca9a5b..d723c08b6 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -227,29 +227,6 @@ theorem rightTotal_cod : Relator.RightTotal (α := cod r) (β := cod r) r :=
 
 theorem equiv_cod : IsEquiv (cod r) r := rightTotal_equiv rightTotal_cod
 
-def dom_at (r : α → α → Prop) (x : α) : Set α := {y | r x y}
-def cod_at (r : α → α → Prop) (y : α) : Set α := {x | r x y}
-
-omit [RightEuclidean r] in
-theorem foo [Nonempty (cod r)] : RightEuclidean r ↔ IsEquiv (cod r) r ∧ (∀ x ∈ (cod r)ᶜ, ∃ y : cod r, cod_at r x ⊆ cod_at r y) := by
-  constructor
-  · intro _
-    constructor
-    · exact equiv_cod
-    · intro _ _
-      use Classical.arbitrary (cod r)
-      grind [cod_at]
-  · rintro ⟨equiv_cod, h⟩
-    constructor
-    intro x y z xy xz
-    by_cases codₓ : x ∈ cod r
-    · have := @equiv_cod.symm
-      have := @equiv_cod.trans
-      have : y ∈ cod r := by grind
-      have : z ∈ cod r := by grind
-
-    · sorry
-
 end RightEuclidean
 
 namespace LeftEuclidean

From f6a8226e630facb58348e5973542bf89ff1331c7 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 20 May 2026 02:23:09 -0400
Subject: [PATCH 19/20] useless <|

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

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index d723c08b6..78c574db9 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -84,14 +84,14 @@ lemma cod_inv : cod (fun a b => r b a) = dom r := rfl
 lemma dom_inv : dom (fun a b => r b a) = cod r := rfl
 
 theorem _root_.Std.Trichotomous.subsingleton_cod [Std.Trichotomous r] :
-    Subsingleton <| ((cod r)ᶜ : Set α) := by
+    Subsingleton ((cod r)ᶜ : Set α) := by
   constructor
   rintro ⟨b₁, _⟩ ⟨b₂, _⟩
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b₁ b₂
   grind
 
 theorem _root_.Std.Trichotomous.subsingleton_dom [Std.Trichotomous r] :
-    Subsingleton <| ((dom r)ᶜ : Set α) := by
+    Subsingleton ((dom r)ᶜ : Set α) := by
   constructor
   rintro ⟨a₁, _⟩ ⟨a₂, _⟩
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a₁ a₂

From 70ff630d8a5d2d7cfcc6add08fe5ea12767db11d Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 20 May 2026 15:38:25 -0400
Subject: [PATCH 20/20] allow hetero for dom/cod

---
 Cslib/Foundations/Data/Relation.lean | 44 ++++++++++++++++++----------
 1 file changed, 28 insertions(+), 16 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 78c574db9..f719b4680 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -37,17 +37,25 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou
 
 namespace Relation
 
-/-- Domain of a relation. -/
-def dom (r : α → α → Prop) : Set α := {a | ∃ b, r a b}
+/-- The empty (heterogeneous) relation, which always returns `False`. -/
+@[nolint unusedArguments]
+def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False
 
-/-- Codomain of a relation, aka range. -/
-def cod (r : α → α → Prop) : Set α := {b | ∃ a, r a b}
+@[simp, grind =]
+theorem emptyHRelation_emptyRelation : (emptyHRelation : α → α → Prop) = emptyRelation := rfl
 
-instance : CoeDep (α → α → Prop) r (dom r → dom r → Prop) where
-  coe a b := r a b
+@[simp, grind =]
+theorem emptyHrelation_apply (a : α) (b : β) : emptyHRelation a b ↔ False := .rfl
 
-instance : CoeDep (α → α → Prop) r (cod r → cod r → Prop) where
-  coe a b := r a b
+section dom_cod
+
+variable {β : Type*} {r : α → β → Prop}
+
+/-- Domain of a relation. -/
+def dom (r : α → β → Prop) : Set α := {a | ∃ b, r a b}
+
+/-- Codomain of a relation, aka range. -/
+def cod (r : α → β → Prop) : Set β := {b | ∃ a, r a b}
 
 @[simp, grind =] lemma mem_dom : a ∈ dom r ↔ ∃ b, r a b := .rfl
 @[simp, grind =] lemma mem_cod : b ∈ cod r ↔ ∃ a, r a b := .rfl
@@ -56,13 +64,13 @@ instance : CoeDep (α → α → Prop) r (cod r → cod r → Prop) where
 @[gcongr] lemma cod_mono (h : r₁ ≤ r₂) : cod r₁ ⊆ cod r₂ := fun b ⟨a, hab⟩ => ⟨a, h a b hab⟩
 
 @[simp, grind =]
-lemma dom_empty : dom (emptyRelation : α → α → Prop) = ∅ := by grind [emptyRelation, dom]
+lemma dom_empty : dom (emptyHRelation : α → β → Prop) = ∅ := by grind
 
 @[simp, grind =]
-lemma cod_empty : cod (emptyRelation : α → α → Prop) = ∅ := by grind [emptyRelation, cod]
+lemma cod_empty : cod (emptyHRelation : α → β → Prop) = ∅ := by grind
 
 @[simp, grind =]
-lemma dom_eq_empty_iff : dom r = ∅ ↔ r = emptyRelation where
+lemma dom_eq_empty_iff : dom r = ∅ ↔ r = emptyHRelation where
   mp h := by
     ext a b
     simp
@@ -70,7 +78,7 @@ lemma dom_eq_empty_iff : dom r = ∅ ↔ r = emptyRelation where
   mpr := by grind
 
 @[simp, grind =]
-lemma cod_eq_empty_iff : cod r = ∅ ↔ r = emptyRelation where
+lemma cod_eq_empty_iff : cod r = ∅ ↔ r = emptyHRelation where
   mp h := by
     ext a b
     simp
@@ -83,6 +91,14 @@ lemma cod_inv : cod (fun a b => r b a) = dom r := rfl
 @[simp]
 lemma dom_inv : dom (fun a b => r b a) = cod r := rfl
 
+end dom_cod
+
+instance : CoeDep (α → α → Prop) r (dom r → dom r → Prop) where
+  coe a b := r a b
+
+instance : CoeDep (α → α → Prop) r (cod r → cod r → Prop) where
+  coe a b := r a b
+
 theorem _root_.Std.Trichotomous.subsingleton_cod [Std.Trichotomous r] :
     Subsingleton ((cod r)ᶜ : Set α) := by
   constructor
@@ -97,10 +113,6 @@ theorem _root_.Std.Trichotomous.subsingleton_dom [Std.Trichotomous r] :
   have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a₁ a₂
   grind
 
-/-- The empty (heterogeneous) relation, which always returns `False`. -/
-@[nolint unusedArguments]
-def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False
-
 attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen CompRel
 
 theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b := by