DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Simplify the strict-step extraction in LTSeries.exists_unzip

Browse Source 
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 <noreply@anthropic.com>
This commit is contained in:
Danila Fedorin
2026-06-24 14:22:24 -05:00
parent 93f913a699
commit 97a9150bf3
1 changed files with 2 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
lean/Spa/Lattice/Prod.lean
View File

@@ -27,16 +27,13 @@ theorem LTSeries.exists_unzip (c : LTSeries (α × β)) :
| succ n ih => | succ n ih =>
intro c hn intro c hn
have h0 : c.length ≠ 0 := by omega have h0 : c.length ≠ 0 := by omega
haveI : NeZero c.length := ⟨h0⟩
obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ := obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ :=
ih (c.tail h0) (by simp [RelSeries.tail_length, hn]) ih (c.tail h0) (by simp [RelSeries.tail_length, hn])
rw [RelSeries.last_tail] at hl₁ hl₂ rw [RelSeries.last_tail] at hl₁ hl₂
rw [RelSeries.head_tail] at hh₁ hh₂ rw [RelSeries.head_tail] at hh₁ hh₂
rw [RelSeries.tail_length] at hlen rw [RelSeries.tail_length] at hlen
have hstep : c.head < c 1 := by have hstep : c.head < c 1 := c.strictMono Fin.one_pos'
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
obtain ⟨hle1, hle2⟩ := Prod.le_def.mp hstep.le 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 hle1 with heq1 | hlt1 <;>
rcases eq_or_lt_of_le hle2 with heq2 | hlt2 rcases eq_or_lt_of_le hle2 with heq2 | hlt2