feat: List.mergeSort

[kim-em]

Defines mergeSort, a naive stable merge sort algorithm, replaces it via a @[csimp] lemma with something faster at runtime, and proves the following results:

• mergeSort_sorted: mergeSort produces a sorted list.
• mergeSort_perm: mergeSort is a permutation of the input list.
• mergeSort_of_sorted: mergeSort does not change a sorted list.
• mergeSort_cons: proves mergeSort le (x :: xs) = l₁ ++ x :: l₂ for some l₁, l₂
  so that mergeSort le xs = l₁ ++ l₂, and no a ∈ l₁ satisfies le a x.
• mergeSort_stable: if c is a sorted sublist of l, then c is still a sublist of mergeSort le l.

[kim-em]

I am really trying hard to resist the temptation to state the result that "forgetting it is sorted" and "stable merge sort" form a Galois connection between sorted lists and lists, with the <+ (sublist) partial order.

[kim-em]

This PR will need to wait for me to verify that #5088 doesn't have any bad performance implications.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5092 build failed against this PR. (2024-08-19 11:10:18) View Log
• 💥 Mathlib branch lean-pr-testing-5092 build failed against this PR. (2024-08-20 01:33:36) View Log
• 💥 Mathlib branch lean-pr-testing-5092 build failed against this PR. (2024-08-20 02:11:41) View Log

[kim-em]

This is expected to break Mathlib as there is a (non-tail-recursive, non-stable) implementation of mergeSort there. I'll clean it up after this is merged.