diff --git a/lean/Spa/Analysis/Forward/Lattices.lean b/lean/Spa/Analysis/Forward/Lattices.lean
index 3dae6c1..4b1180c 100644
--- a/lean/Spa/Analysis/Forward/Lattices.lean
+++ b/lean/Spa/Analysis/Forward/Lattices.lean
@@ -42,7 +42,7 @@ abbrev StateVariables : Type := FiniteMap prog.State (VariableValues L prog) pro
 
 /-- Agda: `⊥ᵛ` (the bottom of `fixedHeightᵛ`, now found by instance search). -/
 def botV [FiniteHeightLattice L] : VariableValues L prog :=
-  FiniteHeightLattice.bot (VariableValues L prog)
+  (⊥ : VariableValues L prog)
 
 variable {L prog}
 
diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean
index 53e92e6..10cc95f 100644
--- a/lean/Spa/Analysis/Sign.lean
+++ b/lean/Spa/Analysis/Sign.lean
@@ -1,30 +1,3 @@
-/-
-Port of `Analysis/Sign.agda`.
-
-Correspondence:
-  Sign (+ / - / 0ˢ)         ↦ Sign.plus / Sign.minus / Sign.zero
-  _≟ᵍ_, ≡-equiv, ≡-Decidable ↦ deriving DecidableEq
-  SignLattice (AboveBelow)  ↦ SignLattice
-  AB.Plain 0ˢ               ↦ the AboveBelow FiniteHeightLattice instance,
-                              seeded by `Inhabited Sign := ⟨.zero⟩`
-  plus, minus               ↦ plus, minus
-  plus-Monoˡ/ʳ, minus-Monoˡ/ʳ (postulates in Agda!)
-                            ↦ plus_mono_left/right, minus_mono_left/right —
-                              now actually proved, via
-                              AboveBelow.monotone₂_of_strict
-  plus-Mono₂, minus-Mono₂   ↦ plus_mono₂, minus_mono₂
-  ⟦_⟧ᵍ                      ↦ interpSign
-  ⟦⟧ᵍ-respects-≈ᵍ           ↦ (trivial with `=`)
-  ⟦⟧ᵍ-⊔ᵍ-∨, ⟦⟧ᵍ-⊓ᵍ-∧        ↦ interpSign_sup, interpSign_inf
-  s₁≢s₂⇒¬s₁∧s₂              ↦ interpSign_mk_disjoint
-  latticeInterpretationᵍ    ↦ signInterpretation
-  WithProg.eval, eval-Monoʳ ↦ SignAnalysis.eval, eval_mono
-  SignEval (instance)       ↦ SignAnalysis.exprEvaluator
-  plus-valid, minus-valid   ↦ plus_valid, minus_valid
-  eval-valid, SignEvalValid ↦ eval_valid
-  output                    ↦ SignAnalysis.output
-  analyze-correct           ↦ SignAnalysis.analyze_correct
--/
 import Spa.Analysis.Forward
 import Spa.Analysis.Utils
 import Spa.Showable
@@ -43,14 +16,11 @@ instance : Showable Sign :=
     | .minus => "-"
     | .zero => "0"⟩
 
-/-- Agda: the module parameter `x = 0ˢ` of `AB.Plain` (it seeds the
-`FiniteHeightLattice (AboveBelow Sign)` instance). -/
 instance : Inhabited Sign := ⟨.zero⟩
 
 abbrev SignLattice : Type := AboveBelow Sign
 
 open AboveBelow in
-/-- Agda: `plus`. -/
 def plus : SignLattice → SignLattice → SignLattice
   | bot, _ => bot
   | _, bot => bot
@@ -67,7 +37,6 @@ def plus : SignLattice → SignLattice → SignLattice
   | mk .zero, mk .zero => mk .zero
 
 open AboveBelow in
-/-- Agda: `minus`. -/
 def minus : SignLattice → SignLattice → SignLattice
   | bot, _ => bot
   | _, bot => bot
@@ -83,9 +52,6 @@ def minus : SignLattice → SignLattice → SignLattice
   | mk .zero, mk .minus => mk .plus
   | mk .zero, mk .zero => mk .zero
 
-/-- Agda: `plus-Mono₂` (its components were postulates in Agda; `plus` is a
-strict operation on the flat lattice, so monotonicity holds regardless of the
-sign table). -/
 theorem plus_mono₂ : Monotone₂ plus :=
   AboveBelow.monotone₂_of_strict plus
     (fun y => by cases y <;> rfl)
@@ -95,13 +61,10 @@ theorem plus_mono₂ : Monotone₂ plus :=
       rcases x with _ | _ | s <;>
         first | exact absurd rfl hx | rfl | (cases s <;> rfl))
 
-/-- Agda: `plus-Monoˡ` — a postulate there, a theorem here. -/
 theorem plus_mono_left (s₂ : SignLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂
 
-/-- Agda: `plus-Monoʳ` — a postulate there, a theorem here. -/
 theorem plus_mono_right (s₁ : SignLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁
 
-/-- Agda: `minus-Mono₂` (likewise from strictness of `minus`). -/
 theorem minus_mono₂ : Monotone₂ minus :=
   AboveBelow.monotone₂_of_strict minus
     (fun y => by cases y <;> rfl)
@@ -111,13 +74,10 @@ theorem minus_mono₂ : Monotone₂ minus :=
       rcases x with _ | _ | s <;>
         first | exact absurd rfl hx | rfl | (cases s <;> rfl))
 
-/-- Agda: `minus-Monoˡ` — a postulate there, a theorem here. -/
 theorem minus_mono_left (s₂ : SignLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂
 
-/-- Agda: `minus-Monoʳ` — a postulate there, a theorem here. -/
 theorem minus_mono_right (s₁ : SignLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁
 
-/-- Agda: `⟦_⟧ᵍ`. -/
 def interpSign : SignLattice → Value → Prop
   | .bot, _ => False
   | .top, _ => True
@@ -125,7 +85,6 @@ def interpSign : SignLattice → Value → Prop
   | .mk .zero, v => v = .int 0
   | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1))
 
-/-- Agda: `s₁≢s₂⇒¬s₁∧s₂`. -/
 theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
     ¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by
   rintro ⟨h₁, h₂⟩
@@ -154,17 +113,14 @@ theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Val
     injection hv with hz
     omega
 
-/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨` (via the factored flat-lattice lemma). -/
 theorem interpSign_sup {s₁ s₂ : SignLattice} (v : Value)
     (h : interpSign s₁ v ∨ interpSign s₂ v) : interpSign (s₁ ⊔ s₂) v :=
   AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
 
-/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧` (via the factored flat-lattice lemma). -/
 theorem interpSign_inf {s₁ s₂ : SignLattice} (v : Value)
     (h : interpSign s₁ v ∧ interpSign s₂ v) : interpSign (s₁ ⊓ s₂) v :=
   AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h
 
-/-- Agda: `latticeInterpretationᵍ` (an instance there too). -/
 instance signInterpretation : LatticeInterpretation SignLattice where
   interp := interpSign
   interp_sup := fun {l₁ l₂} v h => interpSign_sup (s₁ := l₁) (s₂ := l₂) v h
@@ -172,11 +128,8 @@ instance signInterpretation : LatticeInterpretation SignLattice where
 
 namespace SignAnalysis
 
-/-! Agda: `module WithProg (prog : Program)`. -/
-
 variable (prog : Program)
 
-/-- Agda: `WithProg.eval`. -/
 def eval : Expr → VariableValues SignLattice prog → SignLattice
   | .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs)
   | .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs)
