Commit 2026-06-02 15:39 7ecb01bd

chore: avoid declaring duplicate instances LE String and LT String (#39003) 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 removes the mathlib instances, 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. The result relating ltb (String.Legacy.iter s₁) (String.Legacy.iter s₂) (the previous implementation) to s₁ < s₂ is now packaged as String.lt_iff_ltb.