feat: add Sym.simp theorem set attributes

Add `register_sym_simp_attr` command for creating named Sym.simp theorem
sets with associated attributes. Each set gets its own
`SymSimpExtension` (persistent environment extension).

When a proposition is tagged, it is added as a rewrite theorem.
When a definition is tagged, its equation theorems are added.

New files:
- `Sym/Simp/Attr.lean`: `mkSymSimpAttr`, `registerSymSimpAttr`
- `Sym/Simp/RegisterCommand.lean`: `register_sym_simp_attr` macro
- `tests/pkg/sym_simp_attr/`: package test exercising the attribute
9 files changed