Getting a proof term out of `grind`

Stream: lean4

[Wrenna Robson]

I have the following.

theorem blahj {a b : Fin 2} (hab : a < b) : a = 0 ∧ b = 1 := by grind

I would like to understand what grind is using for this. How do I do this?

[Wrenna Robson]

Ah I think it might be using cutsat?

[Ruben Van de Velde]

Not yet, but it will come

[Wrenna Robson]

Fair.

[Bhavik Mehta]

You can see the proof term like this:

theorem blahj {a b : Fin 2} (hab : a < b) : a = 0 ∧ b = 1 := by
  grind -abstractProof

#print blahj