chore: avoid declaring duplicate instances LE String and LT String

[TwoFX]

Since forever, mathlib has declared LE String and LT String instances which are propositionally, but not definitionally, equal to the LE String and LT String instances that have shipped with core. This regularly leads to problems with automation that expects instances to be canonical, most recently as described in leanprover/lean4#13544.

This PR demotes the mathlib instances to definitions, and redefines the LinearOrder String instance to use the core-provided instances rather than the ones defined in mathlib. It also redeclares the theorems String.lt_iff_toList_lt and String.le_iff_toList_le to be about the core-provided instances rather than the mathlib ones, and the theorems about the mathlib instances are now called String.lt_iff_toList_lt' and String.le_iff_toList_le'.

Deprecating the material related to the mathlib instances would be a logical next step, but it might make sense to wait with this until core ships more API for LE String and LT String (right now it ships none).

---

[github-actions]

PR summary 15ab76c080

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ le_iff_not_lt
+ le_iff_toList_le'
+ lt_iff_toList_lt'

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[eric-wieser]

My guess would be that until core (or this PR) ships s₁ ≤ s₂ ↔ s₁.toList ≤ s₂.toList about the core instances as a lemma, we do not want this change.