fix: Add missing csimp lemma

[linesthatinterlace]

trafficstars

Addresses issue batteries#307.

Closes #307

[linesthatinterlace]

This will require changes to Mathlib - specifically, List.sublists_eq_sublistsFast should be removed. Embarrassingly I can't remember how to do this properly.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch batteries-pr-testing-1491 build failed against this PR. (2025-11-03 18:41:36) View Log
• 💥 Mathlib branch batteries-pr-testing-1491 build failed against this PR. (2025-11-03 22:04:51) View Log
• 💥 Mathlib branch batteries-pr-testing-1491 build failed against this PR. (2025-11-03 23:00:03) View Log
• 💥 Mathlib branch batteries-pr-testing-1491 build failed against this PR. (2025-11-04 09:50:07) View Log
• ✅ Mathlib branch batteries-pr-testing-1491 has successfully built against this PR. (2025-11-04 11:32:25) View Log
• 🟡 Mathlib branch batteries-pr-testing-1491 build against this PR was cancelled. (2025-11-06 22:50:17) View Log
• ✅ Mathlib branch batteries-pr-testing-1491 has successfully built against this PR. (2025-11-06 23:55:00) View Log

[linesthatinterlace]

I am not sure about the new lemma in ‎Batteries/Data/Array/Init/Lemmas.lean, but I cannot see where else it would be appropriate to add this lemma.

[linesthatinterlace]

I managed to do it without needing the new lemma and now the proof is very smooth.

[fgdorais]

Please create an adaptation PR on Mathlib from the testing branch.