delete stray file

src/Std/Data/DHashMap/Lemmas.lean

@@ -16,8 +16,6 @@ This file contains lemmas about `Std.DHashMap`. Most of the lemmas require
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 open Std.DHashMap.Internal
 
 set_option linter.missingDocs true

src/Std/Data/DHashMap/RawLemmas.lean

@@ -15,8 +15,6 @@ This file contains lemmas about `Std.Data.DHashMap.Raw`. Most of the lemmas requ
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 open Std.DHashMap.Internal
 
 set_option linter.missingDocs true

src/Std/Data/ExtDHashMap/Lemmas.lean

@@ -12,8 +12,6 @@ import Std.Data.ExtDHashMap.Basic
 This file contains lemmas about `Std.ExtDHashMap`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 

src/Std/Data/ExtHashMap/Lemmas.lean

@@ -13,8 +13,6 @@ import Std.Data.ExtDHashMap.Lemmas
 This module contains lemmas about `Std.ExtHashMap`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 

src/Std/Data/ExtHashSet/Lemmas.lean

@@ -13,8 +13,6 @@ import Std.Data.ExtHashSet.Basic
 This module contains lemmas about `Std.ExtHashSet`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 

src/Std/Data/HashMap/Lemmas.lean

@@ -16,8 +16,6 @@ This module contains lemmas about `Std.Data.HashMap`. Most of the lemmas require
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 

src/Std/Data/HashMap/RawLemmas.lean

@@ -15,8 +15,6 @@ This module contains lemmas about `Std.Data.HashMap.Raw`. Most of the lemmas req
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 

src/Std/Data/HashSet/Lemmas.lean

@@ -15,8 +15,6 @@ This module contains lemmas about `Std.Data.HashSet`. Most of the lemmas require
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 

src/Std/Data/HashSet/RawLemmas.lean

@@ -15,8 +15,6 @@ This module contains lemmas about `Std.Data.HashSet.Raw`. Most of the lemmas req
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 

tests/lean/run/grind_map_uniform.lean

@@ -1,12 +0,0 @@
-import Lean.Meta.Tactic.Grind
-import Std.Data.DHashMap
-import Std.Data.HashMap
-import Std.Data.HashSet
-import Std.Data.TreeMap
-import Std.Data.TreeSet
-
-#eval Lean.Meta.Grind.isEMatchTheorem `Std.DHashMap.isEmpty_emptyWithCapacity
-#eval Lean.Meta.Grind.isEMatchTheorem `Std.HashMap.isEmpty_emptyWithCapacity
-#eval Lean.Meta.Grind.isEMatchTheorem `Std.HashSet.isEmpty_emptyWithCapacity
-#eval Lean.Meta.Grind.isEMatchTheorem `Std.TreeMap.isEmpty_emptyWithCapacity
-#eval Lean.Meta.Grind.isEMatchTheorem `Std.TreeSet.isEmpty_emptyWithCapacity