chore: extend GetElem with getElem! and getElem?

[joehendrix]

This makes changes to the GetElem class so that it does not lead to unnecessary overhead in container like RBMap.

The changes are to:

1. Make getElem? and getElem! part of the GetElem class so they can be overridden in instances.
2. Introduce a LawfulGetElem class that contains correctness theorems for getElem? and getElem! using the original definitions.
3. Reorganize definitions (e.g, by moving GetElem out of Init.Prelude) so that the GetElem changes are feasible.
4. Provide LawfulGetElem instances to complement all existing GetElem instances in Lean core.

To reduce the size of the PR, this doesn't do the work of providing new GetElem instances for RBMap, HashMap etc. That will be done in a separate PR (#3688) that depends on this.

[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 4e3a8468c351531235ba5cffd5566b7283b7a8ca --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-15 17:51:16)
• 💥 Mathlib branch lean-pr-testing-3694 build failed against this PR. (2024-03-15 21:08:58) View Log
• 💥 Mathlib branch lean-pr-testing-3694 build failed against this PR. (2024-03-17 21:50:35) View Log
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2d18eff544093882d45b7e1e97a0876247324f2b --onto 8e96d7ba1d7a36c7160112ef12307e4f361e8c3b. (2024-03-17 22:41:24)

[joehendrix]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5a14080.
There were no significant changes against commit 2d18eff.

[david-christiansen]

Suggested change

	* `arr[i]!`: panics if the side goal is false
	* `arr[i]!`: panics if the side goal is false using `getElem!` in this class

[david-christiansen]

But I think actually it just expands to getElem!, which is intended to panic when the value isn't there, right? That is, the side goal is not checked anymore? In that case,

Suggested change

	* `arr[i]!`: panics if the side goal is false
	* `arr[i]!`: invokes `GetElem.getElem!`, which panics if the index is not found

[david-christiansen]

Suggested change

	* `arr[i]?`: returns `none` if the side goal is false
	* `arr[i]?`: expands to `GetElem.getElem?`, which returns `none` if the index is not found

[joehendrix]

Thanks. I've tried to clarify