@@ -185,7 +138,6 @@ def eval : Expr → VariableValues SignLattice prog → SignLattice
   | .num 0, _ => .mk .zero
   | .num (_ + 1), _ => .mk .plus
 
-/-- Agda: `WithProg.eval-Monoʳ`. -/
 theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
   induction e with
   | add e₁ e₂ ih₁ ih₂ =>
@@ -208,15 +160,12 @@ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
     intro vs₁ vs₂ _
     cases n <;> exact le_refl _
 
-/-- Agda: the `SignEval` instance. -/
 instance exprEvaluator : ExprEvaluator SignLattice prog :=
   ⟨eval prog, eval_mono prog⟩
 
-/-- Agda: `WithProg.result`/`output` — the analysis result, printed. -/
 def output : String :=
   show' (result SignLattice prog)
 
-/-- Agda: `plus-valid`. -/
 theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
     (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) :
     interpSign (plus g₁ g₂) (.int (z₁ + z₂)) := by
@@ -254,7 +203,6 @@ theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
         subst h₂
         omega
 
-/-- Agda: `minus-valid`. -/
 theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
     (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) :
     interpSign (minus g₁ g₂) (.int (z₁ - z₂)) := by
@@ -292,7 +240,6 @@ theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
         subst h₂
         omega
 
-/-- Agda: `eval-valid` / the `SignEvalValid` instance. -/
 instance eval_valid : ValidExprEvaluator SignLattice prog := by
   constructor
   intro vs ρ e v hev
@@ -302,7 +249,7 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
     show interpSign (eval prog (.num n) vs) (.int n)
     cases n with
     | zero => rfl
-    | succ n' => exact ⟨n', congrArg Value.int (by push_cast; ring)⟩
+    | succ n' => exact ⟨n', congrArg Value.int (by norm_cast)⟩
   | var x v hxv =>
     intro hvs
     show interpSign (eval prog (.var x) vs) v
@@ -325,7 +272,6 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
     show interpSign (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂))
     exact minus_valid h₁ h₂
 
-/-- Agda: `WithProg.analyze-correct`. -/
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
     interpV (variablesAt prog.finalState (result SignLattice prog)) ρ :=
   Spa.analyze_correct SignLattice prog hrun
diff --git a/lean/Spa/Fixedpoint.lean b/lean/Spa/Fixedpoint.lean
index 8c282dd..975f927 100644
--- a/lean/Spa/Fixedpoint.lean
+++ b/lean/Spa/Fixedpoint.lean
@@ -1,41 +1,16 @@
-/-
-Port of `Fixedpoint.agda`.
-
-Same gas-based algorithm: iterate `f` starting at the chain-bottom `⊥`; since
-the lattice has fixed height `h`, a fixed point must be reached within `h + 1`
-steps, or we would build a `<`-chain longer than the longest one. We
-deliberately do *not* use mathlib's `OrderHom.lfp` (different proof approach,
-and not computable).
-
-As in Agda — where the module took `{{flA : IsFiniteHeightLattice A h …}}` —
-the finite-height structure arrives by instance resolution
-(`[FiniteHeightLattice α]`); only `f` and its monotonicity are explicit.
-
-Correspondence:
-  doStep             ↦ Spa.Fixedpoint.doStep   (the chain argument now carries
-                                                 `a₁ = ⊥` and its length in the
-                                                 `LTSeries` structure itself)
-  fix                ↦ Spa.Fixedpoint.fix
-  aᶠ                 ↦ Spa.Fixedpoint.aFix
-  aᶠ≈faᶠ             ↦ Spa.Fixedpoint.aFix_eq
-  stepPreservesLess  ↦ Spa.Fixedpoint.doStep_le
-  aᶠ≼                ↦ Spa.Fixedpoint.aFix_le
--/
 import Spa.Lattice
 
 namespace Spa.Fixedpoint
 
-open FiniteHeightLattice (height fixedHeight)
+open FiniteHeightLattice (height)
 
 variable {α : Type*} [Lattice α] [DecidableEq α] [FiniteHeightLattice α]
 
-/-- Agda: `doStep`. `g` is gas; the invariant `c.length + g = h + 1` guarantees
-that when gas runs out the chain contradicts boundedness. -/
 def doStep (f : α → α) (hf : Monotone f) :
     ∀ (g : ℕ) (c : LTSeries α), c.length + g = height (α := α) + 1 →
       c.last ≤ f c.last → {a : α // a = f a}
   | 0, c, hlen, _ =>
-    absurd ((fixedHeight (α := α)).bounded c) (by omega)
+    absurd (FiniteHeightLattice.chains_bounded c) (by omega)
   | g + 1, c, hlen, hle =>
     if heq : c.last = f c.last then
       ⟨c.last, heq⟩
@@ -44,29 +19,25 @@ def doStep (f : α → α) (hf : Monotone f) :
         (by simp [RelSeries.snoc]; omega)
         (by rw [RelSeries.last_snoc]; exact hf hle)
 
-/-- Agda: `fix`. Start iterating from `⊥`. -/
 def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
-  doStep f hf (height (α := α) + 1) (RelSeries.singleton _ (FiniteHeightLattice.bot α))
+  doStep f hf (height (α := α) + 1) (RelSeries.singleton _ ⊥)
     (by simp)
     (by simpa [RelSeries.last_singleton]
-          using FiniteHeightLattice.bot_le α (f (FiniteHeightLattice.bot α)))
+          using FiniteHeightLattice.bot_le α (f ⊥))
 
-/-- Agda: `aᶠ`. -/
 def aFix (f : α → α) (hf : Monotone f) : α :=
   (fix f hf).1
 
-/-- Agda: `aᶠ≈faᶠ`. -/
 theorem aFix_eq (f : α → α) (hf : Monotone f) :
     aFix f hf = f (aFix f hf) :=
   (fix f hf).2
 
-/-- Agda: `stepPreservesLess` — iteration stays below any fixed point. -/
 theorem doStep_le (f : α → α) (hf : Monotone f)
     {b : α} (hb : b = f b) :
     ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1)
       (hle : c.last ≤ f c.last), c.last ≤ b →
       (doStep f hf g c hlen hle : α) ≤ b
-  | 0, c, hlen, _ => fun _ => absurd ((fixedHeight (α := α)).bounded c) (by omega)
+  | 0, c, hlen, _ => fun _ => absurd (FiniteHeightLattice.chains_bounded c) (by omega)
   | g + 1, c, hlen, hle => fun hcb => by
     rw [doStep]
     split
@@ -74,7 +45,6 @@ theorem doStep_le (f : α → α) (hf : Monotone f)
     · exact doStep_le f hf hb g _ _ _
         (by rw [RelSeries.last_snoc]; exact le_of_le_of_eq (hf hcb) hb.symm)
 
