feat: [grind_eq] attribute for the grind tactic

[leodemoura]

This PR introduces the [grind_eq] attribute, designed to annotate equational theorems and functions for heuristic instantiations in the grind tactic.
When applied to an equational theorem, the [grind_eq] attribute instructs the grind tactic to automatically use the annotated theorem to instantiate patterns during proof search. If applied to a function, it marks all equational theorems associated with that function.

@[grind_eq]
theorem foo_idempotent : foo (foo x) = foo x := ...

@[grind_eq] def f (a : Nat) :=
  match a with
  | 0 => 10
  | x+1 => g (f x)

In the example above, the grind tactic will add instances of the theorem foo_idempotent to the local context whenever it encounters the pattern foo (foo x). Similarly, functions annotated with [grind_eq] will propagate this annotation to their associated equational theorems.

[leanprover-community-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 fd091d1dfe03b821ac2888921dfe7d13b6096b4a --onto dc5c8097b5ca053dd49b5de246add54c3e999734. (2025-01-05 20:54:51)