discrepancy between `grind` and `grind => instantiate`

Stream: lean4

[Albert Smith]

In the following scenario, there is a difference between the behaviour of grind [...] and grind => instantiate [...]; finish:

structure Alice (x : Nat) : Prop where
structure Bob (x : Nat) : Prop where

theorem alice_0 : Alice 0 := ⟨⟩
theorem Alice.toBob {x} : Alice x → Bob x := fun ⟨⟩ => ⟨⟩

theorem blob : Bob 0 := by grind [alice_0, → Alice.toBob] -- works
theorem clob : Bob 0 := by grind => instantiate [alice_0, → Alice.toBob] -- doesnt

As far as I'm aware there aren't currently claims made about the behaviour of instantiate, so this isn't really a "bug". But it would be nice for proof development to be able to do whatever the first grind is doing in interactive mode somehow.

[Albert Smith]

:duck: after some more experimentation I guess (without having actually read the code) that what the first grind does is more like repeat instantiate, and indeed repeat instantiate works. Good enough for me, although it would be nice to have a short alias for this for interactive proof development.