chore: remove unused lemmas from a non-terminal simp

[kim-em]

These non-terminal simp calls broke on a branch, but can be fixed on both master and that branch by removing a lemma.

[leanprover-community-mathlib4-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 db3631ba1f98891c6db02c46a2b691b6af618648 --onto d31066646dfa7389d818a2e2e1493be6a941924e. (2024-09-02 06:37:41)