-/-- Agda: `aᶠ≼` — `aFix` is below every fixed point of `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)
diff --git a/lean/Spa/Isomorphism.lean b/lean/Spa/Isomorphism.lean
index 3347dd9..161a8bd 100644
--- a/lean/Spa/Isomorphism.lean
+++ b/lean/Spa/Isomorphism.lean
@@ -1,58 +1,27 @@
-/-
-Port of `Isomorphism.agda` (`TransportFiniteHeight`).
-
-With propositional equality this module shrinks dramatically: the Agda
-hypotheses `f-preserves-≈`, `g-preserves-≈` are free, and `f-⊔-distr` /
-`g-⊔-distr` (which in the setoid world encoded monotonicity of `f` and `g`
-w.r.t. the derived order) become plain `Monotone` hypotheses. The chain
-transport `portChain₁` / `portChain₂` is mathlib's `LTSeries.map`, using that
-a monotone injective map between partial orders is strictly monotone.
-
-Correspondence:
-  IsInverseˡ / IsInverseʳ     ↦ explicit inverse hypotheses `hfg` / `hgf`
-  f-Injective / g-Injective   ↦ local `Function.LeftInverse.injective`
-  portChain₁ / portChain₂     ↦ LTSeries.map
-  instance fixedHeight        ↦ Spa.FixedHeight.transport
-  isFiniteHeightLattice,
-  finiteHeightLattice         ↦ Spa.FiniteHeightLattice.transport
--/
 import Spa.Lattice
 
 namespace Spa
 
-namespace FixedHeight
-
-variable {α β : Type*} [PartialOrder α] [PartialOrder β] {h : ℕ}
-
-/-- Agda: `TransportFiniteHeight.fixedHeight`. Transport a `FixedHeight`
-structure along a monotone inverse pair `f : α → β`, `g : β → α`. -/
-def transport (fh : FixedHeight α h) (f : α → β) (g : β → α)
-    (hf : Monotone f) (hg : Monotone g)
-    (hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
-    FixedHeight β h where
-  bot := f fh.bot
-  top := f fh.top
-  longestChain :=
-    fh.longestChain.map f
-      (hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
-  head_longestChain := by
-    rw [LTSeries.head_map, fh.head_longestChain]
-  last_longestChain := by
-    rw [LTSeries.last_map, fh.last_longestChain]
-  length_longestChain := fh.length_longestChain
-  bounded := fun c =>
-    fh.bounded
-      (c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
-
-end FixedHeight
-
-/-- Agda: `TransportFiniteHeight.finiteHeightLattice`. -/
+/-- Agda: `TransportFiniteHeight.finiteHeightLattice`. Transport a
+`FiniteHeightLattice` structure along a monotone inverse pair `f : α → β`,
+`g : β → α`. -/
 def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
-    (I : FiniteHeightLattice α) (f : α → β) (g : β → α)
+    [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
     (hf : Monotone f) (hg : Monotone g)
     (hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
     FiniteHeightLattice β where
+  bot := f ⊥
+  top := f ⊤
   height := I.height
-  fixedHeight := I.fixedHeight.transport f g hf hg hgf hfg
+  longest_chain :=
+    { series :=
+        I.longest_chain.series.map f
+          (hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
+      head_series := congrArg f I.longest_chain.head_series
+      last_series := congrArg f I.longest_chain.last_series
+      length_series := I.longest_chain.length_series }
+  chains_bounded := fun c =>
+    I.chains_bounded
+      (c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
 
 end Spa
diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean
index f6beae5..d5b9de3 100644
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -1,46 +1,16 @@
-/-
-Port of `Lattice.agda`.
-
-Most of the Agda module is *lifted* into mathlib, since we now work with
-propositional equality instead of a setoid:
-
-  IsSemilattice A _≈_ _⊔_   ↦  SemilatticeSup α
-  IsLattice A _≈_ _⊔_ _⊓_   ↦  Lattice α
-  _≼_ (a ⊔ b ≈ b)           ↦  a ≤ b           (bridge: `sup_eq_right`)
-  _≺_                       ↦  a < b
-  Monotonic                 ↦  Monotone
-  ⊔-assoc/⊔-comm/⊔-idemp    ↦  sup_assoc/sup_comm/sup_idem
-  absorb-⊔-⊓/absorb-⊓-⊔     ↦  sup_inf_self/inf_sup_self
-  ≼-refl/≼-trans/≼-antisym  ↦  le_refl/le_trans/le_antisymm
-  x≼x⊔y                     ↦  le_sup_left
-  ⊔-Monotonicˡ/ʳ            ↦  sup_le_sup_left/sup_le_sup_right
-  id-Mono/const-Mono        ↦  monotone_id/monotone_const
-  IsDecidable               ↦  DecidableEq (kept only where computation needs it)
-  Chain (Chain.agda)        ↦  LTSeries (chains of `<`); concat ↦ RelSeries.smash
-  ChainMapping.Chain-map    ↦  LTSeries.map (Monotone + Injective ⇒ StrictMono)
-
-What remains custom is exactly what mathlib does not have:
-  * monotonicity of folds over pairwise-related lists (foldr-Mono & friends),
-  * the fixed-height machinery (Chain.Height ↦ FixedHeight, Bounded),
-  * the proof that the bottom of the longest chain is a least element (⊥≼).
--/
 import Mathlib.Order.Lattice
 import Mathlib.Order.RelSeries
 
 namespace Spa
 
-/-! ### Monotonicity helpers (Lattice.agda, `Monotonic₂` and fold lemmas) -/
-
-/-- Agda: `Monotonic₂` (a pair of one-sided monotonicity proofs). -/
 def Monotone₂ {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ]
     (f : α → β → γ) : Prop :=
-  (∀ b, Monotone fun a => f a b) ∧ (∀ a, Monotone (f a))
+  (∀ b, Monotone (f · b)) ∧ (∀ a, Monotone (f a ·))
 
 section Folds
 
 variable {α β : Type*} [Preorder α] [Preorder β]
 
-/-- Agda: `foldr-Mono`. `Pairwise _≼₁_` becomes `List.Forall₂ (· ≤ ·)`. -/
 theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
     (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
     (hf₁ : ∀ b, Monotone fun a => f a b) (hf₂ : ∀ a, Monotone (f a)) :
@@ -50,7 +20,6 @@ theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
   | cons hxy _ ih =>
     exact le_trans (hf₁ _ hxy) (hf₂ _ ih)
 
-/-- Agda: `foldl-Mono`. -/
 theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
     (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
     (hf₁ : ∀ a, Monotone fun b => f b a) (hf₂ : ∀ b, Monotone (f b)) :
@@ -61,18 +30,16 @@ theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
     exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))
 
 omit [Preorder α] in
-/-- Agda: `foldr-Mono'` (fixed list, varying accumulator). -/
 theorem foldr_mono' (l : List α) (f : α → β → β)
-    (hf : ∀ a, Monotone (f a)) : Monotone fun b => l.foldr f b := by
+    (hf : ∀ a, Monotone (f a ·)) : Monotone fun b => l.foldr f b := by
   intro b₁ b₂ hb
   induction l with
   | nil => exact hb
   | cons x xs ih => exact hf x ih
 
 omit [Preorder α] in
-/-- Agda: `foldl-Mono'`. -/
 theorem foldl_mono' (l : List α) (f : β → α → β)
-    (hf : ∀ a, Monotone fun b => f b a) : Monotone fun b => l.foldl f b := by
+    (hf : ∀ a, Monotone (f · a)) : Monotone fun b => l.foldl f b := by
   intro b₁ b₂ hb
   induction l generalizing b₁ b₂ with
   | nil => exact hb
@@ -80,76 +47,40 @@ theorem foldl_mono' (l : List α) (f : β → α → β)
 
 end Folds
 
-/-! ### Fixed height (Chain.agda `Bounded`/`Height`, Lattice.agda `FixedHeight`) -/
-
-/-- Agda: `Chain.Bounded`. Every `<`-chain has length at most `n`. -/
 def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
   ∀ c : LTSeries α, c.length ≤ n
 
