diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean
index e34fda9..bcccc79 100644
--- a/lean/Spa/Lattice/AboveBelow.lean
+++ b/lean/Spa/Lattice/AboveBelow.lean
@@ -32,6 +32,7 @@ any inherent structure beyond "matching exactly".
 namespace Spa
 
 /-- The above-below lattice, with bottom element `bot` and top element `top`. -/
+@[aesop safe cases]
 inductive AboveBelow (α : Type*) where
   | bot
   | top
@@ -40,8 +41,6 @@ inductive AboveBelow (α : Type*) where
 
 namespace AboveBelow
 
-attribute [aesop safe cases] AboveBelow
-
 instance {α : Type*} [ToString α] : ToString (AboveBelow α) where
   toString
     | bot => "⊥"
@@ -108,14 +107,9 @@ 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)
-
-lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
-  lt_of_le_of_ne (le_top' _) (by simp)
-
-lemma bot_lt_top : (bot : AboveBelow α) < top :=
-  lt_of_le_of_ne (bot_le' _) (by simp)
+lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lt_of_le_of_ne (bot_le' _) (by simp)
+lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top := lt_of_le_of_ne (le_top' _) (by simp)
+lemma bot_lt_top : (bot : AboveBelow α) < top := lt_of_le_of_ne (bot_le' _) (by simp)
 
 lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
     a = bot ∨ b = top ∨ a = b := by