chore: fix tests

Author: leodemoura

tests/lean/run/grind_dep_match_overlap.lean

@@ -18,9 +18,3 @@ example (a b : Vec α 2) : h a b = 20 := by
 
 example (a b : Vec α 2) : h a b = 20 := by
   grind (splits := 4) [h.eq_def, Vec]
-
-example (a b : Vec α 2) : h a b = 20 := by
-  grind -offset [h.eq_def, Vec]
-
-example (a b : Vec α 2) : h a b = 20 := by
-  grind -offset (splits := 4) [h.eq_def, Vec]

tests/lean/run/grind_fun_singleton.lean

@@ -39,6 +39,3 @@ example [Inhabited α] : ((fun (_ : α) => x = a + 1) = fun (_ : α) => True) 
 
 example : c = 5 → ((fun (_ : Nat × Nat) => { down := a + c = b + 5 : ULift Prop }) = fun (_ : Nat × Nat) => { down := c < 10 : ULift Prop }) → a = b := by
   grind
-
-example : c = 5 → ((fun (_ : Nat × Nat) => { down := a + c = b + 5 : ULift Prop }) = fun (_ : Nat × Nat) => { down := c < 10 : ULift Prop }) → a = b := by
-  grind -offset

tests/lean/run/grind_match_eq_propagation.lean

@@ -73,9 +73,6 @@ def h (v w : Vec α n) : Nat :=
 example : h a b > 0 := by
   grind [h.eq_def]
 
-example : h a b > 0 := by
-  grind -offset [h.eq_def]
-
 -- TODO: introduce casts while instantiating equation theorems for `h.match_1`
 -- example (a b : Vec α 2) : h a b = 20 := by
 --  unfold h

tests/lean/run/grind_order_2.lean

@@ -1,13 +1,13 @@
 open Lean Grind
 
 example (a b : Nat) (h : a + b > 5) : (if a + b ≤ 2 then b else a) = a := by
-  grind -linarith -lia -offset (splits := 0)
+  grind -linarith -lia (splits := 0)
 
 example (a b c : Nat) : a ≤ b → b ≤ c → c < a → False := by
-  grind -linarith -lia -offset (splits := 0)
+  grind -linarith -lia (splits := 0)
 
 example (a b : Nat) : a ≤ 5 → b ≤ 8 → a > 6 ∨ b > 10 → False := by
-  grind -linarith -lia -offset (splits := 0)
+  grind -linarith -lia (splits := 0)
 
 example (a b c d : Nat) : a ≤ b → b ≤ c → c ≤ d → a ≤ d := by
-  grind -linarith -lia -offset (splits := 0)
+  grind -linarith -lia (splits := 0)

tests/lean/run/grind_order_eq.lean

@@ -11,22 +11,22 @@ example (a b : Int) (f : Int → Int) : a ≤ b + 1 → b ≤ a - 1 → f a = f
   grind -mbtc -lia -linarith (splits := 0)
 
 example (a b : Nat) (f : Nat → Int) : a ≤ b + 1 → b + 1 ≤ a → f a = f (1 + b + 0) := by
-  grind -offset -mbtc -lia -linarith (splits := 0)
+  grind -mbtc -lia -linarith (splits := 0)
 
 example (a b : Nat) (f : Nat → Int) : a ≤ b + 1 → b + 1 ≤ c → c ≤ a → f a = f c := by
-  grind -offset -mbtc -lia -linarith (splits := 0)
+  grind -mbtc -lia -linarith (splits := 0)
 
 example (a b : Nat) (f : Nat → Int) : a ≤ b + 1 → b + 1 ≤ a → f (1 + a) = f (1 + b + 1) := by
-  grind -offset -mbtc -lia -linarith (splits := 0)
+  grind -mbtc -lia -linarith (splits := 0)
 
 example
     : 2*n_1 + a = 1 → 2*n_1 + a = n_2 + 1 → n = 1 → n = n_3 + 1 → n_2 ≠ n_3 → False := by
-  grind -lia -linarith -offset -ring (splits := 0)
+  grind -lia -linarith -ring (splits := 0)
 
 example
     : a = b → a ≤ b + 1 := by
-  grind -lia -linarith -offset -ring (splits := 0) only
+  grind -lia -linarith -ring (splits := 0) only
 
 example
     : a = b + 1 → a ≤ b + 2 := by
-  grind -lia -linarith -offset -ring (splits := 0) only
+  grind -lia -linarith -ring (splits := 0) only

tests/lean/run/grind_order_issue.lean

@@ -99,7 +99,7 @@ attribute [local grind] getIdx findIdx insert
 
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
-  grind -offset -ring -linarith -lia =>
+  grind -ring -linarith -lia =>
     instantiate only [= getElem_def, insert]
     cases #f590
     next =>
@@ -114,7 +114,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
 
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
-  grind -offset -ring -linarith -lia =>
+  grind -ring -linarith -lia =>
     instantiate only [= getElem_def, insert]
     cases #f590
     next =>