From eccc472e8dd2d0b488a10ed3a9adb9805da9d7c2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 11 Jun 2025 15:09:19 +1000
Subject: [PATCH] chore: remove set_option grind.warning false (#8714)

This PR removes the now unnecessary `set_option grind.warning false`
statements, now that the warning is disabled by default.
---
 src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean           | 2 --
 src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean                  | 2 --
 src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean               | 2 --
 src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean       | 2 --
 src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean | 2 --
 src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean  | 2 --
 src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean | 2 --
 src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean  | 1 -
 src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean     | 2 --
 tests/lean/grind/experiments/list.lean                          | 2 --
 tests/lean/grind/experiments/map.lean                           | 2 --
 tests/lean/grind/experiments/option.lean                        | 2 --
 tests/lean/grind/grind_lrat_internal_error.lean                 | 2 --
 tests/lean/grind/grind_palindrome.lean                          | 2 --
 tests/lean/grind/ordered_modules.lean                           | 2 --
 tests/lean/grind/sublist.lean                                   | 2 --
 tests/lean/run/grind_abstract_mvars.lean                        | 2 --
 tests/lean/run/grind_append_issue.lean                          | 2 --
 tests/lean/run/grind_array.lean                                 | 2 --
 tests/lean/run/grind_bintree.lean                               | 1 -
 tests/lean/run/grind_bool_diseq.lean                            | 2 --
 tests/lean/run/grind_bool_prop.lean                             | 1 -
 tests/lean/run/grind_casting_issue.lean                         | 1 -
 tests/lean/run/grind_cat.lean                                   | 2 --
 tests/lean/run/grind_clear_error.lean                           | 2 --
 tests/lean/run/grind_congr.lean                                 | 2 --
 tests/lean/run/grind_congr_hash_issue.lean                      | 1 -
 tests/lean/run/grind_constProp.lean                             | 2 --
 tests/lean/run/grind_const_pattern.lean                         | 1 -
 tests/lean/run/grind_countP.lean                                | 1 -
 tests/lean/run/grind_cutsat_auto.lean                           | 2 --
 tests/lean/run/grind_cutsat_cooper.lean                         | 2 --
 tests/lean/run/grind_cutsat_diseq_1.lean                        | 1 -
 tests/lean/run/grind_cutsat_diseq_2.lean                        | 1 -
 tests/lean/run/grind_cutsat_diseq_3.lean                        | 1 -
 tests/lean/run/grind_cutsat_diseq_cooper.lean                   | 2 --
 tests/lean/run/grind_cutsat_div_1.lean                          | 1 -
 tests/lean/run/grind_cutsat_div_mod.lean                        | 2 --
 tests/lean/run/grind_cutsat_eq_1.lean                           | 1 -
 tests/lean/run/grind_cutsat_le_1.lean                           | 1 -
 tests/lean/run/grind_cutsat_le_2.lean                           | 1 -
 tests/lean/run/grind_cutsat_natCast_propagation.lean            | 2 --
 tests/lean/run/grind_cutsat_nat_dvd.lean                        | 2 --
 tests/lean/run/grind_cutsat_nat_eq.lean                         | 2 --
 tests/lean/run/grind_cutsat_nat_le.lean                         | 2 --
 tests/lean/run/grind_cutsat_omega.lean                          | 2 --
 tests/lean/run/grind_cutsat_tests.lean                          | 2 --
 tests/lean/run/grind_ematch_gen_pattern.lean                    | 2 --
 tests/lean/run/grind_ematch_ground_implicit_inst.lean           | 2 --
 tests/lean/run/grind_ematch_theorem_activation.lean             | 2 --
 tests/lean/run/grind_ematch_type_error.lean                     | 2 --
 tests/lean/run/grind_eq_bwd.lean                                | 2 --
 tests/lean/run/grind_eq_false_of_imp_eq_false.lean              | 1 -
 tests/lean/run/grind_eqres_bug.lean                             | 2 --
 tests/lean/run/grind_eta.lean                                   | 2 --
 tests/lean/run/grind_etaStruct.lean                             | 2 --
 tests/lean/run/grind_exfalso.lean                               | 2 --
 tests/lean/run/grind_fastEraseDups.lean                         | 2 --
 tests/lean/run/grind_funext.lean                                | 2 --
 tests/lean/run/grind_getElem.lean                               | 1 -
 tests/lean/run/grind_getLast_dropLast.lean                      | 2 --
 tests/lean/run/grind_guide.lean                                 | 2 --
 tests/lean/run/grind_hashmap_list.lean                          | 1 -
 tests/lean/run/grind_hcongr.lean                                | 1 -
 tests/lean/run/grind_heapsort.lean                              | 2 --
 tests/lean/run/grind_heartbeats.lean                            | 2 --
 tests/lean/run/grind_indexmap.lean                              | 2 --
 tests/lean/run/grind_indexmap_pre.lean                          | 2 --
 tests/lean/run/grind_ite.lean                                   | 2 --
 tests/lean/run/grind_ite_congr.lean                             | 2 --
 tests/lean/run/grind_ite_split_issue.lean                       | 2 --
 tests/lean/run/grind_ite_unused_match.lean                      | 2 --
 tests/lean/run/grind_linarith_1.lean                            | 2 --
 tests/lean/run/grind_list.lean                                  | 2 --
 tests/lean/run/grind_list2.lean                                 | 1 -
 tests/lean/run/grind_list_count.lean                            | 2 --
 tests/lean/run/grind_list_issue.lean                            | 1 -
 tests/lean/run/grind_list_sublist.lean                          | 2 --
 tests/lean/run/grind_lookahead.lean                             | 1 -
 tests/lean/run/grind_map.lean                                   | 2 --
 tests/lean/run/grind_mark_nested_proofs_bug.lean                | 2 --
 tests/lean/run/grind_match_with_eq.lean                         | 2 --
 tests/lean/run/grind_mbtc_1.lean                                | 2 --
 tests/lean/run/grind_min.lean                                   | 2 --
 tests/lean/run/grind_mvar.lean                                  | 2 --
 tests/lean/run/grind_natCast.lean                               | 2 --
 tests/lean/run/grind_nochrono.lean                              | 2 --
 tests/lean/run/grind_offset_cnstr.lean                          | 1 -
 tests/lean/run/grind_omega_examples.lean                        | 1 -
 tests/lean/run/grind_option.lean                                | 2 --
 tests/lean/run/grind_overapplied_ite.lean                       | 2 --
 tests/lean/run/grind_palindrome2.lean                           | 2 --
 tests/lean/run/grind_panic_invariant.lean                       | 2 --
 tests/lean/run/grind_pre.lean                                   | 1 -
 tests/lean/run/grind_product_eta_and_split.lean                 | 1 -
 tests/lean/run/grind_qsort.lean                                 | 2 --
 tests/lean/run/grind_regression.lean                            | 1 -
 tests/lean/run/grind_ring_1.lean                                | 1 -
 tests/lean/run/grind_ring_2.lean                                | 1 -
 tests/lean/run/grind_ring_3.lean                                | 2 --
 tests/lean/run/grind_ring_4.lean                                | 2 --
 tests/lean/run/grind_sort_eqc.lean                              | 1 -
 tests/lean/run/grind_split_arith_imp.lean                       | 1 -
 tests/lean/run/grind_split_issue.lean                           | 1 -
 tests/lean/run/grind_t1.lean                                    | 2 --
 tests/lean/run/grind_trace.lean                                 | 2 --
 tests/lean/run/grind_trig.lean                                  | 2 --
 tests/lean/run/grind_try_trace.lean                             | 1 -
 tests/lean/run/grind_vector.lean                                | 2 --
 tests/lean/run/simp_arith_issues.lean                           | 2 --
 110 files changed, 188 deletions(-)

diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
index 0b28de5ac7..93b654f551 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
@@ -9,8 +9,6 @@ import Std.Tactic.BVDecide.LRAT.Internal.Entails
 import Std.Tactic.BVDecide.LRAT.Internal.PosFin
 import Init.Grind
 
-set_option grind.warning false
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
index b820087579..b406f898fe 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
@@ -6,8 +6,6 @@ Authors: Josh Clune
 prelude
 import Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
 
-set_option grind.warning false
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
index 041571336c..0e5c67a7a9 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
@@ -12,8 +12,6 @@ import Std.Tactic.BVDecide.LRAT.Internal.PosFin
 import Std.Tactic.BVDecide.LRAT.Internal.Assignment
 import Init.Grind
 
-set_option grind.warning false
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
index 3dfdbdc534..c8fe6209b3 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
@@ -7,8 +7,6 @@ prelude
 import Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
 import Std.Tactic.BVDecide.LRAT.Internal.CNF
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
-
 /-!
 This module contains basic statements about the invariants that are satisfied by the LRAT checker
 implementation in `Implementation`.
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
index f641063b66..cf945ad200 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
@@ -11,8 +11,6 @@ This module contains the implementation of RAT-based clause adding for the defau
 implementation.
 -/
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
index 8b39db4c60..deb97520b9 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
@@ -11,8 +11,6 @@ This module contains the verification of RAT-based clause adding for the default
 implementation.
 -/
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index 6d95ec4adf..f92d46c684 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -11,8 +11,6 @@ This module contains the implementation of RUP-based clause adding for the defau
 implementation.
 -/
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
index 22d7f31a7e..81ab6007d3 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
@@ -11,7 +11,6 @@ This module contains the verification of RUP-based clause adding for the default
 implementation.
 -/
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
index eca52b6683..2a838d05f5 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
@@ -8,8 +8,6 @@ import Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
 import Std.Tactic.BVDecide.LRAT.Internal.CNF
 import Std.Tactic.BVDecide.LRAT.Internal.Actions
 
-set_option grind.warning false
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal
diff --git a/tests/lean/grind/experiments/list.lean b/tests/lean/grind/experiments/list.lean
index e4dddede34..846f58f2b8 100644
--- a/tests/lean/grind/experiments/list.lean
+++ b/tests/lean/grind/experiments/list.lean
@@ -6,8 +6,6 @@ It may still be a good source of ideas for `grind` attributes, or `grind` bugs!
 But it's also fine to just delete it at some point.
 -/
 
-set_option grind.warning false
-
 -- Rejected `grind` attributes:
 -- attribute [grind] List.getElem?_eq_getElem -- This is way too slow, it adds about 30% time to this file.
 -- attribute [grind] List.not_mem_nil -- unnecessary
diff --git a/tests/lean/grind/experiments/map.lean b/tests/lean/grind/experiments/map.lean
index 1480ea3865..6b18625dc7 100644
--- a/tests/lean/grind/experiments/map.lean
+++ b/tests/lean/grind/experiments/map.lean
@@ -1,8 +1,6 @@
 import Std.Data.HashMap
 import Std.Data.DHashMap
 import Std.Data.ExtHashMap
-set_option grind.warning false
-
 open Std
 
 -- Do we want this?
diff --git a/tests/lean/grind/experiments/option.lean b/tests/lean/grind/experiments/option.lean
index 2564c554b4..2118e8791b 100644
--- a/tests/lean/grind/experiments/option.lean
+++ b/tests/lean/grind/experiments/option.lean
@@ -1,7 +1,5 @@
 open Option
 
-set_option grind.warning false
-
 -- TODO: the following lemmas currently fail, but could be solved with some subset of the following attributes:
 -- I haven't added them yet, because the nuclear option of `[grind cases]` is tempting, but a bit scary.
 
diff --git a/tests/lean/grind/grind_lrat_internal_error.lean b/tests/lean/grind/grind_lrat_internal_error.lean
index df50d90272..4c28c60115 100644
--- a/tests/lean/grind/grind_lrat_internal_error.lean
+++ b/tests/lean/grind/grind_lrat_internal_error.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 namespace Std
 namespace Sat
 
diff --git a/tests/lean/grind/grind_palindrome.lean b/tests/lean/grind/grind_palindrome.lean
index 749284c037..9908e3baf3 100644
--- a/tests/lean/grind/grind_palindrome.lean
+++ b/tests/lean/grind/grind_palindrome.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 def IsPalindrome (xs : Array Nat) : Prop := xs.reverse = xs
 
 def checkPalin1 (xs : Array Nat) : Bool :=
diff --git a/tests/lean/grind/ordered_modules.lean b/tests/lean/grind/ordered_modules.lean
index d363a3e84b..13e68baf6b 100644
--- a/tests/lean/grind/ordered_modules.lean
+++ b/tests/lean/grind/ordered_modules.lean
@@ -1,7 +1,5 @@
 open Lean.Grind
 
-set_option grind.warning false
-
 variable (R : Type u) [IntModule R] [NoNatZeroDivisors R] [Preorder R] [IntModule.IsOrdered R]
 
 example (a b c : R) (h : a < b) : a + c < b + c := by grind
diff --git a/tests/lean/grind/sublist.lean b/tests/lean/grind/sublist.lean
index 3210a288be..dc8ce1c773 100644
--- a/tests/lean/grind/sublist.lean
+++ b/tests/lean/grind/sublist.lean
@@ -1,7 +1,5 @@
 open List
 
-set_option grind.warning false
-
 example (h : zs <+ ys) (w : xs ++ ys <+ zs) (h' : ¬xs = []) : False := by
   fail_if_success grind
   -- I'm not sure how to make progress here without manually adding that since `xs ≠ []`, it must be a `cons`.
diff --git a/tests/lean/run/grind_abstract_mvars.lean b/tests/lean/run/grind_abstract_mvars.lean
index d8f1370295..9d847f40c6 100644
--- a/tests/lean/run/grind_abstract_mvars.lean
+++ b/tests/lean/run/grind_abstract_mvars.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (xs : Array Nat)
     (w : ∀ (j : Nat), 0 ≤ j → ∀ (x : j < xs.size / 2), xs[j] = xs[xs.size - 1 - j])
     (i : Nat) (hi₁ : i < xs.reverse.size) (hi₂ : i < xs.size) (h : i < xs.size / 2) : xs.reverse[i] = xs[i] := by
diff --git a/tests/lean/run/grind_append_issue.lean b/tests/lean/run/grind_append_issue.lean
index 22b8239e18..e1b3888443 100644
--- a/tests/lean/run/grind_append_issue.lean
+++ b/tests/lean/run/grind_append_issue.lean
@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 attribute [grind] List.length_cons List.length_nil List.length_append
 attribute [grind] List.nil_append List.getElem_cons
 attribute [grind] List.eq_nil_of_length_eq_zero List.getElem_append_right
diff --git a/tests/lean/run/grind_array.lean b/tests/lean/run/grind_array.lean
index a14293b85c..7785e14f0a 100644
--- a/tests/lean/run/grind_array.lean
+++ b/tests/lean/run/grind_array.lean
@@ -1,4 +1,2 @@
-set_option grind.warning false
-
 example {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} :
     l.toArray.uset i a h = (l.set i.toNat a).toArray := by grind
diff --git a/tests/lean/run/grind_bintree.lean b/tests/lean/run/grind_bintree.lean
index 5a68261a2a..147f645ca0 100644
--- a/tests/lean/run/grind_bintree.lean
+++ b/tests/lean/run/grind_bintree.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 reset_grind_attrs%
 
 attribute [grind] List.append_assoc List.cons_append List.nil_append
diff --git a/tests/lean/run/grind_bool_diseq.lean b/tests/lean/run/grind_bool_diseq.lean
index e166eecc8b..3d52f25c6d 100644
--- a/tests/lean/run/grind_bool_diseq.lean
+++ b/tests/lean/run/grind_bool_diseq.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (f : Bool → Nat) : (x = y ↔ q) → ¬ q → y = false → f x = 0 → f true = 0 := by
   grind (splits := 0)
 
diff --git a/tests/lean/run/grind_bool_prop.lean b/tests/lean/run/grind_bool_prop.lean
index b4c2e977e9..1bb3c4a768 100644
--- a/tests/lean/run/grind_bool_prop.lean
+++ b/tests/lean/run/grind_bool_prop.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 example (f : Bool → Nat) : f (a && b) = 0 → a = false → f false = 0 := by grind (splits := 0)
 example (f : Bool → Nat) : f (a && b) = 0 → b = false → f false = 0 := by grind (splits := 0)
 example (f : Bool → Nat) : f (a && b) = 0 → a = true → f b = 0 := by grind (splits := 0)
diff --git a/tests/lean/run/grind_casting_issue.lean b/tests/lean/run/grind_casting_issue.lean
index 81352311fa..fb659fa7ab 100644
--- a/tests/lean/run/grind_casting_issue.lean
+++ b/tests/lean/run/grind_casting_issue.lean
@@ -1,5 +1,4 @@
 
-set_option grind.warning false
 @[grind] def codelen (c: List Bool) : Int := c.length
 
 theorem issue1 : codelen [] = 0 := by grind
diff --git a/tests/lean/run/grind_cat.lean b/tests/lean/run/grind_cat.lean
index 1dd166c996..9ff0327bc1 100644
--- a/tests/lean/run/grind_cat.lean
+++ b/tests/lean/run/grind_cat.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
 namespace CategoryTheory
diff --git a/tests/lean/run/grind_clear_error.lean b/tests/lean/run/grind_clear_error.lean
index 8e447aaffd..39c079eac5 100644
--- a/tests/lean/run/grind_clear_error.lean
+++ b/tests/lean/run/grind_clear_error.lean
@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 attribute [grind] List.not_mem_nil
 
 /--
diff --git a/tests/lean/run/grind_congr.lean b/tests/lean/run/grind_congr.lean
index 4eee390d20..f8632f09f3 100644
--- a/tests/lean/run/grind_congr.lean
+++ b/tests/lean/run/grind_congr.lean
@@ -1,6 +1,4 @@
 import Lean
-set_option grind.warning false
-
 def f (a : Nat) := a + a + a
 def g (a : Nat) := a + a
 
diff --git a/tests/lean/run/grind_congr_hash_issue.lean b/tests/lean/run/grind_congr_hash_issue.lean
index 75f18e6752..0df83aa752 100644
--- a/tests/lean/run/grind_congr_hash_issue.lean
+++ b/tests/lean/run/grind_congr_hash_issue.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 opaque f : Nat → Nat
diff --git a/tests/lean/run/grind_constProp.lean b/tests/lean/run/grind_constProp.lean
index 11450ccc3b..a3a3485976 100644
--- a/tests/lean/run/grind_constProp.lean
+++ b/tests/lean/run/grind_constProp.lean
@@ -1,7 +1,5 @@
 reset_grind_attrs%
 
-set_option grind.warning false
-
 attribute [grind cases] Or
 attribute [grind =] List.length_nil List.length_cons Option.getD
 
diff --git a/tests/lean/run/grind_const_pattern.lean b/tests/lean/run/grind_const_pattern.lean
index 22af8eb68a..263496f97d 100644
--- a/tests/lean/run/grind_const_pattern.lean
+++ b/tests/lean/run/grind_const_pattern.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 reset_grind_attrs%
 
 attribute [grind] List.map_append
diff --git a/tests/lean/run/grind_countP.lean b/tests/lean/run/grind_countP.lean
index f329869d2b..4456e89c41 100644
--- a/tests/lean/run/grind_countP.lean
+++ b/tests/lean/run/grind_countP.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 variable {α : Type u} {l : List α} {P Q : α → Bool}
 
 attribute [grind] List.countP_nil List.countP_cons
diff --git a/tests/lean/run/grind_cutsat_auto.lean b/tests/lean/run/grind_cutsat_auto.lean
index e445e794f0..d35e12eb11 100644
--- a/tests/lean/run/grind_cutsat_auto.lean
+++ b/tests/lean/run/grind_cutsat_auto.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example : ∀ x : Int, x > 7 → 2 * x > 14 := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_cooper.lean b/tests/lean/run/grind_cutsat_cooper.lean
index 38dcd6dc4d..057ceb2afe 100644
--- a/tests/lean/run/grind_cutsat_cooper.lean
+++ b/tests/lean/run/grind_cutsat_cooper.lean
@@ -1,6 +1,4 @@
 import Std.Internal.Rat
-set_option grind.warning false
-
 example (x y : Int) :
     27 ≤ 11*x + 13*y →
     11*x + 13*y ≤ 45 →
diff --git a/tests/lean/run/grind_cutsat_diseq_1.lean b/tests/lean/run/grind_cutsat_diseq_1.lean
index eddc81729e..dc172723df 100644
--- a/tests/lean/run/grind_cutsat_diseq_1.lean
+++ b/tests/lean/run/grind_cutsat_diseq_1.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_diseq_2.lean b/tests/lean/run/grind_cutsat_diseq_2.lean
index 20bf6e4b03..bf61106b5c 100644
--- a/tests/lean/run/grind_cutsat_diseq_2.lean
+++ b/tests/lean/run/grind_cutsat_diseq_2.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_diseq_3.lean b/tests/lean/run/grind_cutsat_diseq_3.lean
index 282fce0c91..66302dd557 100644
--- a/tests/lean/run/grind_cutsat_diseq_3.lean
+++ b/tests/lean/run/grind_cutsat_diseq_3.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_diseq_cooper.lean b/tests/lean/run/grind_cutsat_diseq_cooper.lean
index fcd3dae282..40a38f90ad 100644
--- a/tests/lean/run/grind_cutsat_diseq_cooper.lean
+++ b/tests/lean/run/grind_cutsat_diseq_cooper.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 theorem ex1 (x : Int) : 10 ≤ x → x ≤ 20 → x ≠ 11 → 11 ∣ x → False := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_div_1.lean b/tests/lean/run/grind_cutsat_div_1.lean
index 3a61e154cf..b2fb90f76c 100644
--- a/tests/lean/run/grind_cutsat_div_1.lean
+++ b/tests/lean/run/grind_cutsat_div_1.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 set_option pp.structureInstances false
 open Int.Linear
diff --git a/tests/lean/run/grind_cutsat_div_mod.lean b/tests/lean/run/grind_cutsat_div_mod.lean
index e2477a8b61..e622a38d31 100644
--- a/tests/lean/run/grind_cutsat_div_mod.lean
+++ b/tests/lean/run/grind_cutsat_div_mod.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (x y : Int) : x / 2 + y = 3 → x = 5 → y = 1 := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_eq_1.lean b/tests/lean/run/grind_cutsat_eq_1.lean
index f0318fc4a8..baa0503400 100644
--- a/tests/lean/run/grind_cutsat_eq_1.lean
+++ b/tests/lean/run/grind_cutsat_eq_1.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_le_1.lean b/tests/lean/run/grind_cutsat_le_1.lean
index 63f9c790fb..16506e823a 100644
--- a/tests/lean/run/grind_cutsat_le_1.lean
+++ b/tests/lean/run/grind_cutsat_le_1.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 /--
diff --git a/tests/lean/run/grind_cutsat_le_2.lean b/tests/lean/run/grind_cutsat_le_2.lean
index 7da35a0789..db17883866 100644
--- a/tests/lean/run/grind_cutsat_le_2.lean
+++ b/tests/lean/run/grind_cutsat_le_2.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_natCast_propagation.lean b/tests/lean/run/grind_cutsat_natCast_propagation.lean
index 28046b8a1d..4a2cf283c8 100644
--- a/tests/lean/run/grind_cutsat_natCast_propagation.lean
+++ b/tests/lean/run/grind_cutsat_natCast_propagation.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a b : Nat) : a  = a + b - b := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_nat_dvd.lean b/tests/lean/run/grind_cutsat_nat_dvd.lean
index b6f47197f8..11fcd3041f 100644
--- a/tests/lean/run/grind_cutsat_nat_dvd.lean
+++ b/tests/lean/run/grind_cutsat_nat_dvd.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 theorem ex₁ (a : Nat) (h₁ : 2 ∣ a) (h₂ : 2 ∣ a + 1) : False := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_nat_eq.lean b/tests/lean/run/grind_cutsat_nat_eq.lean
index 89beaf0d60..464bcd8f09 100644
--- a/tests/lean/run/grind_cutsat_nat_eq.lean
+++ b/tests/lean/run/grind_cutsat_nat_eq.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a b c : Nat) : a = 0 → b = 0 → c ≥ a + b := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_nat_le.lean b/tests/lean/run/grind_cutsat_nat_le.lean
index 32e61336de..1a59ea276e 100644
--- a/tests/lean/run/grind_cutsat_nat_le.lean
+++ b/tests/lean/run/grind_cutsat_nat_le.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 theorem ex1 (x y z : Nat) : x < y + z → y + 1 < z → z + x < 3*z := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_omega.lean b/tests/lean/run/grind_cutsat_omega.lean
index adfc4f032c..16cbeba293 100644
--- a/tests/lean/run/grind_cutsat_omega.lean
+++ b/tests/lean/run/grind_cutsat_omega.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (_ : (1 : Int) < (0 : Int)) : False := by grind
 example (_ : (0 : Int) < (0 : Int)) : False := by grind
 example (_ : (0 : Int) < (1 : Int)) : True := by grind
