chore: upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas

[kim-em]

To follow, connecting this to Array.insertAt (and renaming).

[ghost]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0e3f26e6df7cd9f82ef932ec39305aa43d4a7c4a --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-05 22:47:52)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4df71ed24f4be25ba0045b4963a03087d2302fa9 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-06 05:37:54)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 196b1e925050bf979ae9312ee69eb5f78d1512c0 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-06 23:29:38)