fix test

src/Init/Grind.lean

@@ -13,3 +13,4 @@ import Init.Grind.Util
 import Init.Grind.Offset
 import Init.Grind.PP
 import Init.Grind.CommRing
+import Init.Grind.Ext

src/Init/Grind/Ext.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Ext
+import Init.Grind.Tactics
+
+attribute [grind ext] funext

src/Lean/Meta/Tactic/Grind/ExtAttr.lean

@@ -20,7 +20,7 @@ builtin_initialize extTheoremsExt : SimpleScopedEnvExtension Name ExtTheorems
 
 def validateExtAttr (declName : Name) : CoreM Unit := do
   unless (← Ext.isExtTheorem declName) do
-    throwError "invalid `[grind ext]`, `{declName}` is tagged with `[ext]`"
+    throwError "invalid `[grind ext]`, `{declName}` is not tagged with `[ext]`"
 
 def addExtAttr (declName : Name) (attrKind : AttributeKind) : CoreM Unit := do
   validateExtAttr declName

tests/lean/run/grind_bintree.lean

@@ -62,8 +62,6 @@ where
      : toListTR.go t acc = t.toList ++ acc := by
     induction t generalizing acc <;> grind [toListTR.go, toList]
 
-attribute [grind ext] funext -- TODO: remove after update-stage0
-
 @[csimp] theorem Tree.toList_eq_toListTR_csimp
                  : @Tree.toList = @Tree.toListTR := by
   grind [toList_eq_toListTR]

tests/lean/run/grind_cat.lean

@@ -68,7 +68,6 @@ structure NatTrans [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F G : Fu
   naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f := by grind
 
 attribute [grind ext] NatTrans.ext -- TODO: remove after builtin extensionality for structures
-attribute [grind ext] funext -- TODO: remove after update-stage0
 
 attribute [simp, grind =] NatTrans.naturality
 

tests/lean/run/grind_cat2.lean

@@ -68,7 +68,6 @@ structure NatTrans [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F G : Fu
   /-- The naturality square for a given morphism. -/
   naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f := by grind
 
-attribute [grind ext] funext -- TODO: remove
 attribute [grind ext] NatTrans.ext
 
 attribute [simp, grind =] NatTrans.naturality

tests/lean/run/grind_funext.lean

@@ -1,6 +1,4 @@
-
 set_option grind.warning false
-attribute [grind ext] funext -- TODO: remove
 
 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

tests/lean/run/grind_ite.lean

@@ -159,7 +159,6 @@ we are allowed to increase the size of the branches by one, and still be smaller
   | var _ => 1
   | .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1
 
-attribute [grind ext] funext -- TODO remove
 set_option profiler true
 /--
 Normalizes the expression at the same time as

tests/lean/run/grind_list.lean

@@ -19,15 +19,22 @@ theorem getElem!_of_getElem?' [Inhabited α] :
     ∀ {l : List α} {i : Nat}, l[i]? = some b → l[i]! = b := by
   grind
 
-attribute [grind ext] List.ext_getElem?
 
 attribute [local grind =] Option.map_some Option.map_none in
 attribute [local grind =] getElem?_map in
 attribute [local grind =] getElem?_replicate in
 theorem map_replicate' : (replicate n a).map f = replicate n (f a) := by
+  grind +extAll
+
+attribute [grind ext] List.ext_getElem?
+
+attribute [local grind =] Option.map_some Option.map_none in
+attribute [local grind =] getElem?_map in
+attribute [local grind =] getElem?_replicate in
+theorem map_replicate'' : (replicate n a).map f = replicate n (f a) := by
   grind?
 
-#print map_replicate'
+#print map_replicate''
 
 attribute [local grind =] getLast?_eq_some_iff in
 attribute [local grind] mem_concat_self in