chore: update syntax in grind_ite example (#8475)

Author: kim-em

tests/lean/run/grind_ite.lean

@@ -66,7 +66,7 @@ def vars : IfExpr → List Nat
 /--
 A helper function to specify that two lists are disjoint.
 -/
-@[grind] def _root_.List.disjoint {α} [DecidableEq α] : List α → List α → Bool
+def _root_.List.disjoint {α} [DecidableEq α] : List α → List α → Bool
   | [], _ => true
   | x::xs, ys => x ∉ ys && xs.disjoint ys
 
@@ -150,13 +150,13 @@ def normalize (assign : Std.HashMap Nat Bool) : IfExpr → IfExpr
   termination_by e => e.normSize
 
 -- We tell `grind` to unfold our definitions above.
-attribute [local grind] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars eval
+attribute [local grind] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars eval List.disjoint
 
 theorem normalize_spec (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → ¬ v ∈ assign := by
-  fun_induction normalize <;> grind (gen := 7)
+  fun_induction normalize with grind (gen := 7)
 
 -- We can also prove other variations, where we spell "`v` is not in `assign`"
 -- different ways, and `grind` doesn't mind.
@@ -165,13 +165,13 @@ example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign.contains v = false := by
-  fun_induction normalize <;> grind (gen := 7)
+  fun_induction normalize with grind (gen := 7)
 
 example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign[v]? = none := by
-  fun_induction normalize <;> grind (gen := 8)
+  fun_induction normalize with grind (gen := 8)
 
 /--
 We recall the statement of the if-normalization problem.
@@ -207,18 +207,18 @@ theorem normalize'_spec (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
     (normalize' assign e).normalized
     ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → ¬ v ∈ assign := by
-  fun_induction normalize' <;> grind (gen := 7)
+  fun_induction normalize' with grind (gen := 7)
 
 example (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
     (normalize' assign e).normalized
     ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign.contains v = false := by
-  fun_induction normalize' <;> grind (gen := 7)
+  fun_induction normalize' with grind (gen := 7)
 
 example (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
     (normalize' assign e).normalized
     ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign[v]? = none := by
-  fun_induction normalize' <;> grind (gen := 8)
+  fun_induction normalize' with grind (gen := 8)
 
 end IfExpr