From 75628f029abfd9829a1259a6e1dd7758d548c13f Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 16 Nov 2025 18:21:09 +0100
Subject: Lean 4.24

---
 Common/Substring.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Common')

diff --git a/Common/Substring.lean b/Common/Substring.lean
index 4ed39b4..f51b088 100644
--- a/Common/Substring.lean
+++ b/Common/Substring.lean
@@ -5,7 +5,7 @@ namespace Substring
 theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos) : s.nextn n p ≥ p := by
   unfold Substring.nextn
   cases n
-  case zero => simp[String.Pos.le_iff]
+  case zero => simp
   case succ nn =>
     simp
     unfold Substring.next
-- 
cgit v1.2.3