diff --git a/tests/lean/run/grind_cutsat_tests.lean b/tests/lean/run/grind_cutsat_tests.lean
index 058154e5a0..678415ed32 100644
--- a/tests/lean/run/grind_cutsat_tests.lean
+++ b/tests/lean/run/grind_cutsat_tests.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (w x y z : Int) :
   2*w + 3*x - 4*y + z = 10 →
   w - x + 2*y - 3*z = 5 →
diff --git a/tests/lean/run/grind_ematch_gen_pattern.lean b/tests/lean/run/grind_ematch_gen_pattern.lean
index 884ad0e47c..29e6ecba50 100644
--- a/tests/lean/run/grind_ematch_gen_pattern.lean
+++ b/tests/lean/run/grind_ematch_gen_pattern.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 def f (x : Option Nat) (h : x ≠ none) : Nat :=
   match x with
   | none => by contradiction
diff --git a/tests/lean/run/grind_ematch_ground_implicit_inst.lean b/tests/lean/run/grind_ematch_ground_implicit_inst.lean
index 0b1a33dab5..86f8ee67d2 100644
--- a/tests/lean/run/grind_ematch_ground_implicit_inst.lean
+++ b/tests/lean/run/grind_ematch_ground_implicit_inst.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a : Nat) : max a a = a := by
   grind
 
