From 352e0bb8cc7d9bed61432982af56016a0c301689 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 26 Jun 2026 08:52:31 -0500
Subject: [PATCH] Fold Isomorphism module into Lattice.lean

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 lean/Spa.lean               |  1 -
 lean/Spa/Isomorphism.lean   | 16 ----------------
 lean/Spa/Lattice.lean       | 19 +++++++++++++++++++
 lean/Spa/Lattice/Tuple.lean |  1 -
 4 files changed, 19 insertions(+), 18 deletions(-)
 delete mode 100644 lean/Spa/Isomorphism.lean

diff --git a/lean/Spa.lean b/lean/Spa.lean
index b1a0048..3f4b823 100644
--- a/lean/Spa.lean
+++ b/lean/Spa.lean
@@ -1,6 +1,5 @@
 import Spa.Lattice
 import Spa.Fixedpoint
-import Spa.Isomorphism
 import Spa.Lattice.Unit
 import Spa.Lattice.Prod
 import Spa.Lattice.AboveBelow
diff --git a/lean/Spa/Isomorphism.lean b/lean/Spa/Isomorphism.lean
deleted file mode 100644
index dd5e0e6..0000000
--- a/lean/Spa/Isomorphism.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import Spa.Lattice
-
-namespace Spa
-
-def FiniteHeightLattice.transport {α β : Type*} [Lattice β]
-    [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
-    (hf : Monotone f) (hg : Monotone g)
-    (hgf : Function.LeftInverse g f) (hfg : Function.LeftInverse f g) :
-    FiniteHeightLattice β where
-  toLattice := inferInstance
-  longestChain :=
-    I.longestChain.map f (hf.strictMono_of_injective hgf.injective)
-  chains_bounded := fun c =>
-    I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
-
-end Spa
diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean
index 39e96d3..6448702 100644
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -107,6 +107,25 @@ lemma le_top (a : α) : a ≤ (⊤ : α) := by
     rw [RelSeries.snoc_length] at hbound
     omega
 
+/-- This is something like a lemma about isomorphic types having the same height.
+    Given a finite-height lattice `α`, lattice `β`, and a `Monotone` bijection
+    between the two, we can show that lattice `β` also has a finite height.
+
+    The proof is fairly trivial: the longest chain in `α` can be transported
+    to be a longest chain in `β` (by monotonicity), establishing a height witness.
+    At the same time, any chain in `β` can be transported to a chain in `α`,
+    and must be bounded by the same height by `FiniteHeightLattice.chains_bounded`. -/
+def transport {α β : Type*} [Lattice β]
+    [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
+    (hf : Monotone f) (hg : Monotone g)
+    (hgf : Function.LeftInverse g f) (hfg : Function.LeftInverse f g) :
+    FiniteHeightLattice β where
+  toLattice := inferInstance
+  longestChain :=
+    I.longestChain.map f (hf.strictMono_of_injective hgf.injective)
+  chains_bounded := fun c =>
+    I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
+
 end FiniteHeightLattice
 
 end Spa
diff --git a/lean/Spa/Lattice/Tuple.lean b/lean/Spa/Lattice/Tuple.lean
index ec2b3f6..c9a61e4 100644
--- a/lean/Spa/Lattice/Tuple.lean
+++ b/lean/Spa/Lattice/Tuple.lean
@@ -1,5 +1,4 @@
 import Spa.Lattice.IterProd
-import Spa.Isomorphism
 
 namespace Spa