fix: move set_option linter.deprecated false inside @[expose] public section

`set_option ... in @[expose] public section` causes the section's
declarations to not be exported via normal `import`. Moving the
`set_option` inside the section fixes this.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: kim-em

Batteries/Data/String/Lemmas.lean

@@ -20,9 +20,10 @@ import all Init.Data.String.Modify  -- for unfolding `String.mapAux`
 import all Batteries.Data.String.Legacy -- for unfolding `String.Legacy.map`
 import all Init.Data.String.Legacy -- for unfolding `String.splitOnAux`
 
-set_option linter.deprecated false in
 @[expose] public section
 
+set_option linter.deprecated false
+
 namespace String
 
 -- TODO(kmill): add `@[ext]` attribute to `String.ext` in core.