From 4379a1b052a7b7843613d5a3217b4bdbe37341fd Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 12 Oct 2025 23:44:28 +0200
Subject: Lean 4.20.1

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

(limited to 'Common')

diff --git a/Common/Substring.lean b/Common/Substring.lean
index 194e405..4ed39b4 100644
--- a/Common/Substring.lean
+++ b/Common/Substring.lean
@@ -44,7 +44,6 @@ theorem drop_bsize_dec (s : Substring) (n : Nat) (h₁ : ¬s.isEmpty) (h₂ : n
         split <;> try split <;> try split
         all_goals
           simp
-          omega
     else
       have h₄ : s.stopPos.byteIdx - (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring}.nextn nn (if s.startPos + 0 = s.stopPos then 0 else { byteIdx := (s.str.next (s.startPos + 0)).byteIdx - s.startPos.byteIdx })).byteIdx)  = 0 := by
         omega
-- 
cgit v1.2.3