refactor: clean up public API around `Array.eraseIdx`

[timotree3]

• Removes the public definitions Array.eraseIdxAux and Array.eraseIdxSzAux which were implementation details.
  • Motivation: Array.eraseIdxAux and Array.eraseIdxSzAux were clearly not intended to remain public, but simply making them private would make it inconvenient to unfold them when writing proofs in Std.
• Adds documentation comments to the public Array.eraseIdx-related definitions which remain.
• Removes Array.eraseIdx' which was just Array.feraseIdx wrapped in a subtype and adds Array.size_feraseIdx to prove the subtype property as a standalone theorem.

Co-Authored-By: Daniel Windham [email protected]

[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 612d97440b4c0b3da967eaf041687b0f2c468f3a --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 05:02:05)

[timotree3]

awaiting-review

[Seppel3210]

BTW porting over the lemma from my std4 PR leanprover/std4#690 was pretty easy: https://github.com/Seppel3210/std4/commit/109c3ce97e182813a166c9b55418d9a599a01bb6 So this is definitely bug free :smile:

I also think this makes the API nicer