chore: rename insert_emptyc_eq to insert_empty_eq

src/Init/Core.lean

@@ -514,10 +514,21 @@ export Singleton (singleton)
 class LawfulSingleton (α : Type u) (β : Type v) [EmptyCollection β] [Insert α β] [Singleton α β] :
     Prop where
   /-- `insert x ∅ = {x}` -/
-  insert_emptyc_eq (x : α) : (insert x ∅ : β) = singleton x
-export LawfulSingleton (insert_emptyc_eq)
+  insert_empty_eq (x : α) : (insert x ∅ : β) = singleton x
+export LawfulSingleton (insert_empty_eq)
+
+attribute [simp] insert_empty_eq
+
+@[deprecated insert_empty_eq (since := "2025-03-12")]
+theorem insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
+    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
+  insert_empty_eq _
+
+@[deprecated insert_empty_eq (since := "2025-03-12")]
+theorem LawfulSingleton.insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
+    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
+  insert_empty_eq _
 
-attribute [simp] insert_emptyc_eq
 
 /-- Type class used to implement the notation `{ a ∈ c | p a }` -/
 class Sep (α : outParam <| Type u) (γ : Type v) where

src/Std/Data/DTreeMap/Basic.lean

@@ -102,7 +102,7 @@ instance : Insert ((a : α) × β a) (DTreeMap α β cmp) where
   insert e s := s.insert e.1 e.2
 
 instance : LawfulSingleton ((a : α) × β a) (DTreeMap α β cmp) where
-  insert_emptyc_eq _ := rfl
+  insert_empty_eq _ := rfl
 
 /--
 If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,

src/Std/Data/DTreeMap/Raw/Basic.lean

@@ -107,7 +107,7 @@ instance : Insert ((a : α) × β a) (Raw α β cmp) where
   insert e s := s.insert e.1 e.2
 
 instance : LawfulSingleton ((a : α) × β a) (Raw α β cmp) where
-  insert_emptyc_eq _ := rfl
+  insert_empty_eq _ := rfl
 
 @[inline, inherit_doc DTreeMap.insertIfNew]
 def insertIfNew (t : Raw α β cmp) (a : α) (b : β a) : Raw α β cmp :=

src/Std/Data/TreeMap/Basic.lean

@@ -86,7 +86,7 @@ instance : Insert (α × β) (TreeMap α β cmp) where
   insert e s := s.insert e.1 e.2
 
 instance : LawfulSingleton (α × β) (TreeMap α β cmp) where
-  insert_emptyc_eq _ := rfl
+  insert_empty_eq _ := rfl
 
 @[inline, inherit_doc DTreeMap.insertIfNew]
 def insertIfNew (t : TreeMap α β cmp) (a : α) (b : β) : TreeMap α β cmp :=

src/Std/Data/TreeMap/Raw/Basic.lean

@@ -103,7 +103,7 @@ instance : Insert (α × β) (Raw α β cmp) where
   insert e s := s.insert e.1 e.2
 
 instance : LawfulSingleton (α × β) (Raw α β cmp) where
-  insert_emptyc_eq _ := rfl
+  insert_empty_eq _ := rfl
 
 @[inline, inherit_doc DTreeMap.Raw.insertIfNew]
 def insertIfNew (t : Raw α β cmp) (a : α) (b : β) : Raw α β cmp :=

src/Std/Data/TreeSet/Basic.lean

@@ -99,7 +99,7 @@ instance : Insert α (TreeSet α cmp) where
   insert e s := s.insert e
 
 instance : LawfulSingleton α (TreeSet α cmp) where
-  insert_emptyc_eq _ := rfl
+  insert_empty_eq _ := rfl
 
 /--
 Checks whether an element is present in a set and inserts the element if it was not found.

src/Std/Data/TreeSet/Raw/Basic.lean

@@ -103,7 +103,7 @@ instance : Insert α (Raw α cmp) where
   insert e s := s.insert e
 
 instance : LawfulSingleton α (Raw α cmp) where
-  insert_emptyc_eq _ := rfl
+  insert_empty_eq _ := rfl
 
 @[inline, inherit_doc TreeSet.empty]
 def containsThenInsert (t : Raw α cmp) (a : α) : Bool × Raw α cmp :=