feat: extend isRelevant

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Arith/IsRelevant.lean

@@ -7,16 +7,26 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
+import Lean.Meta.Tactic.Grind.Arith.Linear.StructId
 public section
 namespace Lean.Meta.Grind.Arith
 
-def isSupportedType (e : Expr) : GoalM Bool := do
-  return isNatType e || isIntType e
+def isSupportedType (α  : Expr) : GoalM Bool := do
+  if isNatType α || isIntType α then
+    return true
+  else if (← Cutsat.getToIntId? α).isSome then
+    return true
+  else if (← Linear.getStructId? α).isSome then
+    return true
+  else
+    return false
 
 partial def isRelevantPred (e : Expr) : GoalM Bool :=
   match_expr e with
   | Not p => isRelevantPred p
   | LE.le α _ _ _ => isSupportedType α
+  | LT.lt α _ _ _ => isSupportedType α
   | Eq α _ _ => isSupportedType α
   | Dvd.dvd α _ _ _ => isSupportedType α
   | _ => return false