-/-- Agda: `Chain.Height` (with `FixedHeight h = Height h` from Lattice.agda).
-A longest chain runs from `⊥` to `⊤` and has length exactly `height`;
-no chain is longer. -/
-structure FixedHeight (α : Type*) [Preorder α] (height : ℕ) where
-  bot : α
-  top : α
-  longestChain : LTSeries α
-  head_longestChain : longestChain.head = bot
-  last_longestChain : longestChain.last = top
-  length_longestChain : longestChain.length = height
-  bounded : BoundedChains α height
+structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where
+  series : LTSeries α
+  head_series : series.head = f
+  last_series : series.last = t
+  length_series : series.length = n
 
-/-- Agda: `Chain.Bounded-suc-n` (a bounded order admits no chain one longer). -/
 theorem BoundedChains.no_longer {α : Type*} [Preorder α] {n : ℕ}
     (h : BoundedChains α n) (c : LTSeries α) : c.length ≠ n + 1 :=
   fun hc => absurd (h c) (by omega)
 
-/-- Re-index a `FixedHeight` along an equality of heights (used where Agda
-just rewrites with arithmetic identities). -/
-def FixedHeight.cast {α : Type*} [Preorder α] {m n : ℕ} (h : m = n)
-    (fh : FixedHeight α m) : FixedHeight α n where
-  bot := fh.bot
-  top := fh.top
-  longestChain := fh.longestChain
-  head_longestChain := fh.head_longestChain
-  last_longestChain := fh.last_longestChain
-  length_longestChain := h ▸ fh.length_longestChain
-  bounded := h ▸ fh.bounded
-
-@[simp] theorem FixedHeight.cast_bot {α : Type*} [Preorder α] {m n : ℕ}
-    (h : m = n) (fh : FixedHeight α m) : (fh.cast h).bot = fh.bot := rfl
-
-/-- Agda: `IsFiniteHeightLattice` / `FiniteHeightLattice` (bundled). Like the
-Agda code (which took `IsFiniteHeightLattice` as an instance argument `⦃·⦄`),
-this is a typeclass; downstream modules pick it up by instance resolution
-rather than threading a `FixedHeight` value. -/
-class FiniteHeightLattice (α : Type*) [Lattice α] where
+class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
   height : ℕ
-  fixedHeight : FixedHeight α height
+  longest_chain : PointedLTSeries α ⊥ ⊤ height
+  chains_bounded : BoundedChains α height
 
 namespace FixedHeight
 
 variable {α : Type*} [Lattice α] {h : ℕ}
 
-/-- Agda: `Known-⊥`. -/
-def KnownBot (fh : FixedHeight α h) : Prop := ∀ a : α, fh.bot ≤ a
-
-/-- Agda: `Known-⊤`. -/
-def KnownTop (fh : FixedHeight α h) : Prop := ∀ a : α, a ≤ fh.top
-
-/-- Agda: `⊥≼` — the bottom of the longest chain is a least element.
-Same proof: if `⊥ ⊓ a ≠ ⊥` then `⊥ ⊓ a < ⊥` prepends to the longest chain,
-contradicting boundedness. (The decidability hypothesis of the Agda proof is
-not needed classically.) -/
-theorem bot_le (fh : FixedHeight α h) : fh.KnownBot := by
+theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
   intro a
-  by_cases heq : fh.bot ⊓ a = fh.bot
+  by_cases heq : ⊥ ⊓ a = ⊥
   · exact inf_eq_left.mp heq
   · exfalso
-    have hlt : fh.bot ⊓ a < fh.bot :=
-      lt_of_le_of_ne inf_le_left heq
-    exact fh.bounded.no_longer
-      (fh.longestChain.cons (fh.bot ⊓ a) (fh.head_longestChain ▸ hlt))
-      (by simp [RelSeries.cons, fh.length_longestChain])
+    have lc := FiniteHeightLattice.longest_chain (α := α)
+    have hlt : ⊥ ⊓ a < lc.series.head := by
+      rw [lc.head_series]
+      exact lt_of_le_of_ne inf_le_left heq
+    exact FiniteHeightLattice.chains_bounded.no_longer
+      (lc.series.cons (⊥ ⊓ a) hlt)
+      (by simp [RelSeries.cons_length, lc.length_series])
 
 end FixedHeight
 
@@ -157,11 +88,7 @@ namespace FiniteHeightLattice
 
 variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
 
-/-- Agda: the `⊥` of `Chain.Height`, with the type explicit. -/
-def bot : α := (fixedHeight (α := α)).bot
-
-/-- Agda: `⊥≼` for the instance bottom. -/
-theorem bot_le (a : α) : bot α ≤ a := FixedHeight.bot_le _ a
+theorem bot_le (a : α) : (⊥ : α) ≤ a := FixedHeight.bot_le a
 
 end FiniteHeightLattice
 
diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean
index 1f2b585..ca425ed 100644
--- a/lean/Spa/Lattice/AboveBelow.lean
+++ b/lean/Spa/Lattice/AboveBelow.lean
@@ -175,6 +175,7 @@ theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
       · rw [htopl y hy]; exact le_top' _
     · exact le_rfl
   · intro x a b hab
+    show f x a ≤ f x b
     rcases le_cases hab with rfl | rfl | rfl
     · rw [hbotr]; exact bot_le' _
     · rcases eq_or_ne x bot with rfl | hx
@@ -264,25 +265,23 @@ theorem boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
   have h2 : rank c.last ≤ 2 := by cases c.last <;> simp [rank]
   omega
 
-/-- Agda: `Plain.longestChain` and `Plain.fixedHeight` — the witness `x`
-seeds the chain `⊥ ≺ [x] ≺ ⊤` of length 2. -/
-def plainFixedHeight (x : α) : FixedHeight (AboveBelow α) 2 where
+/-- Agda: `Plain.longestChain`/`Plain.fixedHeight` and
+`Plain.isFiniteHeightLattice`/`Plain.finiteHeightLattice` — the witness
+(`default`, playing the role of the Agda module parameter `x`) seeds the chain
+`⊥ ≺ [x] ≺ ⊤` of length 2. -/
+instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
   bot := bot
   top := top
-  longestChain :=
-    ((RelSeries.singleton _ bot).snoc (mk x)
-        (by rw [RelSeries.last_singleton]; exact bot_lt_mk x)).snoc top
-      (by rw [RelSeries.last_snoc]; exact mk_lt_top x)
-  head_longestChain := by simp
-  last_longestChain := by simp
-  length_longestChain := by simp [RelSeries.snoc, RelSeries.append]
-  bounded := boundedChains
-
-/-- Agda: `Plain.isFiniteHeightLattice` / `Plain.finiteHeightLattice`
-(`default` plays the role of the Agda module parameter `x`). -/
-instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
   height := 2
-  fixedHeight := plainFixedHeight default
+  longest_chain :=
+    { series :=
+        ((RelSeries.singleton _ bot).snoc (mk default)
+            (by rw [RelSeries.last_singleton]; exact bot_lt_mk default)).snoc top
+          (by rw [RelSeries.last_snoc]; exact mk_lt_top default)
+      head_series := by simp
+      last_series := by simp
+      length_series := by simp [RelSeries.snoc, RelSeries.append] }
+  chains_bounded := boundedChains
 
 end AboveBelow
 
