From 47d54f5b4bca3a38843843441f6b72195ba8fbfc Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 28 Jun 2026 15:01:24 -0500
Subject: [PATCH] Further simplify proofs in AboveBelow

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 lean/Spa/Lattice/AboveBelow.lean | 54 +++++++-------------------------
 1 file changed, 12 insertions(+), 42 deletions(-)

diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean
index 7cf7dc0..e34fda9 100644
--- a/lean/Spa/Lattice/AboveBelow.lean
+++ b/lean/Spa/Lattice/AboveBelow.lean
@@ -119,21 +119,8 @@ lemma bot_lt_top : (bot : AboveBelow α) < top :=
 
 lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
     a = bot ∨ b = top ∨ a = b := by
-  have hsup := le_iff.mp h
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y
-  · exact Or.inl rfl
-  · exact Or.inr (Or.inl rfl)
-  · exact Or.inl rfl
-  · exact absurd hsup (by simp)
-  · exact Or.inr (Or.inl rfl)
-  · exact absurd hsup (by simp)
-  · exact absurd hsup (by simp)
-  · exact Or.inr (Or.inl rfl)
-  · rw [mk_sup_mk] at hsup
-    by_cases hxy : x = y
-    · exact Or.inr (Or.inr (by rw [hxy]))
-    · rw [if_neg hxy] at hsup
-      exact absurd hsup (by simp)
+  rw [le_iff] at h
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp_all
 
 /-- If `f` sends `⊥` to `⊥` (in both arguments) and `⊤` to `⊤`
     (against any non-`⊥` argument), it is monotone in both arguments.
@@ -145,23 +132,10 @@ lemma monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
     (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
     (htopl : ∀ y, y ≠ bot → f top y = top)
     (htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by
-  constructor
-  · intro y a b hab
-    show f a y ≤ f b y
-    rcases le_cases hab with rfl | rfl | rfl
-    · rw [hbotl]; exact bot_le' _
-    · rcases eq_or_ne y bot with rfl | hy
-      · rw [hbotr, hbotr]
-      · 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
-      · rw [hbotl, hbotl]
-      · rw [htopr x hx]; exact le_top' _
-    · exact le_rfl
+  constructor <;> intro c a b hab <;>
+    rcases eq_or_ne c bot with rfl | hc <;>
+    rcases le_cases hab with rfl | rfl | rfl <;>
+    simp [hbotl, hbotr, htopl, htopr, bot_le', le_top', *]
 
 section Interp
 
@@ -178,8 +152,10 @@ lemma interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
 lemma interp_inf_of
     (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v))
     {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by
-  rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> try aesop
-  exfalso; exact (hdisj h v left right)
+  rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> simp_all
+  split
+  · exact h.2
+  · next hne => exact (hdisj hne v h.1 h.2).elim
 
 end Interp
 
@@ -199,14 +175,8 @@ lemma not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
 /-- The rank of elements is strictly monotonic. -/
 lemma rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
   intro a b hab
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y
-    <;> try simp [rank]
-  · exact absurd hab (lt_irrefl _)
-  · exact absurd hab (bot_le' _).not_lt
-  · exact absurd hab (lt_irrefl _)
-  · exact absurd hab (le_top' _).not_lt
-  · exact absurd hab (bot_le' _).not_lt
-  · exact absurd hab (not_mk_lt_mk x y)
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
+    simp_all [rank, not_mk_lt_mk, (bot_le' _).not_lt, (le_top' _).not_lt]
 
 /-- All chains in the above-below lattice have at most 2 comparisons. -/
 lemma boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by