fix: E-matching patterns containing ground universe polymorphic patterns in grind

[leodemoura]

This PR ensures grind can E-match patterns containing universe polymorphic ground sub-patterns. For example, given

set_option pp.universes true in
attribute [grind?] Id.run_pure

the pattern

Id.run_pure.{u_1}: [@Id.run.{u_1} #1 (@pure.{u_1, u_1} `[Id.{u_1}] `[Applicative.toPure.{u_1, u_1}] _ #0)]

contains two nested universe polymorphic ground patterns

• Id.{u_1}
• Applicative.toPure.{u_1, u_1}

This kind of pattern is not common, but it occurs in core.

[ghost]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5abf4bb651329452deb16496845f8937b1bbc270 --onto e0fcaf5e7ddab2fcab51be8c403446d84a8a0d45. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-11 21:45:43)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5abf4bb651329452deb16496845f8937b1bbc270 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-08-11 21:45:45)