chore: isolate String.length

[TwoFX]

This PR removes all uses of the String.length function from core.

This is in preparation for a future deprecation of the String.length function. Note: the string length can still be obtained in linear time using s.chars.length.

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for 91a0f41 against 043b8a7 are in! @TwoFX

• 🟥 build//instructions: +22.9G (+0.18%)

Large changes (1🟥)

• 🟥 workspaceSymbols//instructions: +1.0G (+3.97%)

Medium changes (3🟥)

• 🟥 build/module/Lake.Util.Cli//bytes .olean: +62kiB (+22.35%)
• 🟥 build/module/Lean.Widget.TaggedText//bytes .olean.private: +90kiB (+20.80%)
• 🟥 import Lean//instructions: +29.6M (+1.93%)

Small changes (3✅, 103🟥)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 043b8a765a98b223d0ecef47f076c28aefb57d28 --onto 91bd6e19a7b7aca769f9720e1127c768df0cd2a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-18 22:10:03)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 043b8a765a98b223d0ecef47f076c28aefb57d28 --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-18 22:10:05)

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for 12bfa48 against 043b8a7 are in! @TwoFX

• 🟥 build//instructions: +23.4G (+0.18%)

Large changes (1🟥)

• 🟥 workspaceSymbols//instructions: +623.3M (+2.45%)

Medium changes (3🟥)

• 🟥 build/module/Lake.Util.Cli//bytes .olean: +62kiB (+22.35%)
• 🟥 build/module/Lean.Widget.TaggedText//bytes .olean.private: +90kiB (+20.80%)
• 🟥 import Lean//instructions: +29.2M (+1.90%)

Small changes (3✅, 101🟥)

Too many entries to display here. View the full report on radar instead.