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.

Author: kim-em

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

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

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

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`.

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

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

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

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

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

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