chore: bump Std (#12256)

Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Apr 19, 2024 · 11f79c5 · 11f79c5
1 parent 1d4a722
commit 11f79c5
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 7 deletions.
diff --git a/Mathlib/Data/String/Lemmas.lean b/Mathlib/Data/String/Lemmas.lean
@@ -12,12 +12,6 @@ namespace String
 lemma congr_append : ∀ (a b : String), a ++ b = String.mk (a.data ++ b.data)
   | ⟨_⟩, ⟨_⟩ => rfl
 
-@[simp] lemma length_append : ∀ (as bs : String), (as ++ bs).length = as.length + bs.length
-  | ⟨as⟩, ⟨bs⟩ => by
-    rw [congr_append]
-    simp only [String.length]
-    exact List.length_append as bs
-
 @[simp] lemma length_replicate (n : ℕ) (c : Char) : (replicate n c).length = n := by
   simp only [String.length, String.replicate, List.length_replicate]
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "cb172855f1712a9e906e91f3e14541960562fb78",
+   "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",