diff --git a/lean/Spa/Fixedpoint.lean b/lean/Spa/Fixedpoint.lean
index 6666277..8bc466c 100644
--- a/lean/Spa/Fixedpoint.lean
+++ b/lean/Spa/Fixedpoint.lean
@@ -24,8 +24,7 @@ def doStep (f : α → α) (hf : Monotone f) :
 def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
   doStep f hf (height (α := α) + 1) (RelSeries.singleton _ ⊥)
     (by simp)
-    (by simpa [RelSeries.last_singleton]
-          using FiniteHeightLattice.bot_le α (f ⊥))
+    (by simp)
 
 def aFix (f : α → α) (hf : Monotone f) : α :=
   (fix f hf).1
@@ -50,7 +49,7 @@ lemma doStep_le (f : α → α) (hf : Monotone f)
 
 theorem aFix_le (f : α → α) (hf : Monotone f)
     {a : α} (ha : a = f a) : aFix f hf ≤ a :=
-  doStep_le f hf ha _ _ _ _ (by simpa using FiniteHeightLattice.bot_le α a)
+  doStep_le f hf ha _ _ _ _ (by simp)
 
 end Fixedpoint
 
diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean
index 8ccf56f..a906d01 100644
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -76,7 +76,7 @@ lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
   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
+class FiniteHeightLattice (α : Type*) extends Lattice α, OrderBot α, OrderTop α where
   longestChain : LTSeries α
   chains_bounded : BoundedChains α longestChain.length
 
@@ -90,30 +90,19 @@ def height (α : Type*) [FiniteHeightLattice α] : ℕ :=
 
 variable (α : Type*) [FiniteHeightLattice α]
 
-instance (priority := 100) : Bot α := ⟨(longestChain (α := α)).head⟩
-instance (priority := 100) : Top α := ⟨(longestChain (α := α)).last⟩
+/-- Any maximum-length chain in a bounded finite-height lattice starts at `⊥`. -/
+lemma longestChain_head : (longestChain (α := α)).head = ⊥ := by
+  by_contra hne
+  have hbound := chains_bounded ((longestChain (α := α)).cons ⊥ (bot_lt_iff_ne_bot.mpr hne))
+  rw [RelSeries.cons_length] at hbound
+  omega
 
-/-- The bottom element `⊥` of a finite height lattice is _actually_ the least element. -/
-lemma bot_le (a : α) : (⊥ : α) ≤ a := by
-  by_cases heq : ⊥ ⊓ a = ⊥
-  · exact inf_eq_left.mp heq
-  · exfalso
-    have hlt : ⊥ ⊓ a < (longestChain (α := α)).head :=
-      lt_of_le_of_ne inf_le_left heq
-    have hbound := chains_bounded ((longestChain (α := α)).cons (⊥ ⊓ a) hlt)
-    rw [RelSeries.cons_length] at hbound
-    omega
-
-/-- The top element `⊤` of a finite height lattice is _actually_ the greatest element. -/
-lemma le_top (a : α) : a ≤ (⊤ : α) := by
-  by_cases heq : a ⊔ ⊤ = ⊤
-  · exact sup_eq_right.mp heq
-  · exfalso
-    have hlt : (longestChain (α := α)).last < a ⊔ ⊤ :=
-      lt_of_le_of_ne le_sup_right (Ne.symm heq)
-    have hbound := chains_bounded ((longestChain (α := α)).snoc (a ⊔ ⊤) hlt)
-    rw [RelSeries.snoc_length] at hbound
-    omega
+/-- Any maximum-length chain in a bounded finite-height lattice ends at `⊤`. -/
+lemma longestChain_last : (longestChain (α := α)).last = ⊤ := by
+  by_contra hne
+  have hbound := chains_bounded ((longestChain (α := α)).snoc ⊤ (lt_top_iff_ne_top.mpr hne))
+  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
@@ -129,6 +118,16 @@ def transport {α β : Type*} [Lattice β]
     (hgf : Function.LeftInverse g f) (hfg : Function.LeftInverse f g) :
     FiniteHeightLattice β where
   toLattice := inferInstance