diff --git a/tests/lean/run/grind_ematch_theorem_activation.lean b/tests/lean/run/grind_ematch_theorem_activation.lean
index fd0065e060..6132458569 100644
--- a/tests/lean/run/grind_ematch_theorem_activation.lean
+++ b/tests/lean/run/grind_ematch_theorem_activation.lean
@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 attribute [grind] List.length_set
 attribute [grind →] List.eq_nil_of_length_eq_zero
 attribute [grind] List.getElem_set
diff --git a/tests/lean/run/grind_ematch_type_error.lean b/tests/lean/run/grind_ematch_type_error.lean
index 9cfbdba524..2990fe3e1b 100644
--- a/tests/lean/run/grind_ematch_type_error.lean
+++ b/tests/lean/run/grind_ematch_type_error.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2) :
     xs[j] = xs[xs.size - 1 - j] := by
   grind
diff --git a/tests/lean/run/grind_eq_bwd.lean b/tests/lean/run/grind_eq_bwd.lean
index fc88bc13db..9d4890f105 100644
--- a/tests/lean/run/grind_eq_bwd.lean
+++ b/tests/lean/run/grind_eq_bwd.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 theorem dummy (x : Nat) : x = x :=
   rfl
 
diff --git a/tests/lean/run/grind_eq_false_of_imp_eq_false.lean b/tests/lean/run/grind_eq_false_of_imp_eq_false.lean
index 8a9d0ea7c2..ef30c4df99 100644
--- a/tests/lean/run/grind_eq_false_of_imp_eq_false.lean
+++ b/tests/lean/run/grind_eq_false_of_imp_eq_false.lean
@@ -1,5 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
 open List
 
 attribute [grind] List.map_nil
