feat: guard against variables in head positions of lhs of simp theorems

[wkrozowski]

This PR adds a check that rejects simp theorems whose left-hand side has a variable as the head symbol (e.g. x = x + 0 or x 0 = x 0 + 0). Such theorems cause the simplifier to loop or match everything, since the head symbol is unconstrained. The check applies to both @[simp] and attribute [simp ←].

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f7ec39d6a164820200fc971fe675eb02e6b30591 --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-02 15:36:28)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f7ec39d6a164820200fc971fe675eb02e6b30591 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-02 15:36:30)