diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index e9f2d8d88987..d8ac004e5d88 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2375,10 +2375,7 @@ Indexing a `String` by a byte position is constant-time, while codepoint
 positions need to be translated internally to byte positions in linear-time.
 
 A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.endPos` and `p`
-lies on a UTF8 byte boundary. This notion is properly introduced in [std's
-`String.Pos.Valid`][valid].
-
-[valid]: https://leanprover-community.github.io/mathlib4_docs/Std/Data/String/Lemmas.html#String.Pos.Valid
+lies on a UTF8 byte boundary.
 -/
 structure String.Pos where
   /-- Get the underlying byte index of a `String.Pos` -/