diff --git a/tests/lean/run/grind_eqres_bug.lean b/tests/lean/run/grind_eqres_bug.lean
index bf04f2972f..b64a066dc5 100644
--- a/tests/lean/run/grind_eqres_bug.lean
+++ b/tests/lean/run/grind_eqres_bug.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 /--
 trace: [grind.eqResolution] ∀ (x : Nat), p x a → ∀ (y : Nat), p y b → ¬x = y, ∀ (y : Nat), p y a → p y b → False
 [grind.ematch.instance] local_0: p c a → ¬p c b
diff --git a/tests/lean/run/grind_eta.lean b/tests/lean/run/grind_eta.lean
index 1bf4358217..5b8443f9ce 100644
--- a/tests/lean/run/grind_eta.lean
+++ b/tests/lean/run/grind_eta.lean
@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 example {l : List α} {f : β → α → β} {b : β} :
     l.foldl f b = l.reverse.foldr (fun x y => f y x) b := by
   grind [List.foldr_reverse]
diff --git a/tests/lean/run/grind_etaStruct.lean b/tests/lean/run/grind_etaStruct.lean
index a25dd0427a..356fd5e60e 100644
--- a/tests/lean/run/grind_etaStruct.lean
+++ b/tests/lean/run/grind_etaStruct.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 opaque f (a : Nat) : Nat × Bool
 
 example (a b : Nat) : (f a).1 = (f b).1 → (f a).2 = (f b).2 → f a = f b := by
