Over eager simplification of Array.drop

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

Simp simplifies (Array.drop xs n).toList to List.take (xs.size - n) (List.drop n xs.toList). This is self evidently a bad simplification, the List.take is totally superfluous.

The offending simp lemma is, in my view, Array.drop_eq_extract. Neither List.drop_eq_extract nor List.take_eq_extract are simp lemmas, and their array counterparts likely should not be either.

Instead, I believe core should provide Array.toList_take and Array.toList_drop which should be simp lemmas.

Context

This came up in one of my PRs to Batteries.

Zulip

Steps to Reproduce

example : (Array.drop as n).toList = List.take (as.size - n) (List.drop n as.toList) := by
  simp

Expected behavior: Array.drop as n).toList simplifies to List.drop n as.toList

Actual behavior: it instead simplifies to List.take (as.size - n) (List.drop n as.toList)

Versions

Lean 4.29.0-nightly-2026-02-03
Target: x86_64-unknown-linux-gnu

Impact

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

Start with the minimal Array.drop reproduction and inspect the named Array.drop_eq_extract simp lemma. Compare its behavior with the stated List.drop and List.take cases, then verify that simplification produces List.drop n as.toList rather than the redundant List.take expression.