+  toOrderBot := {
+    bot := f (⊥ : α)
+    bot_le := fun b => by
+      rw [← hfg b]
+      exact hf (_root_.bot_le : (⊥ : α) ≤ g b) }
+  toOrderTop := {
+    top := f (⊤ : α)
+    le_top := fun b => by
+      rw [← hfg b]
+      exact hf (_root_.le_top : g b ≤ (⊤ : α)) }
   longestChain :=
     I.longestChain.map f (hf.strictMono_of_injective hgf.injective)
   chains_bounded := fun c =>
@@ -136,8 +135,15 @@ def transport {α β : Type*} [Lattice β]
 
 /-- 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
+def ofUnique (α : Type*) [Lattice α] [Unique α] :
+    FiniteHeightLattice α where
   toLattice := inferInstance
+  toOrderBot := {
+    bot := default
+    bot_le := fun _ => le_of_eq (Subsingleton.elim _ _) }
+  toOrderTop := {
+    top := default
+    le_top := fun _ => le_of_eq (Subsingleton.elim _ _) }
   longestChain := RelSeries.singleton _ default
   chains_bounded := boundedChains_of_subsingleton α 0
 
diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean
index d25b777..558d6c7 100644
--- a/lean/Spa/Lattice/AboveBelow.lean
+++ b/lean/Spa/Lattice/AboveBelow.lean
@@ -93,6 +93,14 @@ lemma bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
 lemma le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
   le_iff.mpr (sup_top a)
 
+instance : OrderBot (AboveBelow α) where
+  bot := bot
+  bot_le := bot_le'
+
+instance : OrderTop (AboveBelow α) where
+  top := top
+  le_top := le_top'
+
 lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
   lt_of_le_of_ne (bot_le' _) (by simp)
 
@@ -224,6 +232,8 @@ lemma boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
 
 instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
   toLattice := inferInstance
+  toOrderBot := inferInstance
+  toOrderTop := inferInstance
   longestChain :=
     ((RelSeries.singleton _ bot).snoc (mk default)
         (by rw [RelSeries.last_singleton]; exact bot_lt_mk default)).snoc top
diff --git a/lean/Spa/Lattice/Bool.lean b/lean/Spa/Lattice/Bool.lean
index 390a0c8..4e8a9b2 100644
--- a/lean/Spa/Lattice/Bool.lean
+++ b/lean/Spa/Lattice/Bool.lean
@@ -29,6 +29,8 @@ lemma boundedChains : BoundedChains Bool 1 := fun c => by
 
 instance : FiniteHeightLattice Bool where
   toLattice := inferInstance
+  toOrderBot := inferInstance
+  toOrderTop := inferInstance
   longestChain := (RelSeries.singleton _ (⊥ : Bool)).snoc (⊤ : Bool)
     (by rw [RelSeries.last_singleton]; exact bot_lt_top)
   chains_bounded := boundedChains
diff --git a/lean/Spa/Lattice/Tuple.lean b/lean/Spa/Lattice/Tuple.lean
index 846eb9e..94ec152 100644
--- a/lean/Spa/Lattice/Tuple.lean
+++ b/lean/Spa/Lattice/Tuple.lean
@@ -141,10 +141,12 @@ private def stdChain : (n : ℕ) →
           ((FiniteHeightLattice.longestChain (α := β)).map
             (fun b => (Fin.cons b (⊥ : Fin n → β) : Fin (n + 1) → β)) consBot_strictMono)
           (prev.1.map (fun f => (Fin.cons (⊤ : β) f : Fin (n + 1) → β)) consTop_strictMono)
-          (by rw [LTSeries.last_map, LTSeries.head_map, prev.2.1]; rfl),
+          (by
+            rw [LTSeries.last_map, LTSeries.head_map,
+              FiniteHeightLattice.longestChain_last, prev.2.1]),
         by
           simp only [RelSeries.head_smash, LTSeries.head_map]
-          rw [show (FiniteHeightLattice.longestChain (α := β)).head = (⊥ : β) from rfl]
+          rw [FiniteHeightLattice.longestChain_head]
           funext i
           refine Fin.cases ?_ (fun j => ?_) i <;> simp [Pi.bot_apply],
         by
@@ -154,6 +156,8 @@ private def stdChain : (n : ℕ) →
 
 instance instFiniteHeight {n : ℕ} : FiniteHeightLattice (Fin n → β) where
   toLattice := inferInstance
+  toOrderBot := inferInstance
+  toOrderTop := inferInstance
   longestChain := (stdChain n).1
   chains_bounded := fun c => by
     obtain ⟨cs, _, _, hbound⟩ := exists_unzip c