feat: user attribute at `grind_pattern`

This PR implements support for user-defined attributes at
`grind_pattern`. Suppose we have `register_grind_attr my_grind`. Then,
we can now write

```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
axiom fg : g (f x) = x

grind_pattern [my_grind] fg => g (f x)
```