From 2598df690cd072a5de47ae04e82dd45b657cd379 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 29 Jun 2026 08:16:55 -0500 Subject: [PATCH] Slightly tweak AboveBelow proofs --- lean/Spa/Lattice/AboveBelow.lean | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) 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