Refactor shared simp only with custom tactics

[andrewmwells-amazon]

Category

Lean formalization

Describe the feature you'd like to request

As pointed out here #278 (comment) there are many almost identical simp only instances we could rewrite more cleanly with a custom tactic.

Describe alternatives you've considered

N/A

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change

[andrewmwells-amazon]

From a Zulip thread:
We should import

import Lean.Elab.Tactic.Simp

register_simp_attr bv_normalize

then add

@[bv_normalize]

before the defs in question and then

simp only [bv_normalize]

will do what we want.