diff --git a/lean/Spa/Lattice/FiniteMap.lean b/lean/Spa/Lattice/FiniteMap.lean
index 23b345b..3bfd6bc 100644
--- a/lean/Spa/Lattice/FiniteMap.lean
+++ b/lean/Spa/Lattice/FiniteMap.lean
@@ -1,71 +1,8 @@
-/-
-Port of `Lattice/FiniteMap.agda` (and the parts of `Lattice/Map.agda` it was
-built on).
-
-Representation change enabled by dropping the setoid: a finite map over a
-*fixed* key list `ks` is an association list whose key spine is *exactly* `ks`:
-
-    FiniteMap A B ks := { l : List (A × B) // l.map Prod.fst = ks }
-
-Since the spine (including order) is pinned by the type, the representation is
-canonical and propositional equality coincides with the Agda `_≈_` (pointwise
-value equality). The 1100-line `Lattice/Map.agda` — whose unordered-keys
-union/intersection and `Provenance` machinery existed to make `_≈_` workable —
-collapses into the positional `combine` below.
-
-Correspondence (Agda ↦ Lean):
-  FiniteMap, _≈_, ≈-Decidable    ↦ FiniteMap, `=`, DecidableEq instance
-  _⊔_/_⊓_ (via Map union/inter)  ↦ Max/Min via `combine`
-  isUnionSemilattice,
-  isIntersectSemilattice,
-  isLattice, lattice             ↦ instance Lattice (FiniteMap A B ks) (Lattice.mk',
-                                   i.e. the same "two semilattices + absorption" data)
-  _∈_, _∈k_, ∈k-dec, forget      ↦ Membership instance, MemKey (+ Decidable),
-                                   mem_key_of_mem
-  locate                         ↦ locate (computable)
-  all-equal-keys                 ↦ spine_eq
-  ∈k-exclusive                   ↦ immediate from memKey_iff (both sides ↔ k ∈ ks)
-  m₁≼m₂⇒m₁[k]≼m₂[k]              ↦ le_of_mem_mem (takes `ks.Nodup`; the Agda Map
-                                   carried key-uniqueness intrinsically)
-  m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂         ↦ trivial with `=` (congruence)
-  _updating_via_ + Map lemmas:
-    updating-via-keys-≡          ↦ (the `property` field of `updating`)
-    updating-via-∈k-forward      ↦ memKey_updating
-    updating-via-k∈ks            ↦ mem_updating
-    updating-via-k∈ks-≡          ↦ eq_of_mem_updating
-    updating-via-k∉ks-forward    ↦ mem_updating_of_not_mem
-    updating-via-k∉ks-backward   ↦ mem_of_mem_updating
-    f'-Monotonic (Map)           ↦ updating_mono
-  GeneralizedUpdate:
-    f'                           ↦ generalizedUpdate
-    f'-Monotonic                 ↦ generalizedUpdate_monotone
-    f'-∈k-forward                ↦ generalizedUpdate_memKey
-    f'-k∈ks                      ↦ generalizedUpdate_mem
-    f'-k∈ks-≡                    ↦ generalizedUpdate_mem_eq
-    f'-k∉ks-forward, -backward   ↦ generalizedUpdate_not_mem_forward, _backward
-  _[_], []-∈                     ↦ valuesAt, mem_valuesAt (takes `ks.Nodup`)
-  m₁≼m₂⇒m₁[ks]≼m₂[ks]            ↦ valuesAt_le
-  Provenance-union               ↦ mem_sup
-  ⊔-combines                     ↦ (omitted: only used inside the Agda
-                                   isomorphism proofs, which simplified away)
-  IterProdIsomorphism.from/to    ↦ toIter / ofIter — no `Unique ks` needed: the
-                                   spine-pinned representation is already
-                                   canonical, so the isomorphism is exact
-  from/to-preserves-≈, -⊔-distr  ↦ toIter_monotone / ofIter_monotone (with `≼`
-                                   being `≤`, the transport interface consumes
-                                   monotonicity directly)
-  from-to-inverseˡ/ʳ             ↦ toIter_ofIter / ofIter_toIter
-  to-build                       ↦ mem_ofIter_build
-  FixedHeight.fixedHeight        ↦ FiniteMap.fixedHeight (still obtained by
-                                   transport along the IterProd isomorphism)
-  ⊥-contains-bottoms             ↦ bot_contains_bots
--/
 import Spa.Lattice.IterProd
 import Spa.Isomorphism
 
 namespace Spa
 
-/-- Agda: `FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)`. -/
 def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
   { l : List (A × B) // l.map Prod.fst = ks }
 
@@ -76,14 +13,10 @@ variable {A B : Type*} {ks : List A}
 instance [DecidableEq A] [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
   fun a b => decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm
 
-/-- Agda: `all-equal-keys`. -/
 theorem spine_eq (fm₁ fm₂ : FiniteMap A B ks) :
     fm₁.val.map Prod.fst = fm₂.val.map Prod.fst :=
   fm₁.property.trans fm₂.property.symm
 
-/-! ### The lattice structure (`combine` replaces Map union/intersection) -/
-
-/-- Positional combination of two maps with equal spines. -/
 def combine (f : B → B → B) (l₁ l₂ : List (A × B)) : List (A × B) :=
   List.zipWith (fun p q => (p.1, f p.2 q.2)) l₁ l₂
 
@@ -154,8 +87,6 @@ instance : Min (FiniteMap A B ks) where
 @[simp] theorem inf_val (fm₁ fm₂ : FiniteMap A B ks) :
     (fm₁ ⊓ fm₂).val = combine (· ⊓ ·) fm₁.val fm₂.val := rfl
 
-/-- Agda: `isLattice`/`lattice` (built like the Agda record from the two
-semilattices plus absorption; `Lattice.mk'` defines `a ≤ b ↔ a ⊔ b = b`). -/
 instance : Lattice (FiniteMap A B ks) :=
   Lattice.mk'
     (fun a b => Subtype.ext (combine_comm _ sup_comm (spine_eq a b)))
@@ -165,8 +96,6 @@ instance : Lattice (FiniteMap A B ks) :=
     (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => sup_inf_self) (spine_eq a b)))
     (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => inf_sup_self) (spine_eq a b)))
 
-/-! ### Membership -/
-
 instance : Membership (A × B) (FiniteMap A B ks) :=
   ⟨fun fm p => p ∈ fm.val⟩
 
@@ -174,23 +103,18 @@ omit [Lattice B] in
 theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val :=
   Iff.rfl
 
-/-- Agda: `_∈k_`. -/
 def MemKey (k : A) (fm : FiniteMap A B ks) : Prop :=
   k ∈ fm.val.map Prod.fst
 
 omit [Lattice B] in
-/-- A key is in the map iff it is in the (fixed) key list
-(Agda: `∈k-exclusive` becomes a special case). -/
 theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by
   rw [MemKey, fm.property]
 
-/-- Agda: `∈k-dec`. -/
 instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] :
     Decidable (MemKey k fm) :=
   decidable_of_iff _ memKey_iff.symm
 
 omit [Lattice B] in
-/-- Agda: `forget`. -/
 theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
     (h : (k, v) ∈ fm) : MemKey k fm :=
   List.mem_map_of_mem _ h
@@ -212,15 +136,12 @@ private def locateList (k : A) :
         · exact h')
       ⟨v, List.mem_cons_of_mem _ hv⟩
 
