fix test?

Author: kim-em

MathlibTest/grind/pairwise_disjoint.lean

@@ -5,7 +5,14 @@ abbrev S1 : Fin 3 → Finset (Fin 4)
   | 1 => {1}
   | 2 => {2, 3}
 
-attribute [grind _=_] LawfulSingleton.insert_emptyc_eq
+-- #adaptation_note 2025-10-27
+-- This theorem was deprecated, but the replacement theorm has `Singleton` as an implicit argument,
+-- and this seems to confuse `grind`.
+theorem LawfulSingleton.insert_empty_eq' [EmptyCollection β] [Insert α β] [Singleton α β]
+    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
+  insert_empty_eq _
+
+attribute [grind _=_] LawfulSingleton.insert_empty_eq'
 
 attribute [grind =] Finset.mem_singleton