From a43972c856b0e1a2c92104fcd650fe2f204391d5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 15:06:12 +0200
Subject: [PATCH] chore: don't use grind in HTTP (#13639)

---
 src/Std/Http/Internal/LowerCase.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Std/Http/Internal/LowerCase.lean b/src/Std/Http/Internal/LowerCase.lean
index 1a02239148..c4cb106390 100644
--- a/src/Std/Http/Internal/LowerCase.lean
+++ b/src/Std/Http/Internal/LowerCase.lean
@@ -50,7 +50,14 @@ instance : Decidable (IsLowerCase s) :=
 namespace IsLowerCase
 
 private theorem Char.toLower_idempotent (c : Char) : c.toLower.toLower = c.toLower := by
-  grind [Char.toLower]
+  simp only [Char.toLower]
+  split
+  · split
+    · next h1 h2 =>
+      simp only [UInt32.le_iff_toNat_le, UInt32.toNat_add, seval] at h1 h2
+      omega
+    · simp
+  · rfl
 
 /--
 Proof that applying `toLower` to any string results in a string that satisfies the `IsLowerCase`