feat: upstream lemmas about basic List/Array operations

[kim-em]

This PR upstreams lemmas about List/Array operations already defined in Lean from std/batteries.

Happy to take suggestions about increasing or decreasing scope.

[digama0]

For this and future moves, would it be possible to follow the same protocol we used during the port, and have the initial commit be a plain copy/paste job so that the diffs needed to make it compile (and any additional changes) stand out more clearly?

[kim-em]

For this and future moves, would it be possible to follow the same protocol we used during the port, and have the initial commit be a plain copy/paste job so that the diffs needed to make it compile (and any additional changes) stand out more clearly?

Ah, yes, sorry, I know you've asked this before. I'll try to remember. It's a bit difficult to know where exactly to make that commit here: I initially copy-pasted in the entire files that I was drawing from, and then whittled down as dependencies weren't available or I decided I didn't want something upstreamed.

[digama0]

As long as the diff isn't a complete mess, I think it's okay if the first commit includes the entirety of the affected files and hence subsequent commits contain a lot of red

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e733149134a9fa9e92bc589afbe6c2cbb665835c --onto b470eb522bfd68ca96938c23f6a1bce79da8a99f. (2024-05-03 04:25:49)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e733149134a9fa9e92bc589afbe6c2cbb665835c --onto 00cf5771f31e7de7f6ab3089cb4b9ffa606a35ed. (2024-05-06 03:54:35)