feat: add @[grind ext] attributes for extensional maps

Author: kim-em

src/Std/Data/ExtDHashMap/Lemmas.lean

@@ -2791,7 +2791,7 @@ section Ext
 
 variable {m₁ m₂ : Std.ExtDHashMap α β}
 
-@[ext]
+@[ext, grind ext]
 theorem ext_get? [LawfulBEq α] {m₁ m₂ : Std.ExtDHashMap α β} (h : ∀ k, m₁.get? k = m₂.get? k) : m₁ = m₂ :=
   m₁.inductionOn₂ m₂ (fun _ _ h => sound (.of_forall_get?_eq h)) h
 

src/Std/Data/ExtDTreeMap/Lemmas.lean

@@ -4369,7 +4369,7 @@ section Ext
 
 variable {t₁ t₂ : ExtDTreeMap α β cmp}
 
-@[ext]
+@[ext, grind ext]
 theorem ext_get? [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : ExtDTreeMap α β cmp}
     (h : ∀ k, t₁.get? k = t₂.get? k) : t₁ = t₂ :=
   t₁.inductionOn₂ t₂ (fun _ _ h => sound (.of_forall_get?_eq h)) h

src/Std/Data/ExtHashMap/Lemmas.lean

@@ -1705,7 +1705,7 @@ theorem ext_getKey_getElem? [EquivBEq α] [LawfulHashable α]
     (hv : ∀ k : α, m₁[k]? = m₂[k]?) : m₁ = m₂ :=
   ext (ExtDHashMap.Const.ext_getKey_get? hk hv)
 
-@[ext]
+@[ext, grind ext]
 theorem ext_getElem? [LawfulBEq α] {m₁ m₂ : ExtHashMap α β}
     (h : ∀ k : α, m₁[k]? = m₂[k]?) : m₁ = m₂ :=
   ext (ExtDHashMap.Const.ext_get? h)

src/Std/Data/ExtHashSet/Lemmas.lean

@@ -678,7 +678,7 @@ theorem ext_contains [LawfulBEq α] {m₁ m₂ : ExtHashSet α}
     (h : ∀ k, m₁.contains k = m₂.contains k) : m₁ = m₂ :=
   ext (ExtHashMap.ext_contains_unit h)
 
-@[ext]
+@[ext, grind ext]
 theorem ext_mem [LawfulBEq α] {m₁ m₂ : ExtHashSet α} (h : ∀ k, k ∈ m₁ ↔ k ∈ m₂) : m₁ = m₂ :=
   ext (ExtHashMap.ext_mem_unit h)
 

src/Std/Data/ExtTreeMap/Lemmas.lean

@@ -3021,7 +3021,7 @@ theorem ext_getKey_getElem? [TransCmp cmp] {t₁ t₂ : ExtTreeMap α β cmp}
     (hv : ∀ k : α, t₁[k]? = t₂[k]?) : t₁ = t₂ :=
   ext (ExtDTreeMap.Const.ext_getKey_get? hk hv)
 
-@[ext]
+@[ext, grind ext]
 theorem ext_getElem? [TransCmp cmp] [LawfulEqCmp cmp]
     {t₁ t₂ : ExtTreeMap α β cmp}
     (h : ∀ k : α, t₁[k]? = t₂[k]?) : t₁ = t₂ :=

src/Std/Data/ExtTreeSet/Lemmas.lean

@@ -1554,7 +1554,7 @@ theorem ext_contains [TransCmp cmp] [LawfulEqCmp cmp]
     (h : ∀ k, t₁.contains k = t₂.contains k) : t₁ = t₂ :=
   ext (ExtTreeMap.ext_contains_unit h)
 
-@[ext]
+@[ext, grind ext]
 theorem ext_mem [TransCmp cmp] [LawfulEqCmp cmp]
     {t₁ t₂ : ExtTreeSet α cmp}
     (h : ∀ k, k ∈ t₁ ↔ k ∈ t₂) : t₁ = t₂ :=

tests/lean/run/grind_ExtTreeSet.lean

@@ -0,0 +1,17 @@
+import Std
+
+open Std
+
+example {cmp : α → α → Ordering} [TransCmp cmp] (m : ExtTreeSet α cmp) (x : α) :
+    (m.insert x).erase x = m.erase x := by
+  grind
+
+example (m : ExtTreeSet Nat compare) (x : Nat) : (m.insert x).erase x = m.erase x := by
+  grind
+
+example [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (m : ExtHashSet α) (x : α) :
+    (m.insert x).erase x = m.erase x := by
+  grind
+
+example (m : ExtHashMap Int Int) (x y : Int) : (m.insert x y).erase x = m.erase x := by
+  grind