perf: remove simp annotations

[TwoFX]

This PR removes most of the simp annotations added in #12945, to mitigate the performance impact. The lemmas remain.

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for 9112376 against 61a3443 are in. Significant changes detected! @TwoFX

• ✅ build//instructions: -29.8G (-0.24%)

Medium changes (6✅)

• ✅ build/module/Init.Data.Array.Attach//instructions: -1.6G (-11.85%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Int.Linear//instructions: -1.5G (-4.68%)
• ✅ build/module/Init.Data.List.Find//instructions: -1.2G (-4.91%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Range.Polymorphic.Lemmas//instructions: -2.6G (-4.73%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Vector.Lemmas//instructions: -1.2G (-2.27%) (reduced significance based on absolute threshold)
• ✅ misc/import Init.Data.List.Sublist//instructions: -133.6M (-1.22%)

Small changes (108✅)

Too many entries to display here. View the full report on radar instead.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-19 08:27:40)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-12977 build failed against this PR. (2026-03-19 09:03:20) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12977 has successfully built against this PR. (2026-03-19 10:09:36) View Log