diff --git a/tests/lean/run/grind_exfalso.lean b/tests/lean/run/grind_exfalso.lean
index 2a317e222a..cb82241e84 100644
--- a/tests/lean/run/grind_exfalso.lean
+++ b/tests/lean/run/grind_exfalso.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (x : Nat) (h : x < 0) : Nat → Nat := by
   grind
 
diff --git a/tests/lean/run/grind_fastEraseDups.lean b/tests/lean/run/grind_fastEraseDups.lean
index c73d2f504f..b27a3a331f 100644
--- a/tests/lean/run/grind_fastEraseDups.lean
+++ b/tests/lean/run/grind_fastEraseDups.lean
@@ -3,8 +3,6 @@ import Std.Data.HashSet
 
 open Std
 
-set_option grind.warning false
-
 namespace List
 
 -- Fast duplicate-removing function, using a hash set to check if an element was seen before
diff --git a/tests/lean/run/grind_funext.lean b/tests/lean/run/grind_funext.lean
index ffe8d4fba6..58819569b7 100644
--- a/tests/lean/run/grind_funext.lean
+++ b/tests/lean/run/grind_funext.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (f : (Nat → Nat) → Nat → Nat → Nat) : a = b → f (fun x => a + x) 1 b = f (fun x => b + x) 1 a := by
   grind
 
diff --git a/tests/lean/run/grind_getElem.lean b/tests/lean/run/grind_getElem.lean
index a2da8ffa07..84f1d676d0 100644
--- a/tests/lean/run/grind_getElem.lean
+++ b/tests/lean/run/grind_getElem.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 reset_grind_attrs%
 
 attribute [grind]
diff --git a/tests/lean/run/grind_getLast_dropLast.lean b/tests/lean/run/grind_getLast_dropLast.lean
index 08773ab765..2c5611bde8 100644
--- a/tests/lean/run/grind_getLast_dropLast.lean
+++ b/tests/lean/run/grind_getLast_dropLast.lean
@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 open List
 
 theorem length_pos_of_ne_nil {l : List α} (h : l ≠ []) : 0 < l.length := by
diff --git a/tests/lean/run/grind_guide.lean b/tests/lean/run/grind_guide.lean
index 959067fd07..d396fd72e2 100644
--- a/tests/lean/run/grind_guide.lean
+++ b/tests/lean/run/grind_guide.lean
@@ -11,8 +11,6 @@ we keep all the facts we know about the current goal.
 Remark: Terms known to be true (false) belong to the equivalence class of the term `True` (`False`).
 -/
 
-set_option grind.warning false -- Disables warning messages stating that `grind` is WIP.
-
 example (a b c : α) (f : α → α) : f a = c → a = b → c = f b := by
   grind
 
diff --git a/tests/lean/run/grind_hashmap_list.lean b/tests/lean/run/grind_hashmap_list.lean
index 319619fbd0..ca9c3ef29a 100644
--- a/tests/lean/run/grind_hashmap_list.lean
+++ b/tests/lean/run/grind_hashmap_list.lean
@@ -1,5 +1,4 @@
 import Std.Data.HashMap
-set_option grind.warning false
 reset_grind_attrs%
 
 open Std
diff --git a/tests/lean/run/grind_hcongr.lean b/tests/lean/run/grind_hcongr.lean
index 256138d249..a451d5d178 100644
--- a/tests/lean/run/grind_hcongr.lean
+++ b/tests/lean/run/grind_hcongr.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 def Matrix (m : Type) (n : Type) (α : Type) : Type :=
   m → n → α
 
