chore: BitVec.Lemmas - drop non-terminal simps

[tobiasgrosser]

BitVec.Lemmas contained a couple of non-terminal simps. We turn non-terminal simp$, simp [, and simp at expressions into simp only to improve code maintainability.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ef71f0beabddd0dd272ea55e294d1f2535408195 --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-28 05:43:31)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ef71f0beabddd0dd272ea55e294d1f2535408195 --onto 9460f79d28d3a72d7484766b5f2c83362e91dd5b. (2024-09-28 09:27:23)

[hargoniX]

Is this PR supposed to address all of them or only the ones seen here? If it is all of them, did you verify with e.g. grep simp | grep -v "simp only" that you got all of them?

[tobiasgrosser]

Is this PR supposed to address all of them or only the ones seen here? If it is all of them, did you verify with, e.g., grep simp | grep -v "simp only" that you got all of them?

I searched now for simp$, simp [, and simp at and manually verified that they are terminal. While this was manual, I tried to be careful to catch all.