-/-- Agda: `locate`. -/
 def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
     {v : B // (k, v) ∈ fm} :=
   locateList k fm.val h
 
 end Locate
 
-/-! ### The pointwise order -/
-
 theorem combine_eq_right_iff : ∀ {l₁ l₂ : List (A × B)},
     l₁.map Prod.fst = l₂.map Prod.fst →
     (combine (· ⊔ ·) l₁ l₂ = l₂ ↔
@@ -241,7 +162,6 @@ theorem combine_eq_right_iff : ∀ {l₁ l₂ : List (A × B)},
   | [], _ :: _, h => by simp at h
   | _ :: _, [], h => by simp at h
 
-/-- The order on finite maps is the pointwise order on values. -/
 theorem le_iff {fm₁ fm₂ : FiniteMap A B ks} :
     fm₁ ≤ fm₂ ↔
       List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) fm₁.val fm₂.val := by
@@ -282,15 +202,11 @@ private theorem forall₂_mem_mem {l₁ l₂ : List (A × B)}
         exact List.mem_map_of_mem _ h₁'
       · exact ih hnd.2 h₁' h₂'
 
-/-- Agda: `m₁≼m₂⇒m₁[k]≼m₂[k]`. The `Nodup` hypothesis was carried inside the
-Agda `Map` type. -/
 theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
     (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
     (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ :=
   forall₂_mem_mem (le_iff.mp hle) (fm₁.property.symm ▸ hks) h₁ h₂
 
-/-! ### Provenance of joined values -/
-
 omit [Lattice B] in
 private theorem mem_combine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)} {k : A} {v : B},
     l₁.map Prod.fst = l₂.map Prod.fst →
@@ -308,20 +224,15 @@ private theorem mem_combine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)
     · obtain ⟨v₁, v₂, hv, h₁, h₂⟩ := mem_combine f hsp.2 h'
       exact ⟨v₁, v₂, hv, List.mem_cons_of_mem _ h₁, List.mem_cons_of_mem _ h₂⟩
 
-/-- Agda: `Provenance-union` — a binding of a join comes from bindings of both
-maps. -/
 theorem mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
     (h : (k, v) ∈ fm₁ ⊔ fm₂) :
     ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ :=
   mem_combine _ (spine_eq fm₁ fm₂) h
 
-/-! ### Updating (Agda: `_updating_via_` and `GeneralizedUpdate`) -/
-
 section Updating
 
 variable [DecidableEq A]
 
-/-- Agda: `_updating_via_` — for each key in `ks'`, replace its value by `g k`. -/
 def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
     FiniteMap A B ks :=
   ⟨fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p), by
@@ -336,13 +247,11 @@ omit [Lattice B] in
       = fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p) := rfl
 
 omit [Lattice B] in
