[Merged by Bors] - feat: stability of List.insertionSort

[marcusrossel]

The statements of stability follow those used for mergeSort in leanprover/lean4#5092.

---

This PR is a result of this discussion on Zulip, where @semorrison recommended we verify that List.insertionSort is stable.

[github-actions]

PR summary cbd44d5495

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Sublist.orderedInsert_sublist
+ cons_sublist_orderedInsert
+ pair_sublist_insertionSort
+ pair_sublist_insertionSort'
+ sublist_insertionSort
+ sublist_insertionSort'

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.

[kim-em]

Otherwise LGTM!

[marcusrossel]

I've added the stability theorems based on <+~, as well as the additional lemma orderedInsert_sublist.

[marcusrossel]

Also, leanprover/lean4-nightly@6d0b008 adds Pairwise.erase, which I would use on Line 425. Should I add a TODO indicating that this should be changed once Mathlib uses the next release, or is this not important enough?

[Ruben-VandeVelde]

And please add the TODO, yes

[marcusrossel]

I've changed the theorem names as to align with leanprover/lean4#5242

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style