fix(Data/List/Lex): remove duplicate List.LE instance

[vihdzp]

Mathlib currently duplicates the Lean core instance for ≤ in lists in an incompatible way. We delete this duplicate instance.

See Zulip.

---

This is a very quick and dirty fix. Core Lean provides all of the theorems we need to prove ≤ forms a linear order, but it provides them in terms of Std relation typeclasses which currently see no use in Mathlib. I've added the instances that were required to get the list theorems working. In the future, we really ought to unify the core and Mathlib relation typeclasses.

[github-actions]

PR summary 4c53273848

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance [LinearOrder α] : @Std.Antisymm α (¬ · < ·)
+ instance [LinearOrder α] : @Std.Total α (¬ · < ·)
+ instance [LinearOrder α] : @Trans α α α (¬ · < ·) (¬ · < ·) (¬ · < ·)
+ instance [Preorder α] : @Std.Asymm α (· < ·) := ⟨fun _ _ ↦ lt_asymm⟩
+ instance [Preorder α] : @Std.Irrefl α (· < ·) := ⟨lt_irrefl⟩
- LE'
- LT'
- isStrictTotalOrder

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).