chore: grind test file demonstrating interactive use (#12114)

tests/lean/run/grind_interactive_2.lean

@@ -0,0 +1,30 @@
+import Lean.LibrarySuggestions.Default
+
+theorem sq_inj (x y : Nat) (h : x ^ 2 = y ^ 2) : x = y := by
+  -- Puzzle for anyone bored: a quick Mathlib-free proof?
+  sorry
+
+example (a b c d e : Nat) (_ : a = b) (_ : b = c) (_ : c ^ 2 = d ^ 2) (_ : d = e) : a = e := by
+  grind =>
+    -- We can verify that `grind` can see certain facts:
+    have : a = c
+    -- We can ask for all the known equivalence classes,
+    -- or classes involving certain terms:
+    show_eqcs a
+    -- We can add additional facts, giving proofs inline.
+    have : c = d := by grind? +suggestions
+    -- These facts are automatically used to extend equivalence classes,
+    -- so in this case the `have` statement itself closes the goal.
+
+example (a b c d e : Nat) (_ : a = b) (_ : b = c) (_ : c ^ 2 = d ^ 2) (_ : d = e) : a = e := by
+  grind [sq_inj]
+
+example (x y : Rat) (_ : x^2 = 1) (_ : x + y = 1) : y ≤ 2 := by
+  fail_if_success grind
+  grind =>
+    -- We can also use `have` statements as clues to guide `grind`.
+    have : x = 1 ∨ x = -1
+    -- Here `grind` can both prove the `have` statement (via a Grobner argument)
+    -- and finish off afterwards (using linear arithmetic),
+    -- even though it can't close the original goal by itself.
+    finish