From 1a843747bf6eaa770922858b1ffaabe99aac66ee Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 26 Jun 2026 10:17:25 -0500
Subject: [PATCH] Delete unused code and moved some lemmas into Lattice.lean

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 lean/Spa/Lattice.lean          | 15 +++++++++++++++
 lean/Spa/Lattice/IterProd.lean |  9 ---------
 lean/Spa/Lattice/Unit.lean     | 13 +------------
 3 files changed, 16 insertions(+), 21 deletions(-)

diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean
index 6448702..8ccf56f 100644
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -67,6 +67,14 @@ end Folds
 def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
   ∀ c : LTSeries α, c.length ≤ n
 
+/-- Since a singleton type's preorder has no nonempty `<` chains,
+    they are vacuously bounded by any minimum height. -/
+lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
+    (n : ℕ) : BoundedChains α n := fun c => by
+  by_contra hc
+  push_neg at hc
+  exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)
+
 /-- A finite height lattice is a lattice in which all chains $a < \ldots < z$ have a maximum height `height`. -/
 class FiniteHeightLattice (α : Type*) extends Lattice α where
   longestChain : LTSeries α
@@ -126,6 +134,13 @@ def transport {α β : Type*} [Lattice β]
   chains_bounded := fun c =>
     I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
 
+/-- A `Unique` lattice trivially has finite height: its only chain is the singleton
+    `[default]`, and there are no nontrivial `<` chains in a subsingleton. -/
+def ofUnique (α : Type*) [Lattice α] [Unique α] : FiniteHeightLattice α where
+  toLattice := inferInstance
+  longestChain := RelSeries.singleton _ default
+  chains_bounded := boundedChains_of_subsingleton α 0
+
 end FiniteHeightLattice
 
 end Spa
diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean
index 27d7752..6ebe692 100644
--- a/lean/Spa/Lattice/IterProd.lean
+++ b/lean/Spa/Lattice/IterProd.lean
@@ -13,15 +13,6 @@ namespace IterProd
 
 variable {A B : Type u}
 
-instance decidableEq [DecidableEq A] [DecidableEq B] :
-    ∀ k, DecidableEq (IterProd A B k)
-  | 0 => inferInstanceAs (DecidableEq B)
-  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (decidableEq k)
-
-def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
-  | 0 => b
-  | k + 1 => (a, build a b k)
-
 def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
     ∀ k, FiniteHeightLattice (IterProd A B k)
   | 0 => inferInstanceAs (FiniteHeightLattice B)
diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean
index 2e20475..60d2ac1 100644
--- a/lean/Spa/Lattice/Unit.lean
+++ b/lean/Spa/Lattice/Unit.lean
@@ -11,17 +11,6 @@ as a base case for the iterated product `Spa/Lattice/IterProd.lean`). -/
 
 namespace Spa
 
-/-- Since a singleton type's preorder has no nonempty `<` chains,
-    they are vacuously bounded by any minimum height. -/
-lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
-    (n : ℕ) : BoundedChains α n := fun c => by
-  by_contra hc
-  push_neg at hc
-  exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)
-
-instance : FiniteHeightLattice PUnit where
-  toLattice := inferInstance
-  longestChain := RelSeries.singleton _ PUnit.unit
-  chains_bounded := boundedChains_of_subsingleton PUnit 0
+instance : FiniteHeightLattice PUnit := FiniteHeightLattice.ofUnique PUnit
 
 end Spa