feat: add iff theorem for List.toArray equality

[raphael-solace]

This PR adds List.toArray_eq_toArray_iff, the iff-shaped theorem for injectivity of List.toArray, while keeping the existing one-way List.toArray_inj theorem for compatibility.

The new theorem follows the usual iff naming shape and is marked [simp], so goals comparing two List.toArray expressions simplify back to list equality.

Addresses #13095.

[raphael-solace]

changelog-library

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7f13a8988f0018f404d4bb0954f95122b8855084 --onto 2cd98639c40d2d2a026dd599093b70f55f55ffaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-25 13:16:10)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7f13a8988f0018f404d4bb0954f95122b8855084 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-25 13:16:12)

[Rob23oba]

example (a b : List Nat) : a.toArray = b.toArray ↔ a = b := by simp

actually already works, via Array.mk.injEq. Also if you want to change anything, List.toArray_inj has the wrong name, _inj should be used for the iff theorems, so I'd instead promote List.toArray_inj to an iff theorem like this:

theorem toArray_inj {as bs : List α} : as.toArray = bs.toArray ↔ as = bs := by simp