test: beta reduction tests for `grind`

tests/lean/run/grind_beta.lean

diff --git a/tests/lean/run/grind_beta.lean b/tests/lean/run/grind_beta.lean
new file mode 100644
index 0000000..6e24e05
--- /dev/null
+++ b/tests/lean/run/grind_beta.lean
@@ -0,0 +1,72 @@
+def f (x : Nat) : Nat → Nat → Nat :=
+  match x with
+  | 0 => fun _ _ => 0
+  | _+1 => fun a b => a + b
+
+example : f 0 b c = 0 := by
+  grind [f]
+
+example : f (a+1) b c = b + c := by
+  grind [f]
+
+example : f x b c ≠ b + c → x = a + 1 → False := by
+  grind [f]
+
+example : x = a + 1 → f x b c ≠ b + c → False := by
+  grind [f]
+
+example : x = a + 1 → f x b c ≠ b + c → False := by
+  grind [f]
+
+example : f x b c > 0 → x = 0 → False := by
+  grind [f]
+
+example : f x b c > 0 → x ≠ 0 := by
+  grind [f]
+
+example (f : Nat → Nat → Nat) : f 2 3 ≠ 5 → f = (fun x y : Nat => x + y) → False := by
+  grind
+
+opaque bla : Nat → Nat → Nat → Nat
+
+/--
+info: [grind.beta] f 2 3 = bla 2 3 2, using fun x y => bla x y x
+[grind.beta] f 2 3 = 2 + 3, using fun x y => x + y
+-/
+#guard_msgs (info) in
+set_option trace.grind.beta true in
+example (g h f : Nat → Nat → Nat) :
+        f 2 3 ≠ 5 →
+          g = (fun x y : Nat => x + y) →
+          h = (fun x y => bla x y x) →
+          g = h →
+          f = h →
+          False := by
+  grind
+
+example (g h f : Nat → Nat → Nat) :
+        f 2 3 ≠ 5 →
+          h = (fun x y => bla x y x) →
+          g = (fun x y : Nat => x + y) →
+          g = h →
+          h = f →
+          False := by
+  grind
+
+
+example (f : Nat → Nat → Nat) : f = (fun x y : Nat => x + y) → f 2 3 = 5 := by
+  grind
+
+example (f g h : Nat → Nat → Nat) :
+          h = (fun x y => bla x y x) →
+          g = (fun x y : Nat => x + y) →
+          g = h →
+          h = f →
+          f 2 3 = 5 := by
+  grind
+
+example (f : Nat → Nat) : f = (fun x : Nat => x + 5) → f 2 > 5 := by
+  grind
+
+example (f : Nat → Nat → Nat) : f a = (fun x : Nat => x + 5) → f a 2 > 5 := by
+  grind