diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean
index 29e8946..c7f1f10 100644
--- a/lean/Spa/Lattice/AboveBelow.lean
+++ b/lean/Spa/Lattice/AboveBelow.lean
@@ -49,36 +49,22 @@ instance : Min (AboveBelow α) where
     (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl
 
 protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
-    [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
-  split_ifs with h₁ h₂ h₂ <;> simp_all
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> aesop
 
 protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
-    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
-  split_ifs <;> simp_all
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> aesop
 
 protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
-    [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
-  split_ifs with h₁ h₂ h₂ <;> simp_all
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> aesop
 
 protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
-    simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
-  split_ifs <;> simp_all
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> aesop
 
 protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
-    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
-               bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
-    try (split_ifs <;> simp_all)
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> aesop
 
 protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
-    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
-               bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
-    try (split_ifs <;> simp_all)
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> aesop
 
 instance : Lattice (AboveBelow α) :=
   Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc