From 97a9150bf31d077e8a0acc346897e422c407ac23 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 24 Jun 2026 14:22:24 -0500 Subject: [PATCH] Simplify the strict-step extraction in LTSeries.exists_unzip Derive c.head < c 1 from the series' StrictMono instance and Fin.one_pos' instead of unfolding c.step with manual Fin.succ index arithmetic. Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Lattice/Prod.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/lean/Spa/Lattice/Prod.lean b/lean/Spa/Lattice/Prod.lean index 454f2f9..2416b0b 100644 --- a/lean/Spa/Lattice/Prod.lean +++ b/lean/Spa/Lattice/Prod.lean @@ -27,16 +27,13 @@ theorem LTSeries.exists_unzip (c : LTSeries (α × β)) : | succ n ih => intro c hn have h0 : c.length ≠ 0 := by omega + haveI : NeZero c.length := ⟨h0⟩ obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ := ih (c.tail h0) (by simp [RelSeries.tail_length, hn]) rw [RelSeries.last_tail] at hl₁ hl₂ rw [RelSeries.head_tail] at hh₁ hh₂ rw [RelSeries.tail_length] at hlen - have hstep : c.head < c 1 := by - have h := c.step ⟨0, by omega⟩ - have h1 : (⟨0, by omega⟩ : Fin c.length).succ = 1 := by - ext; simp [Fin.val_one, Nat.mod_eq_of_lt (by omega : 1 < c.length + 1)] - rwa [h1] at h + have hstep : c.head < c 1 := c.strictMono Fin.one_pos' obtain ⟨hle1, hle2⟩ := Prod.le_def.mp hstep.le rcases eq_or_lt_of_le hle1 with heq1 | hlt1 <;> rcases eq_or_lt_of_le hle2 with heq2 | hlt2