-/-- Agda: `updating-via-∈k-forward` (strengthened to an iff). -/
 theorem memKey_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} :
     MemKey k (updating fm ks' g) ↔ MemKey k fm := by
   rw [memKey_iff, memKey_iff]
 
 omit [Lattice B] in
-/-- Agda: `updating-via-k∈ks-≡`. -/
 theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
     {ks' : List A} {g : A → B} (hk : k ∈ ks')
     (h : (k, v) ∈ updating fm ks' g) : v = g k := by
@@ -356,21 +265,18 @@ theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
     exact absurd hk hmem
 
 omit [Lattice B] in
-/-- Agda: `updating-via-k∈ks`. -/
 theorem mem_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B}
     (hk : k ∈ ks') (hmem : MemKey k fm) : (k, g k) ∈ updating fm ks' g := by
   obtain ⟨v, hv⟩ := locate hmem
   exact List.mem_map.mpr ⟨(k, v), hv, by simp [hk]⟩
 
 omit [Lattice B] in
-/-- Agda: `updating-via-k∉ks-forward`. -/
 theorem mem_updating_of_not_mem {k : A} {v : B} {fm : FiniteMap A B ks}
     {ks' : List A} {g : A → B} (hk : k ∉ ks') (h : (k, v) ∈ fm) :
     (k, v) ∈ updating fm ks' g :=
   List.mem_map.mpr ⟨(k, v), h, by simp [hk]⟩
 
 omit [Lattice B] in
-/-- Agda: `updating-via-k∉ks-backward`. -/
 theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
     {ks' : List A} {g : A → B} (hk : k ∉ ks')
     (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
@@ -401,7 +307,6 @@ private theorem updating_mono_list {ks' : List A} {g₁ g₂ : A → B}
     · rw [if_neg h, if_neg (fun hy => h (hk.symm ▸ hy))]
       exact ⟨hk, hv⟩
 
-/-- Agda: `f'-Monotonic` at the `Map` level. -/
 theorem updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
     {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
     updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
@@ -413,52 +318,43 @@ end Updating
 
 section GeneralizedUpdate
 
-/-! Agda: `GeneralizedUpdate` (the "Exercise 4.26" construction). -/
-
 variable [DecidableEq A] {L : Type*} [Lattice L]
 
-/-- Agda: `GeneralizedUpdate.f'`. -/
 def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
     (ks' : List A) (l : L) : FiniteMap A B ks :=
   (f l).updating ks' (fun k => g k l)
 
 variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
 
-/-- Agda: `f'-Monotonic`. -/
 theorem generalizedUpdate_monotone (hf : Monotone f)
     (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
   fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
 
 omit [Lattice B] [Lattice L] in
-/-- Agda: `f'-∈k-forward`. -/
 theorem generalizedUpdate_memKey {k : A} {l : L}
     (h : MemKey k (f l)) : MemKey k (generalizedUpdate f g ks' l) := by
   unfold generalizedUpdate
   exact memKey_updating.mpr h
 
 omit [Lattice B] [Lattice L] in
-/-- Agda: `f'-k∈ks`. -/
 theorem generalizedUpdate_mem {k : A} {l : L} (hk : k ∈ ks')
     (h : MemKey k (f l)) : (k, g k l) ∈ generalizedUpdate f g ks' l := by
   unfold generalizedUpdate
   exact mem_updating hk h
 
 omit [Lattice B] [Lattice L] in
-/-- Agda: `f'-k∈ks-≡`. -/
 theorem generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
     (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := by
   unfold generalizedUpdate at h
   exact eq_of_mem_updating (g := fun k => g k l) hk h
 
 omit [Lattice B] [Lattice L] in
-/-- Agda: `f'-k∉ks-forward`. -/
 theorem generalizedUpdate_not_mem_forward {k : A} {v : B} {l : L} (hk : k ∉ ks')
     (h : (k, v) ∈ f l) : (k, v) ∈ generalizedUpdate f g ks' l := by
   unfold generalizedUpdate
   exact mem_updating_of_not_mem hk h
 
 omit [Lattice B] [Lattice L] in
-/-- Agda: `f'-k∉ks-backward`. -/
 theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
     (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := by
   unfold generalizedUpdate at h
@@ -466,8 +362,6 @@ theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ k
 
 end GeneralizedUpdate
 
-/-! ### Reading off values at a list of keys (Agda: `_[_]`) -/
-
 section ValuesAt
 
 variable [DecidableEq A]
@@ -476,7 +370,6 @@ private def lookup? (k : A) : List (A × B) → Option B
   | [] => none
   | p :: l' => if p.1 = k then some p.2 else lookup? k l'
 
-/-- Agda: `_[_]`. -/
 def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
   ks'.filterMap (fun k => lookup? k fm.val)
 
@@ -498,7 +391,6 @@ private theorem lookup?_eq_some_of_mem : ∀ {l : List (A × B)},
         exact hnd.1 this
 
 omit [Lattice B] in
-/-- Agda: `[]-∈`. -/
 theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
     {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' :=
   List.mem_filterMap.mpr
@@ -517,7 +409,6 @@ private theorem lookup?_forall₂ {l₁ l₂ : List (A × B)}
     · rw [if_neg hc, if_neg (fun hp => hc (hpq.1 ▸ hp))]
       exact ih
 
-/-- Agda: `m₁≼m₂⇒m₁[ks]≼m₂[ks]`. -/
 theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
     (ks' : List A) :
     List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
@@ -536,8 +427,6 @@ theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
 
 end ValuesAt
 
-/-! ### The isomorphism with `IterProd` and the fixed height -/
-
 section Iso
 
 omit [Lattice B] in
@@ -551,7 +440,6 @@ def headVal {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → B
   | ⟨[], h⟩ => absurd h (by simp)
   | ⟨p :: _, _⟩ => p.2
 
-/-- Agda: `pop`. -/
 def pop {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → FiniteMap A B ks'
   | ⟨[], h⟩ => absurd h (by simp)
   | ⟨_ :: l, h⟩ =>
@@ -565,13 +453,10 @@ theorem val_eq_cons {k : A} {ks' : List A} :
     simp only [List.map_cons, List.cons.injEq] at h
     simp [headVal, pop, ← h.1]
 
-/-- Agda: `IterProdIsomorphism.from`. -/
 def toIter : {ks : List A} → FiniteMap A B ks → IterProd B PUnit ks.length
   | [], _ => PUnit.unit
   | _ :: _, fm => (fm.headVal, toIter fm.pop)
 
-/-- Agda: `IterProdIsomorphism.to` (no `Unique ks` needed: the spine-pinned
-representation is canonical). -/
 def ofIter : (ks : List A) → IterProd B PUnit ks.length → FiniteMap A B ks
   | [], _ => ⟨[], rfl⟩
   | k :: ks', ip =>
@@ -579,7 +464,6 @@ def ofIter : (ks : List A) → IterProd B PUnit ks.length → FiniteMap A B ks
       simp [(ofIter ks' ip.2).property]⟩
 
 omit [Lattice B] in
-/-- Agda: `from-to-inverseʳ`. -/
 theorem ofIter_toIter : ∀ {ks : List A} (fm : FiniteMap A B ks),
     ofIter ks (toIter fm) = fm
   | [], fm => by
@@ -592,7 +476,6 @@ theorem ofIter_toIter : ∀ {ks : List A} (fm : FiniteMap A B ks),
       rw [ofIter_toIter fm.pop, ← val_eq_cons fm])
 
 omit [Lattice B] in
-/-- Agda: `from-to-inverseˡ`. -/
 theorem toIter_ofIter : ∀ (ks : List A) (ip : IterProd B PUnit ks.length),
     toIter (ofIter ks ip) = ip
   | [], _ => rfl
@@ -615,14 +498,12 @@ theorem pop_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
   rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
   exact (List.forall₂_cons.mp h').2
 
-/-- Agda: `from-preserves-≈` and `from-⊔-distr` (see header note). -/
 theorem toIter_monotone : ∀ {ks : List A},
     Monotone (toIter : FiniteMap A B ks → IterProd B PUnit ks.length)
   | [] => fun _ _ _ => le_refl _
   | _ :: _ => fun _ _ h =>
     Prod.mk_le_mk.mpr ⟨headVal_le h, toIter_monotone (pop_le h)⟩
 
-/-- Agda: `to-preserves-≈` and `to-⊔-distr` (see header note). -/
 theorem ofIter_monotone : ∀ (ks : List A), Monotone (ofIter (A := A) (B := B) ks)
   | [] => fun _ _ _ => le_refl _
   | k :: ks' => fun ip₁ ip₂ h => by
@@ -631,22 +512,16 @@ theorem ofIter_monotone : ∀ (ks : List A), Monotone (ofIter (A := A) (B := B)
                         ((k, ip₂.1) :: (ofIter ks' ip₂.2).val)
     exact List.Forall₂.cons ⟨rfl, h.1⟩ (le_iff.mp (ofIter_monotone ks' h.2))
 
-/-- Agda: `FixedHeight.fixedHeight` — a finite map into a lattice of height
-`hB` has height `|ks| · hB`, by transport along the `IterProd` isomorphism. -/
-def fixedHeight {hB : ℕ} (fhB : FixedHeight B hB) (ks : List A) :
-    FixedHeight (FiniteMap A B ks) (ks.length * hB) :=
-  ((IterProd.fixedHeight fhB punitFixedHeight ks.length).transport
-      (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
-      (toIter_ofIter ks) (fun fm => ofIter_toIter fm)).cast (by ring)
+def fixedHeight [FiniteHeightLattice B] (ks : List A) :
+    FiniteHeightLattice (FiniteMap A B ks) :=
+  FiniteHeightLattice.transport
+    (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
+    (toIter_ofIter ks) (fun fm => ofIter_toIter fm)
 
-/-- Agda: `isFiniteHeightLattice`/`finiteHeightLattice` of `Lattice/FiniteMap.agda`
-(there instance arguments; here an instance). -/
-instance [IB : FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) where
-  height := ks.length * IB.height
-  fixedHeight := fixedHeight IB.fixedHeight ks
+instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
+  fixedHeight ks
 
 omit [Lattice B] in
-/-- Agda: `to-build`. -/
 theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B},
     (k, v) ∈ ofIter ks (IterProd.build b PUnit.unit ks.length) → v = b
   | [], _, _, h => by simp [ofIter, mem_def] at h
@@ -655,12 +530,11 @@ theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B},
     · exact (Prod.ext_iff.mp heq).2
     · exact mem_ofIter_build h'
 
-/-- Agda: `⊥-contains-bottoms`. -/
-theorem bot_contains_bots {hB : ℕ} (fhB : FixedHeight B hB) {k : A} {v : B}
-    (h : (k, v) ∈ (fixedHeight fhB ks).bot) : v = fhB.bot := by
-  have hbot : (fixedHeight fhB ks).bot
-      = ofIter ks (IterProd.build fhB.bot PUnit.unit ks.length) := by
-    show ofIter ks (IterProd.fixedHeight fhB punitFixedHeight ks.length).bot = _
+theorem bot_contains_bots [FiniteHeightLattice B] {k : A} {v : B}
+    (h : (k, v) ∈ (fixedHeight ks).bot) : v = (⊥ : B) := by
+  have hbot : (fixedHeight ks).bot
+      = ofIter ks (IterProd.build (⊥ : B) (⊥ : PUnit) ks.length) := by
+    show ofIter ks (IterProd.fixedHeight (A := B) (B := PUnit) ks.length).bot = _
     rw [IterProd.bot_fixedHeight]
   rw [hbot] at h
   exact mem_ofIter_build h
diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean
index 967cdf3..cffa120 100644
--- a/lean/Spa/Lattice/IterProd.lean
+++ b/lean/Spa/Lattice/IterProd.lean
@@ -13,12 +13,11 @@ Correspondence:
   isLattice/lattice   ↦ instance Spa.IterProd.instLattice
   fixedHeight,
   isFiniteHeightLattice,
-  finiteHeightLattice ↦ Spa.IterProd.fixedHeight (+ FiniteHeightLattice instance)
+  finiteHeightLattice ↦ Spa.IterProd.fixedHeight (+ instFiniteHeight instance)
   ⊥-built             ↦ Spa.IterProd.bot_fixedHeight
 -/
 import Spa.Lattice.Prod
 import Spa.Lattice.Unit
-import Mathlib.Tactic.Ring
 
 namespace Spa
 
@@ -51,25 +50,21 @@ def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
 
 variable [Lattice A] [Lattice B]
 
-/-- Agda: `fixedHeight` (the `isFiniteHeightIfSupported` recursion). -/
-def fixedHeight {hA hB : ℕ} (fhA : FixedHeight A hA) (fhB : FixedHeight B hB) :
-    (k : ℕ) → FixedHeight (IterProd A B k) (k * hA + hB)
-  | 0 => fhB.cast (by ring)
-  | k + 1 => (fhA.prod (fixedHeight fhA fhB k)).cast (by ring)
+def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
+    ∀ k, FiniteHeightLattice (IterProd A B k)
+  | 0 => inferInstanceAs (FiniteHeightLattice B)
+  | k + 1 => @Spa.prod A (IterProd A B k) _ (instLattice k) _ (fixedHeight k)
 
-/-- Agda: `⊥-built` — the bottom of the iterated product is built from the
-component bottoms. -/
-theorem bot_fixedHeight {hA hB : ℕ} (fhA : FixedHeight A hA) (fhB : FixedHeight B hB) :
-    ∀ k, (fixedHeight fhA fhB k).bot = build fhA.bot fhB.bot k
+instance instFiniteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
+    FiniteHeightLattice (IterProd A B k) := fixedHeight k
+
+theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
+    ∀ k, (fixedHeight (A := A) (B := B) k).bot = build (⊥ : A) (⊥ : B) k
   | 0 => rfl
   | k + 1 => by
-    show (fhA.bot, (fixedHeight fhA fhB k).bot) = (fhA.bot, build fhA.bot fhB.bot k)
-    rw [bot_fixedHeight fhA fhB k]
-
-instance [IA : FiniteHeightLattice A] [IB : FiniteHeightLattice B] (k : ℕ) :
-    FiniteHeightLattice (IterProd A B k) where
-  height := k * IA.height + IB.height
-  fixedHeight := fixedHeight IA.fixedHeight IB.fixedHeight k
+    show ((⊥ : A), (fixedHeight (A := A) (B := B) k).bot)
+        = ((⊥ : A), build (⊥ : A) (⊥ : B) k)
+    rw [bot_fixedHeight k]
 
 end IterProd
 
diff --git a/lean/Spa/Lattice/Prod.lean b/lean/Spa/Lattice/Prod.lean
index 240dabd..f4f2ba6 100644
--- a/lean/Spa/Lattice/Prod.lean
+++ b/lean/Spa/Lattice/Prod.lean
@@ -1,16 +1,3 @@
-/-
-Port of `Lattice/Prod.agda`.
-
-The component-wise lattice structure on `α × β` is lifted into mathlib
-(`Prod.instLattice`), as is decidability of equality. What remains custom is
-the fixed-height content:
-
-  unzip                      ↦ LTSeries.exists_unzip
-  a,∙-Monotonic/∙,b-Monotonic ↦ Prod.mk_lt_mk_iff_right/left (strict mono of
-                                the two injections, used to map the chains)
-  fixedHeight (h₁ + h₂)      ↦ FixedHeight.prod
-  isFiniteHeightLattice      ↦ instance FiniteHeightLattice (α × β)
--/
 import Spa.Lattice
 
 namespace Spa
@@ -19,8 +6,6 @@ section Unzip
 
 variable {α β : Type*} [PartialOrder α] [PartialOrder β]
 
-/-- Agda: `unzip` — a chain in the product splits into chains of the
-components whose lengths sum to at least the original length. -/
 theorem LTSeries.exists_unzip (c : LTSeries (α × β)) :
     ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
       c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
@@ -78,35 +63,35 @@ section FixedHeight
 
 variable {α β : Type*} [Lattice α] [Lattice β]
 
-/-- Agda: `Lattice/Prod.agda`'s `fixedHeight` — the product of lattices of
-heights `h₁` and `h₂` has height `h₁ + h₂`. The longest chain climbs the first
-component (at `⊥₂`), then the second component (at `⊤₁`). -/
-def FixedHeight.prod {h₁ h₂ : ℕ} (fhA : FixedHeight α h₁) (fhB : FixedHeight β h₂) :
-    FixedHeight (α × β) (h₁ + h₂) where
-  bot := (fhA.bot, fhB.bot)
-  top := (fhA.top, fhB.top)
-  longestChain :=
-    RelSeries.smash
-      (fhA.longestChain.map (fun a => (a, fhB.bot))
-        (fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
-      (fhB.longestChain.map (fun b => (fhA.top, b))
-        (fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
-      (by simp [fhA.last_longestChain, fhB.head_longestChain])
-  head_longestChain := by simp [fhA.head_longestChain]
-  last_longestChain := by simp [fhB.last_longestChain]
-  length_longestChain := by
-    simp [fhA.length_longestChain, fhB.length_longestChain]
-  bounded := fun c => by
-    obtain ⟨c₁, c₂, -, -, -, -, hlen⟩ := LTSeries.exists_unzip c
-    have h₁ := fhA.bounded c₁
-    have h₂ := fhB.bounded c₂
-    omega
-
-/-- Agda: `Lattice/Prod.agda`'s `isFiniteHeightLattice`/`finiteHeightLattice`. -/
-instance [IA : FiniteHeightLattice α] [IB : FiniteHeightLattice β] :
+instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
     FiniteHeightLattice (α × β) where
-  height := IA.height + IB.height
-  fixedHeight := IA.fixedHeight.prod IB.fixedHeight
+  bot := ((⊥ : α), (⊥ : β))
+  top := ((⊤ : α), (⊤ : β))
+  height := A.height + B.height
+  longest_chain :=
+    { series :=
+        RelSeries.smash
+          (A.longest_chain.series.map (fun a => (a, (⊥ : β)))
+            (fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
+          (B.longest_chain.series.map (fun b => ((⊤ : α), b))
+            (fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
+          (by simp [A.longest_chain.last_series, B.longest_chain.head_series])
+      head_series :=
+        (RelSeries.head_smash _).trans
+          ((LTSeries.head_map _ _ _).trans
+            (congrArg (·, (⊥ : β)) A.longest_chain.head_series))
+      last_series :=
+        (RelSeries.last_smash _).trans
+          ((LTSeries.last_map _ _ _).trans
+            (congrArg ((⊤ : α), ·) B.longest_chain.last_series))
+      length_series := by
+        show A.longest_chain.series.length + B.longest_chain.series.length = _
+        rw [A.longest_chain.length_series, B.longest_chain.length_series] }
+  chains_bounded := fun c => by
+    obtain ⟨c₁, c₂, -, -, -, -, hlen⟩ := LTSeries.exists_unzip c
+    have h₁ := A.chains_bounded c₁
+    have h₂ := B.chains_bounded c₂
+    omega
 
 end FixedHeight
 
diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean
index 7ca7ec8..7aa48cf 100644
--- a/lean/Spa/Lattice/Unit.lean
+++ b/lean/Spa/Lattice/Unit.lean
@@ -18,18 +18,11 @@ theorem boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton 
   exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)
 
 /-- Agda: `Lattice/Unit.agda`'s `fixedHeight`. -/
-def punitFixedHeight : FixedHeight PUnit 0 where
+instance : FiniteHeightLattice PUnit where
   bot := PUnit.unit
   top := PUnit.unit
-  longestChain := RelSeries.singleton _ PUnit.unit
-  head_longestChain := rfl
-  last_longestChain := rfl
-  length_longestChain := rfl
-  bounded := boundedChains_of_subsingleton PUnit 0
-
-/-- Agda: `Lattice/Unit.agda`'s `isFiniteHeightLattice`. -/
-instance : FiniteHeightLattice PUnit where
   height := 0
-  fixedHeight := punitFixedHeight
+  longest_chain := { series := RelSeries.singleton _ PUnit.unit, head_series := refl _, last_series := refl _, length_series := refl _ }
+  chains_bounded := boundedChains_of_subsingleton PUnit 0
 
 end Spa