diff --git a/tests/lean/run/grind_heapsort.lean b/tests/lean/run/grind_heapsort.lean
index 4f80387d7d..be1d0dc67e 100644
--- a/tests/lean/run/grind_heapsort.lean
+++ b/tests/lean/run/grind_heapsort.lean
@@ -1,6 +1,4 @@
 import Lean
-set_option grind.warning false
-
 /-
 Use `grind` as one of the tactics for array-element access and termination proofs.
 -/
diff --git a/tests/lean/run/grind_heartbeats.lean b/tests/lean/run/grind_heartbeats.lean
index 530c40496d..2245808287 100644
--- a/tests/lean/run/grind_heartbeats.lean
+++ b/tests/lean/run/grind_heartbeats.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 opaque f : Nat → Nat
 opaque op : Nat → Nat → Nat
 @[grind] theorem op_comm : op x y = op y x := sorry
diff --git a/tests/lean/run/grind_indexmap.lean b/tests/lean/run/grind_indexmap.lean
index 8d7c2ebf7c..6d9c40d4fe 100644
--- a/tests/lean/run/grind_indexmap.lean
+++ b/tests/lean/run/grind_indexmap.lean
@@ -4,8 +4,6 @@
 
 import Std.Data.HashMap
 
-set_option grind.warning false
-
 macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
 
 open Std
diff --git a/tests/lean/run/grind_indexmap_pre.lean b/tests/lean/run/grind_indexmap_pre.lean
index e7c64272ce..71fa28443b 100644
--- a/tests/lean/run/grind_indexmap_pre.lean
+++ b/tests/lean/run/grind_indexmap_pre.lean
@@ -3,8 +3,6 @@
 
 import Std.Data.HashMap
 
-set_option grind.warning false
-
 open Std
 
 structure IndexMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
diff --git a/tests/lean/run/grind_ite.lean b/tests/lean/run/grind_ite.lean
index 96eff8044e..a95860dd56 100644
--- a/tests/lean/run/grind_ite.lean
+++ b/tests/lean/run/grind_ite.lean
@@ -111,8 +111,6 @@ def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized
 -/
 
 -- `grind` is currently experimental, but for now we can suppress the warnings about this.
-set_option grind.warning false
-
 namespace IfExpr
 
 /--
diff --git a/tests/lean/run/grind_ite_congr.lean b/tests/lean/run/grind_ite_congr.lean
index 74e7395789..b7b9375f6c 100644
--- a/tests/lean/run/grind_ite_congr.lean
+++ b/tests/lean/run/grind_ite_congr.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example : ((if true then id else id) false) = false := by
   grind
 
diff --git a/tests/lean/run/grind_ite_split_issue.lean b/tests/lean/run/grind_ite_split_issue.lean
index 32474375ce..f8b174a37b 100644
--- a/tests/lean/run/grind_ite_split_issue.lean
+++ b/tests/lean/run/grind_ite_split_issue.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a b : Int) : min a b = 10 → a ≥ 10 := by
   grind
 
diff --git a/tests/lean/run/grind_ite_unused_match.lean b/tests/lean/run/grind_ite_unused_match.lean
index fcb255682b..ec8a905d17 100644
--- a/tests/lean/run/grind_ite_unused_match.lean
+++ b/tests/lean/run/grind_ite_unused_match.lean
@@ -99,8 +99,6 @@ def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized
 -/
 
 -- `grind` is currently experimental, but for now we can suppress the warnings about this.
-set_option grind.warning false
-
 namespace IfExpr
 
 attribute [grind] List.mem_cons List.not_mem_nil List.mem_append
diff --git a/tests/lean/run/grind_linarith_1.lean b/tests/lean/run/grind_linarith_1.lean
index 2d7685475c..3ea414d41e 100644
--- a/tests/lean/run/grind_linarith_1.lean
+++ b/tests/lean/run/grind_linarith_1.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 open Lean.Grind
 
 example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
diff --git a/tests/lean/run/grind_list.lean b/tests/lean/run/grind_list.lean
index 75db0132b2..222f351c41 100644
--- a/tests/lean/run/grind_list.lean
+++ b/tests/lean/run/grind_list.lean
@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 namespace List
 
 attribute [local grind =] List.length_cons in
diff --git a/tests/lean/run/grind_list2.lean b/tests/lean/run/grind_list2.lean
index 1d8cc76615..4f7910c1aa 100644
--- a/tests/lean/run/grind_list2.lean
+++ b/tests/lean/run/grind_list2.lean
@@ -10,7 +10,6 @@
 -- `tests/lean/grind/experiments/list.lean` contains everything from `Data/List/Lemmas.lean`
 -- that still resists `grind`!
 
-set_option grind.warning false
 open List Nat
 
 namespace Hidden
diff --git a/tests/lean/run/grind_list_count.lean b/tests/lean/run/grind_list_count.lean
index d53ec9ff94..a80aad8b54 100644
--- a/tests/lean/run/grind_list_count.lean
+++ b/tests/lean/run/grind_list_count.lean
@@ -1,6 +1,4 @@
 
-set_option grind.warning false
-
 open List Nat
 
 namespace List'
diff --git a/tests/lean/run/grind_list_issue.lean b/tests/lean/run/grind_list_issue.lean
index 9ec06c0c68..1fa8622f2c 100644
--- a/tests/lean/run/grind_list_issue.lean
+++ b/tests/lean/run/grind_list_issue.lean
@@ -1,5 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
 open List Nat
 
 attribute [grind] List.filter_nil List.filter_cons
diff --git a/tests/lean/run/grind_list_sublist.lean b/tests/lean/run/grind_list_sublist.lean
index 2d66c17a7c..e94ea638af 100644
--- a/tests/lean/run/grind_list_sublist.lean
+++ b/tests/lean/run/grind_list_sublist.lean
@@ -1,7 +1,5 @@
 open List
 
-set_option grind.warning false
-
 variable {α} {l₁ l₂ l₃ l₄ l₅ : List α}
 
 example : l₂ ++ l₄ ⊆ l₁ ++ l₂ ++ l₃ ++ l₄ ++ l₅ := by
diff --git a/tests/lean/run/grind_lookahead.lean b/tests/lean/run/grind_lookahead.lean
index 82b76a7c81..6883b8e619 100644
--- a/tests/lean/run/grind_lookahead.lean
+++ b/tests/lean/run/grind_lookahead.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 reset_grind_attrs%
 
 attribute [grind] List.eq_nil_of_length_eq_zero
