update tryAtEachStep

dwrensha · Dec 5, 2024 · aefb0e5 · aefb0e5
1 parent 0dfe6c8
commit aefb0e5
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/Compfiles/Imo2024P5.lean b/Compfiles/Imo2024P5.lean
@@ -129,9 +129,7 @@ lemma coe_coe_row1 (hN : 2 ≤ N) : (((row1 hN) : Fin (N + 2)) : ℕ) = 1 :=
 def row2 (hN : 2 ≤ N) : InteriorRow N :=
   ⟨⟨2, by omega⟩, ⟨by
     simp only [Fin.le_def, Fin.val_one]
-    omega, by
-    simp only [Fin.le_def]
-    omega⟩⟩
+    omega, Fin.mk_le_mk.mpr hN⟩⟩
 
 /-- Reflecting monster data. -/
 def MonsterData.reflect (m : MonsterData N) : MonsterData N where

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f072223cf96313ee0e5a70b8c41fe8632622253d",
+   "rev": "c07c298daae923a6700df67171272b1900384841",
    "name": "tryAtEachStep",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",