From 8c37a4c049eb361aafbed27edf0f3e2a4bb7deb3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 22 Jun 2026 18:46:58 -0500 Subject: [PATCH] Lean: inline BoundedChains.no_longer into FixedHeight.bot_le MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The lemma had a single caller. Inline it as `chains_bounded` applied to the over-long chain, rewriting its length to `height + 1 ≤ height` and closing with `omega`, and drop the standalone theorem. Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Lattice.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean index d5b9de3..d3d67d3 100644 --- a/lean/Spa/Lattice.lean +++ b/lean/Spa/Lattice.lean @@ -56,10 +56,6 @@ structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where last_series : series.last = t length_series : series.length = n -theorem BoundedChains.no_longer {α : Type*} [Preorder α] {n : ℕ} - (h : BoundedChains α n) (c : LTSeries α) : c.length ≠ n + 1 := - fun hc => absurd (h c) (by omega) - class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where height : ℕ longest_chain : PointedLTSeries α ⊥ ⊤ height @@ -78,9 +74,9 @@ theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by 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]) + have hbound := FiniteHeightLattice.chains_bounded (lc.series.cons (⊥ ⊓ a) hlt) + rw [RelSeries.cons_length, lc.length_series] at hbound + omega end FixedHeight