feat: add [grind cases eager] Subtype

This PR adds `[grind cases eager]` attribute to `Subtype`. See new
test.

src/Init/Grind/Cases.lean

@@ -7,5 +7,5 @@ prelude
 import Init.Core
 import Init.Grind.Tactics
 
-attribute [grind cases eager] And Prod False Empty True Unit Exists
+attribute [grind cases eager] And Prod False Empty True Unit Exists Subtype
 attribute [grind cases] Or

tests/lean/run/grind_cutsat_auto.lean

@@ -80,3 +80,9 @@ example (x y z : Int) :
     -5 ≤  3*x - 11*y +  2*z →  3*x - 11*y +  2*z ≤ -1 →
     10 ≤  8*x +  9*y -  4*z →  8*x +  9*y -  4*z ≤ 12 → False := by
   grind
+
+example (x y : Int) (h : x < y) (z : { z : Int // y ≤ z ∧ z ≤ x }) : False := by
+  grind
+
+example (x y : Int) (h : x < y) (z : { z : Int // y ≤ z ∧ z ≤ x }) : Nat := by
+  grind