From 4d6f26fa4550601fb5504f01587c6afeb1d1722a Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 15 Jun 2026 06:29:29 -0400
Subject: [PATCH 1/6] feat(Logic/Relation): some EqvGen API

---
 Mathlib/Logic/Relation.lean | 73 ++++++++++++++++++++++++++++++-------
 1 file changed, 59 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index 8607a7d2f4a46c..a8bc8d2403aede 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -361,6 +361,10 @@ theorem to_reflTransGen : ∀ {a b}, ReflGen r a b → ReflTransGen r a b
   | a, _, refl => by rfl
   | _, _, single h => ReflTransGen.tail ReflTransGen.refl h
 
+theorem to_eqvGen : ∀ {a b}, ReflGen r a b → EqvGen r a b
+  | a, _, refl => EqvGen.refl a
+  | _, _, single h => EqvGen.rel _ _ h
+
 theorem mono {p : α → α → Prop} (hp : ∀ a b, r a b → p a b) : ∀ {a b}, ReflGen r a b → ReflGen p a b
   | a, _, ReflGen.refl => by rfl
   | a, b, single h => single (hp a b h)
@@ -387,6 +391,11 @@ end ReflGen
 
 namespace SymmGen
 
+theorem to_eqvGen {a b} (h : SymmGen r a b) : EqvGen r a b := by
+  cases h with
+  | inl hab => exact .rel a b hab
+  | inr hba => exact .symm _ _ (.rel b a hba)
+
 theorem of_rel (h : r a b) : SymmGen r a b :=
   Or.inl h
 
@@ -427,6 +436,11 @@ end SymmGen
 
 namespace ReflTransGen
 
+theorem to_eqvGen {a b} (h : ReflTransGen r a b) : EqvGen r a b := by
+  induction h with
+  | refl => exact EqvGen.refl a
+  | tail _ bc ab => grind [eqvGen_iff]
+
 @[trans]
 theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by
   induction hbc with
@@ -504,6 +518,11 @@ theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b := by
   | single h => exact ReflTransGen.single h
   | tail _ bc ab => exact ReflTransGen.tail ab bc
 
