Quantifier Instantiation with Grind

Stream: lean4

[Siddharth Bhat]

I'm trying to get grind to instantiate variables, but I'm not sure what the syntax for doing this is! MWE I'm trying to improve:

axiom X : Type
axiom f : X → X → X
axiom fid : X


@[grind] axiom f_fid : ∀ (x : X), f fid x = x

@[grind] axiom fid_f : ∀ (x : X), f x fid = x

theorem foo (x : X) (hx : ∀ y, f y x = y) : x = fid := by
  fail_if_success grind -- I want this to succeed.
  have := hx fid -- ... but I need to do this to instantiate 'hx' at 'fid'.
  grind [f_fid]

Can someone tell me how to get grind to instantiate hx with all known X constants?
This is extracted from some generic bicategorical situation that I'm trying to grind away.

Alternatively, can I be told that grind does not plan to perform quantifier instantiation? :D

[Joachim Breitner]

Judging from
https://pr-451--lean-reference-manual-review.netlify.app/The--grind--tactic/What-is--grind-___/#The-Lean-Language-Reference--The--grind--tactic--What-is--grind-___ and the following section I’d say grind does not perform quantifier instantiation (at least not in an exploratory way)

[Siddharth Bhat]

Aha, thank you for (1) showing me how to access the reference manual of nightly lean, and (2) for pointing me to the right place!