fix: theorem instantiation in grind

[leodemoura]

This PR fixes a bug in the theorem instantiation procedure in the (WIP) grind tactic. For example, it was missing the following instance in one of the tests:

[grind.ematch.instance] Array.get_set_ne: ∀ (hj : i < bs.size), j ≠ i → (bs.set j w ⋯)[i] = bs[i]

This PR also renames the grind base monad to GrindCoreM.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-01-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2025-01-01 17:25:21)