From 2868457bb85f4f0eb20d433027c72cb22888992b Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sun, 15 Oct 2023 20:00:40 -0400
Subject: [PATCH] Revert "fix: add type annotation to `by simpa using ... `"

This reverts commit 038ff75800d716a4946d23251cf8992d767c639f.
---
 Std/Data/String/Lemmas.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Std/Data/String/Lemmas.lean b/Std/Data/String/Lemmas.lean
index 291de7a21b..cfe42277b2 100644
--- a/Std/Data/String/Lemmas.lean
+++ b/Std/Data/String/Lemmas.lean
@@ -466,9 +466,7 @@ theorem splitAux_of_valid (p l m r acc) :
     splitAux ⟨l ++ m ++ r⟩ p ⟨utf8Len l⟩ ⟨utf8Len l + utf8Len m⟩ acc =
       acc.reverse ++ (List.splitOnP.go p r m.reverse).map mk := by
   unfold splitAux
-  simp [show utf8Len l + (utf8Len m + utf8Len r) ≤ utf8Len l + utf8Len m ↔ r = [] from by
-    simpa using atEnd_of_valid (l ++ m) r]
-  split
+  simp [by simpa using atEnd_of_valid (l ++ m) r]; split
   · subst r; simpa [List.splitOnP.go] using extract_of_valid l m []
   · obtain ⟨c, r, rfl⟩ := r.exists_cons_of_ne_nil ‹_›
     simp [by simpa using (⟨get_of_valid (l++m) (c::r), next_of_valid (l++m) c r,