+theorem to_eqvGen {a b} (h : TransGen r a b) : EqvGen r a b := by
+  induction h with
+  | single h => exact EqvGen.rel _ _ h
+  | tail _ bc ab => grind [eqvGen_iff]
+
 theorem trans_left (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c := by
   induction hbc with
   | refl => assumption
@@ -802,6 +821,46 @@ theorem mono {r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : Eq
   | symm a b _ ih => exact EqvGen.symm _ _ ih
   | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
 
+variable {r}
+
+theorem _root_.Equivalence.eqvGen_iff (h : Equivalence r) : EqvGen r a b ↔ r a b :=
+  Iff.intro
+    (by
+      intro h
+      induction h with
+      | rel => assumption
+      | refl => exact h.1 _
+      | symm => apply h.symm; assumption
+      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc)
+    (EqvGen.rel a b)
+
+theorem _root_.Equivalence.eqvGen_eq (h : Equivalence r) : EqvGen r = r :=
+  funext fun _ ↦ funext fun _ ↦ propext <| h.eqvGen_iff
+
+theorem _root_.Relation.eqvGen_idem : EqvGen (EqvGen r) = EqvGen r :=
+  Equivalence.eqvGen_eq (EqvGen.is_equivalence r)
+
+theorem lift {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b))
+    (hab : EqvGen r a b) : EqvGen p (f a) (f b) := by
+  induction hab with
+  | rel a b ab => exact rel (f a) (f b) (h a b ab)
+  | refl a => exact refl (f a)
+  | symm a b ab ih => exact symm (f a) (f b) ih
+  | trans a b c ab bc ih₁ ih₂ => exact trans (f a) (f b) (f c) ih₁ ih₂
+
+theorem lift' {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → EqvGen p (f a) (f b))
+    (hab : EqvGen r a b) : EqvGen p (f a) (f b) := by
+  simpa [eqvGen_idem] using hab.lift f h
+
+theorem _root_.Relation.reflTransGen_eqvGen_eq [Std.Symm r] : ReflTransGen r = EqvGen r := by
+  ext a b
+  refine ⟨ReflTransGen.to_eqvGen, fun hab => ?_⟩
+  induction hab with
+  | rel a b ab => exact .single ab
+  | refl a => exact .refl
+  | symm a b ab ih => grind [Std.Symm.swap_eq, reflTransGen_swap]
+  | trans a b c ab bc ih₁ ih₂ => exact .trans ih₁ ih₂
+
 end EqvGen
 
 /-- The join of a relation on a single type is a new relation for which
@@ -911,18 +970,4 @@ theorem Quot.eqvGen_sound (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b :=
     (fun _ _ _ _ _ IH₁ IH₂ ↦ Eq.trans IH₁ IH₂)
     H
 
-theorem Equivalence.eqvGen_iff (h : Equivalence r) : EqvGen r a b ↔ r a b :=
-  Iff.intro
-    (by
-      intro h
-      induction h with
-      | rel => assumption
-      | refl => exact h.1 _
-      | symm => apply h.symm; assumption
-      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc)
-    (EqvGen.rel a b)
-
-theorem Equivalence.eqvGen_eq (h : Equivalence r) : EqvGen r = r :=
-  funext fun _ ↦ funext fun _ ↦ propext <| h.eqvGen_iff
-
 end EqvGen

From 11dfcac9bb858f70a5e2a15e4618556ca7534feb Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 15 Jun 2026 06:38:16 -0400
Subject: [PATCH 2/6] consistent dot notation usage

---
 Mathlib/Logic/Relation.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index a8bc8d2403aede..d856af8e92e3e2 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -362,8 +362,8 @@ theorem to_reflTransGen : ∀ {a b}, ReflGen r a b → ReflTransGen r a b
   | _, _, single h => ReflTransGen.tail ReflTransGen.refl h
 
 theorem to_eqvGen : ∀ {a b}, ReflGen r a b → EqvGen r a b
-  | a, _, refl => EqvGen.refl a
-  | _, _, single h => EqvGen.rel _ _ h
+  | a, _, refl => .refl a
+  | _, _, single h => .rel _ _ h
 
 theorem mono {p : α → α → Prop} (hp : ∀ a b, r a b → p a b) : ∀ {a b}, ReflGen r a b → ReflGen p a b
   | a, _, ReflGen.refl => by rfl
@@ -438,7 +438,7 @@ namespace ReflTransGen
 
 theorem to_eqvGen {a b} (h : ReflTransGen r a b) : EqvGen r a b := by
   induction h with
-  | refl => exact EqvGen.refl a
+  | refl => exact .refl a
   | tail _ bc ab => grind [eqvGen_iff]
 
 @[trans]
@@ -520,7 +520,7 @@ theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b := by
 
 theorem to_eqvGen {a b} (h : TransGen r a b) : EqvGen r a b := by
   induction h with
-  | single h => exact EqvGen.rel _ _ h
+  | single h => exact .rel _ _ h
   | tail _ bc ab => grind [eqvGen_iff]
 
 theorem trans_left (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c := by

From 91ecacdb73332193c7373e549846db164a6ca9e7 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 15 Jun 2026 11:51:41 -0400
Subject: [PATCH 3/6] nicer proofs using trans_induction_on

---
 Mathlib/Logic/Relation.lean | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index d856af8e92e3e2..0798389a284afc 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -436,11 +436,6 @@ end SymmGen
 
 namespace ReflTransGen
 
-theorem to_eqvGen {a b} (h : ReflTransGen r a b) : EqvGen r a b := by
-  induction h with
-  | refl => exact .refl a
-  | tail _ bc ab => grind [eqvGen_iff]
-
 @[trans]
 theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by
   induction hbc with
@@ -509,6 +504,12 @@ theorem total_of_right_unique (U : Relator.RightUnique r) (ab : ReflTransGen r a
         exact Or.inl ec
     · exact Or.inr (IH.tail bd)
 
+theorem to_eqvGen {a b} (h : ReflTransGen r a b) : EqvGen r a b := by
+  induction h using trans_induction_on with
+  | refl a => exact .refl a
+  | single hab => exact .rel _ _ hab
+  | trans _ _ hab hbc => exact .trans _ _ _ hab hbc
+
 end ReflTransGen
 
 namespace TransGen
@@ -518,11 +519,6 @@ theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b := by
   | single h => exact ReflTransGen.single h
   | tail _ bc ab => exact ReflTransGen.tail ab bc
 
-theorem to_eqvGen {a b} (h : TransGen r a b) : EqvGen r a b := by
-  induction h with
-  | single h => exact .rel _ _ h
-  | tail _ bc ab => grind [eqvGen_iff]
-
 theorem trans_left (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c := by
   induction hbc with
   | refl => assumption
@@ -563,6 +559,11 @@ theorem trans_induction_on {motive : ∀ {a b : α}, TransGen r a b → Prop} {a
   | single h => exact single h
   | tail hab hbc h_ih => exact trans hab (.single hbc) h_ih (single hbc)
 
+theorem to_eqvGen {a b} (h : TransGen r a b) : EqvGen r a b := by
+  induction h using trans_induction_on with
+  | single h => exact .rel _ _ h
+  | trans _ _ hab hbc => exact .trans _ _ _ hab hbc
+
 theorem trans_right (hab : ReflTransGen r a b) (hbc : TransGen r b c) : TransGen r a c := by
   induction hbc with
   | single hbc => exact tail' hab hbc

From 3ea131a71f903998292a5169210b32bfe5fb2ea4 Mon Sep 17 00:00:00 2001
From: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Date: Tue, 16 Jun 2026 16:33:26 -0400
Subject: [PATCH 4/6] Naming

---
 Mathlib/Logic/Relation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index 0798389a284afc..4f1900b7270e46 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -853,7 +853,7 @@ theorem lift' {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b,
     (hab : EqvGen r a b) : EqvGen p (f a) (f b) := by
   simpa [eqvGen_idem] using hab.lift f h
 
-theorem _root_.Relation.reflTransGen_eqvGen_eq [Std.Symm r] : ReflTransGen r = EqvGen r := by
+theorem _root_.Relation.reflTransGen_eq_eqvGen [Std.Symm r] : ReflTransGen r = EqvGen r := by
   ext a b
   refine ⟨ReflTransGen.to_eqvGen, fun hab => ?_⟩
   induction hab with

From 0816791d9473fafc1129fad2698599acaea494be Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 3 Jul 2026 22:55:51 +0100
Subject: [PATCH 5/6] consistent statements with 30526

---
 Mathlib/Logic/Relation.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index 612818e0478335..d5bb778f65c727 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -851,16 +851,18 @@ theorem _root_.Equivalence.eqvGen_eq (h : Equivalence r) : EqvGen r = r :=
 theorem _root_.Relation.eqvGen_idem : EqvGen (EqvGen r) = EqvGen r :=
   Equivalence.eqvGen_eq (EqvGen.is_equivalence r)
 
-theorem lift {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b))
-    (hab : EqvGen r a b) : EqvGen p (f a) (f b) := by
+theorem lift {p : β → β → Prop} (f : α → β) (h : r ≤ (p on f)) :
+    EqvGen r ≤ (EqvGen p on f) := by
+  intro _ _ hab
   induction hab with
   | rel a b ab => exact rel (f a) (f b) (h a b ab)
   | refl a => exact refl (f a)
   | symm a b ab ih => exact symm (f a) (f b) ih
   | trans a b c ab bc ih₁ ih₂ => exact trans (f a) (f b) (f c) ih₁ ih₂
 
-theorem lift' {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → EqvGen p (f a) (f b))
-    (hab : EqvGen r a b) : EqvGen p (f a) (f b) := by
+theorem lift' {p : β → β → Prop} (f : α → β) (h : r ≤ (EqvGen p on f)) :
+    EqvGen r ≤ (EqvGen p on f) := by
+  intro _ _ hab
   simpa [eqvGen_idem] using hab.lift f h
 
 theorem _root_.Relation.reflTransGen_eq_eqvGen [Std.Symm r] : ReflTransGen r = EqvGen r := by

From 092676e0b1393b449fefc51ea7effb2e0951354d Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 4 Jul 2026 17:04:27 +0100
Subject: [PATCH 6/6] more consistency with 30526

---
 Mathlib/Logic/Relation.lean | 31 +++++++++++++++++++++++--------
 1 file changed, 23 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index d5bb778f65c727..df65269a3326ad 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -361,14 +361,17 @@ theorem reflGen_le_reflTransGen : ReflGen r ≤ ReflTransGen r
   | a, _, .refl => by rfl
   | _, _, .single h => ReflTransGen.tail ReflTransGen.refl h
 
+theorem reflGen_le_eqvGen : ReflGen r ≤ EqvGen r
+  | a, _, .refl => .refl a
+  | _, _, .single h => .rel _ _ h
+
 namespace ReflGen
 
 theorem to_reflTransGen {a b} : ReflGen r a b → ReflTransGen r a b :=
   reflGen_le_reflTransGen a b
 
-theorem to_eqvGen : ∀ {a b}, ReflGen r a b → EqvGen r a b
-  | a, _, refl => .refl a
-  | _, _, single h => .rel _ _ h
+theorem to_eqvGen {a b} : ReflGen r a b → EqvGen r a b :=
+  reflGen_le_eqvGen a b
 
 theorem mono {p : α → α → Prop} (hp : r ≤ p) : ReflGen r ≤ ReflGen p
   | a, _, ReflGen.refl => by rfl
@@ -394,13 +397,17 @@ instance [IsTrans α r] : IsTrans α (ReflGen r) where
 
 end ReflGen
 
-namespace SymmGen
-
-theorem to_eqvGen {a b} (h : SymmGen r a b) : EqvGen r a b := by
+theorem symmGen_le_eqvGen : SymmGen r ≤ EqvGen r := by
+  intro a b h
   cases h with
   | inl hab => exact .rel a b hab
   | inr hba => exact .symm _ _ (.rel b a hba)
 
+namespace SymmGen
+
+theorem to_eqvGen {a b} : SymmGen r a b → EqvGen r a b :=
+  symmGen_le_eqvGen a b
+
 theorem of_rel (h : r a b) : SymmGen r a b :=
   Or.inl h
 
@@ -512,12 +519,16 @@ theorem total_of_right_unique (U : Relator.RightUnique r) (ab : ReflTransGen r a
         exact Or.inl ec
     · exact Or.inr (IH.tail bd)
 
-theorem to_eqvGen {a b} (h : ReflTransGen r a b) : EqvGen r a b := by
+theorem _root_.Relation.reflTransGen_le_eqvGen : ReflTransGen r ≤ EqvGen r := by
+  intro _ _ h
   induction h using trans_induction_on with
   | refl a => exact .refl a
   | single hab => exact .rel _ _ hab
   | trans _ _ hab hbc => exact .trans _ _ _ hab hbc
 
+theorem to_eqvGen {a b} : ReflTransGen r a b → EqvGen r a b :=
+  reflTransGen_le_eqvGen a b
+
 end ReflTransGen
 
 theorem transGen_le_reflTransGen : TransGen r ≤ ReflTransGen r := by
@@ -571,11 +582,15 @@ theorem trans_induction_on {motive : ∀ {a b : α}, TransGen r a b → Prop} {a
   | single h => exact single h
   | tail hab hbc h_ih => exact trans hab (.single hbc) h_ih (single hbc)
 
-theorem to_eqvGen {a b} (h : TransGen r a b) : EqvGen r a b := by
+theorem _root_.Relation.transGen_le_eqvGen : TransGen r ≤ EqvGen r := by
+  intro _ _ h
   induction h using trans_induction_on with
   | single h => exact .rel _ _ h
   | trans _ _ hab hbc => exact .trans _ _ _ hab hbc
 
+theorem to_eqvGen {a b} : TransGen r a b → EqvGen r a b :=
+  transGen_le_eqvGen a b
+
 theorem trans_right (hab : ReflTransGen r a b) (hbc : TransGen r b c) : TransGen r a c := by
   induction hbc with
   | single hbc => exact tail' hab hbc