feat: refactor of find functions on List/Array/Vector

[kim-em]

This PR makes the signatures of find functions across List/Array/Vector consistent. Verification lemmas will follow in subsequent PRs.

We were previously quite inconsistent about the signature of indexOf/findIdx functions across List and Array. Moreover, there are still quite large gaps in the verification lemma coverage for these even at the List level.

My intention is to make the signatures consistent by providing: findIdx / findIdx? / findFinIdx? (these all take a predicate, and return respectively a Nat, Option Nat, Option (Fin l.length)) and similarly idxOf / idxOf? / finIdxOf? (which look for an element) for each of List/Array/Vector. I've seen enough examples by now where each variant is genuinely the most convenient at the call-site, so I'm going to accept the cost of having many closely related functions. Hopefully for the verification lemmas we can simp all of these into "projections" of the Option (Fin l.length) versions, and then only have to specify that.

However, I will not plan on immediately either filling in the missing verification lemmas (or even deciding what the simp normal forms relating these operations are), and just reach parity amongst List/Array/Vector for what is already there.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9b5fadd2759f4511f9fddb88009edf4b21c70aad --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 02:08:51)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 07e2b7d913834c068cc5f271accfa3fcb43ba47a --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 02:41:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 08ec2541c755b8797c09766ea55b4d7bc19e3526 --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 07:37:42)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 61c843a3c7541bed30a4302aa8ab23cf98bd279c --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 23:31:14)

[kim-em]

I'd like to test Mathlib, but as this has conflicts with #6800 I'll need to wait for the next nightly.

[kim-em]

Changed my mind, this is blocking stuff, I will just fix Mathlib tonight.