feat: suggestions for some size/count/length confusions

[robsimmons]

This PR adds suggest_for annotations directing uses of Array.length permanently to Array.size, and uses of String.size permanently to String.length.

[robsimmons]

(Note: only merge after #11554)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 72196169b679949b3a19d6c69b80189562cd5b7f --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-10 14:59:50)

[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 72196169b679949b3a19d6c69b80189562cd5b7f --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force reference manual CI using the force-manual-ci label. (2025-12-10 14:59:52)