diff --git a/tests/lean/run/grind_map.lean b/tests/lean/run/grind_map.lean
index 7d32e6f137..3515a5902b 100644
--- a/tests/lean/run/grind_map.lean
+++ b/tests/lean/run/grind_map.lean
@@ -4,8 +4,6 @@ import Std.Data.ExtHashMap
 import Std.Data.HashSet
 import Std.Data.TreeMap
 
-set_option grind.warning false
-
 open Std
 
 section
diff --git a/tests/lean/run/grind_mark_nested_proofs_bug.lean b/tests/lean/run/grind_mark_nested_proofs_bug.lean
index cbaef54291..8a09fbf3a0 100644
--- a/tests/lean/run/grind_mark_nested_proofs_bug.lean
+++ b/tests/lean/run/grind_mark_nested_proofs_bug.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (as bs cs : Array α) (v : α)
         (i : Nat)
         (h₁ : i < as.size)
diff --git a/tests/lean/run/grind_match_with_eq.lean b/tests/lean/run/grind_match_with_eq.lean
index 83a26841fc..f542814355 100644
--- a/tests/lean/run/grind_match_with_eq.lean
+++ b/tests/lean/run/grind_match_with_eq.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 def f (a : Option Nat) (h : a ≠ none) : Nat :=
  match a with
  | some a => a
diff --git a/tests/lean/run/grind_mbtc_1.lean b/tests/lean/run/grind_mbtc_1.lean
index ce5b32f940..d0935e434c 100644
--- a/tests/lean/run/grind_mbtc_1.lean
+++ b/tests/lean/run/grind_mbtc_1.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (f : Int → Int) (x : Int)
     : 0 ≤ x → x ≠ 0 → x ≤ 1 → f x = 2 → f 1 = 2 := by
   grind
diff --git a/tests/lean/run/grind_min.lean b/tests/lean/run/grind_min.lean
index 9b82b86c19..e5d8f7cabb 100644
--- a/tests/lean/run/grind_min.lean
+++ b/tests/lean/run/grind_min.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
     (_ : ¬as.size = 0) : min lo (as.size - 1) ≤ i := by
   grind
diff --git a/tests/lean/run/grind_mvar.lean b/tests/lean/run/grind_mvar.lean
index e6972526a8..79d25cc21d 100644
--- a/tests/lean/run/grind_mvar.lean
+++ b/tests/lean/run/grind_mvar.lean
@@ -1,7 +1,5 @@
 open List
 reset_grind_attrs%
-set_option grind.warning false
-
 attribute [grind →] Array.eq_empty_of_append_eq_empty eq_nil_of_length_eq_zero
 attribute [grind] Vector.getElem?_append getElem?_dropLast
 
diff --git a/tests/lean/run/grind_natCast.lean b/tests/lean/run/grind_natCast.lean
index df2be31d78..7c99fbfc95 100644
--- a/tests/lean/run/grind_natCast.lean
+++ b/tests/lean/run/grind_natCast.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (x : Nat) : x ≥ (0 : Int) := by grind
 example (x : Nat) : Int.ofNat x ≥ (0 : Int) := by grind
 example (x : Nat) : NatCast.natCast x ≥ 0 := by grind
diff --git a/tests/lean/run/grind_nochrono.lean b/tests/lean/run/grind_nochrono.lean
index 5571774e05..021740ecf5 100644
--- a/tests/lean/run/grind_nochrono.lean
+++ b/tests/lean/run/grind_nochrono.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 -- In the following test, the first 8 case-splits are irrelevant,
 -- and non-choronological backtracking is used to avoid searching
 -- (2^8 - 1) irrelevant branches
diff --git a/tests/lean/run/grind_offset_cnstr.lean b/tests/lean/run/grind_offset_cnstr.lean
index d814933f40..b906dc4a6b 100644
--- a/tests/lean/run/grind_offset_cnstr.lean
+++ b/tests/lean/run/grind_offset_cnstr.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 /--
diff --git a/tests/lean/run/grind_omega_examples.lean b/tests/lean/run/grind_omega_examples.lean
index bf7e36f8db..0a0d594db7 100644
--- a/tests/lean/run/grind_omega_examples.lean
+++ b/tests/lean/run/grind_omega_examples.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 example {x y : Nat} (_ : x + y > 10) (_ : x < 5) (_ : y < 5) : False := by grind
 example {x y : Nat} (_ : x + y > 10) (_ : 2 * x < 11) (_ : y < 5) : False := by grind
 example {x y : Nat} (_ : 2 * x + 4 * y = 5) : False := by grind
diff --git a/tests/lean/run/grind_option.lean b/tests/lean/run/grind_option.lean
index d201cbc182..e36cf83b09 100644
--- a/tests/lean/run/grind_option.lean
+++ b/tests/lean/run/grind_option.lean
@@ -2,8 +2,6 @@
 -- This may prove fragile, so remember it is okay to update the expected output if appropriate!
 -- Hopefully these will act as regression tests against `grind` activating irrelevant lemmas.
 
-set_option grind.warning false
-
 section
 
 variable [BEq α] {o₁ o₂ o₃ o₄ o₅ : Option α}
diff --git a/tests/lean/run/grind_overapplied_ite.lean b/tests/lean/run/grind_overapplied_ite.lean
index 785e26490f..3b8d750bf1 100644
--- a/tests/lean/run/grind_overapplied_ite.lean
+++ b/tests/lean/run/grind_overapplied_ite.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example : (if (!false) = true then id else id) false = false := by
   grind
 
diff --git a/tests/lean/run/grind_palindrome2.lean b/tests/lean/run/grind_palindrome2.lean
index 87649c2b81..09822e12c8 100644
--- a/tests/lean/run/grind_palindrome2.lean
+++ b/tests/lean/run/grind_palindrome2.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 def IsPalindrome (xs : Array Nat) : Prop := xs.reverse = xs
 
 def checkPalin1 (xs : Array Nat) : Bool :=
diff --git a/tests/lean/run/grind_panic_invariant.lean b/tests/lean/run/grind_panic_invariant.lean
index b995387501..72b3184de3 100644
--- a/tests/lean/run/grind_panic_invariant.lean
+++ b/tests/lean/run/grind_panic_invariant.lean
@@ -5,8 +5,6 @@
   | star_step : ∀ x y z, R x y → star R y z → star R x z
 
 set_option grind.debug true
-set_option grind.warning false
-
 inductive com: Type where
   | SKIP
   | ASSIGN
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index ecde73cc1b..9a6cd0b04c 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -1,5 +1,4 @@
 abbrev f (a : α) := a
-set_option grind.warning false
 set_option grind.debug true
 set_option grind.debug.proofs true
 
