`List.toArray_inj` has incorrect statement

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

By our naming convention, List.toArray_inj should be l1.toArray = l2.toArray <-> l1 = l2, but it is something different.

Versions

nightly-2026-03-24

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Search the Lean source for the List.toArray_inj declaration and inspect its current statement. Reproduce the reported mismatch against the nightly release, then verify that the declaration expresses the expected equivalence and that the relevant Lean checks pass.