diff --git a/tests/lean/run/grind_product_eta_and_split.lean b/tests/lean/run/grind_product_eta_and_split.lean
index bd1291b868..b0c8f0b007 100644
--- a/tests/lean/run/grind_product_eta_and_split.lean
+++ b/tests/lean/run/grind_product_eta_and_split.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 def α : Type := Unit × Unit
diff --git a/tests/lean/run/grind_qsort.lean b/tests/lean/run/grind_qsort.lean
index e07140a5d6..98356eaec7 100644
--- a/tests/lean/run/grind_qsort.lean
+++ b/tests/lean/run/grind_qsort.lean
@@ -5,8 +5,6 @@ Authors: Kim Morrison
 -/
 
 -- TODO: when `grind` is ready for production use, move this file to `src/Init/Data/Array/QSort/Lemmas.lean`.
-set_option grind.warning false
-
 /-!
 # Verification of `Array.qsort`
 
diff --git a/tests/lean/run/grind_regression.lean b/tests/lean/run/grind_regression.lean
index 24d33a67a4..3b00b86d96 100644
--- a/tests/lean/run/grind_regression.lean
+++ b/tests/lean/run/grind_regression.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Marcus Rossel, Kim Morrison
 -/
 import Lean.Elab.Term
-set_option grind.warning false
 /-!
 These tests are originally from the `lean-egg` repository at
 https://github.com/marcusrossel/lean-egg and were written by Marcus Rossel.
diff --git a/tests/lean/run/grind_ring_1.lean b/tests/lean/run/grind_ring_1.lean
index bef6809046..878af04016 100644
--- a/tests/lean/run/grind_ring_1.lean
+++ b/tests/lean/run/grind_ring_1.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 open Lean.Grind
diff --git a/tests/lean/run/grind_ring_2.lean b/tests/lean/run/grind_ring_2.lean
index 7850fba020..fb79ab0649 100644
--- a/tests/lean/run/grind_ring_2.lean
+++ b/tests/lean/run/grind_ring_2.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Lean.Grind
 
diff --git a/tests/lean/run/grind_ring_3.lean b/tests/lean/run/grind_ring_3.lean
index ea130c7ace..0aedea597e 100644
--- a/tests/lean/run/grind_ring_3.lean
+++ b/tests/lean/run/grind_ring_3.lean
@@ -1,7 +1,5 @@
 open Lean.Grind
 
-set_option grind.warning false
-
 example {α} [CommRing α] [IsCharP α 0]
     (d t : α)
   (Δ40 : d + t + d * t = 0)
diff --git a/tests/lean/run/grind_ring_4.lean b/tests/lean/run/grind_ring_4.lean
index 14c265c908..c16ed99123 100644
--- a/tests/lean/run/grind_ring_4.lean
+++ b/tests/lean/run/grind_ring_4.lean
@@ -1,7 +1,5 @@
 open Lean.Grind
 
-set_option grind.warning false
-
 example {α} [CommRing α] [IsCharP α 0] [NoNatZeroDivisors α]
     (d t : α)
   (Δ40 : d + t + d * t = 0)
diff --git a/tests/lean/run/grind_sort_eqc.lean b/tests/lean/run/grind_sort_eqc.lean
index 39e784dc8f..958626ae00 100644
--- a/tests/lean/run/grind_sort_eqc.lean
+++ b/tests/lean/run/grind_sort_eqc.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 opaque f [Inhabited α] : α → α
 theorem feq [Inhabited α] [Add α] [One α] (x : α) : f x = f (f x) + 1 := sorry
 opaque g [Inhabited α] : α → α → α
diff --git a/tests/lean/run/grind_split_arith_imp.lean b/tests/lean/run/grind_split_arith_imp.lean
index 0f4fdb950b..7ad7488a3a 100644
--- a/tests/lean/run/grind_split_arith_imp.lean
+++ b/tests/lean/run/grind_split_arith_imp.lean
@@ -1,5 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
 attribute [grind] Vector.getElem_swap_of_ne
 
 example (hi : i < n) (hj : j < i) (hk : k < j) (as : Vector α n) (p : α → Prop) (h : p as[k]) :
diff --git a/tests/lean/run/grind_split_issue.lean b/tests/lean/run/grind_split_issue.lean
index aa765bcdaf..435ab672d2 100644
--- a/tests/lean/run/grind_split_issue.lean
+++ b/tests/lean/run/grind_split_issue.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 variable (d : Nat) in
 inductive X : Nat → Prop
   | f {s : Nat} : X s
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index c475eb79da..86275d48d0 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a b : List Nat) : a = [] → b = [2] → a = b → False := by
   grind
 
diff --git a/tests/lean/run/grind_trace.lean b/tests/lean/run/grind_trace.lean
index f6b3f40464..9584cf4b28 100644
--- a/tests/lean/run/grind_trace.lean
+++ b/tests/lean/run/grind_trace.lean
@@ -1,7 +1,5 @@
 reset_grind_attrs%
 
-set_option grind.warning false
-
 attribute [grind =] List.length_cons
 attribute [grind →] List.getElem?_eq_getElem
 attribute [grind =] List.length_replicate
diff --git a/tests/lean/run/grind_trig.lean b/tests/lean/run/grind_trig.lean
index 67687689e5..a53a3c0752 100644
--- a/tests/lean/run/grind_trig.lean
+++ b/tests/lean/run/grind_trig.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 axiom R : Type
 instance : Lean.Grind.CommRing R := sorry
 
diff --git a/tests/lean/run/grind_try_trace.lean b/tests/lean/run/grind_try_trace.lean
index b23e10e84c..2a3d2c43b4 100644
--- a/tests/lean/run/grind_try_trace.lean
+++ b/tests/lean/run/grind_try_trace.lean
@@ -1,4 +1,3 @@
-set_option grind.warning false
 reset_grind_attrs%
 
 /--
diff --git a/tests/lean/run/grind_vector.lean b/tests/lean/run/grind_vector.lean
index 86c9935a12..cd2fd02097 100644
--- a/tests/lean/run/grind_vector.lean
+++ b/tests/lean/run/grind_vector.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by grind
 
 example [LT α] {xs ys : Vector α n} : xs.toList < ys.toList ↔ xs < ys := by grind
diff --git a/tests/lean/run/simp_arith_issues.lean b/tests/lean/run/simp_arith_issues.lean
index 78ea4e4825..6323d8d8a6 100644
--- a/tests/lean/run/simp_arith_issues.lean
+++ b/tests/lean/run/simp_arith_issues.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a b : Int) (f : Int → Int) (h : a = (if a < 0 then b - 1 else 1 - b)) : False := by
   simp +arith only at h
   guard_hyp h : a = if a + 1 ≤ 0 then b + -1 else -1 * b + 1