From 883bff1e168d81f90ef02b92149977f7d2afa563 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 12 Mar 2025 08:12:30 +0100
Subject: [PATCH] chore: rename `insert_emptyc_eq` to `insert_empty_eq`

---
 src/Init/Core.lean                   | 17 ++++++++++++++---
 src/Std/Data/DTreeMap/Basic.lean     |  2 +-
 src/Std/Data/DTreeMap/Raw/Basic.lean |  2 +-
 src/Std/Data/TreeMap/Basic.lean      |  2 +-
 src/Std/Data/TreeMap/Raw/Basic.lean  |  2 +-
 src/Std/Data/TreeSet/Basic.lean      |  2 +-
 src/Std/Data/TreeSet/Raw/Basic.lean  |  2 +-
 7 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index beb28d662d12..597a25dbe181 100644
--- a/src/Init/Core.lean
+++ b/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
diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean
index db628f42d4dd..0c6006639eb3 100644
--- a/src/Std/Data/DTreeMap/Basic.lean
+++ b/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,
diff --git a/src/Std/Data/DTreeMap/Raw/Basic.lean b/src/Std/Data/DTreeMap/Raw/Basic.lean
index 708650c4f198..14e259a745c0 100644
--- a/src/Std/Data/DTreeMap/Raw/Basic.lean
+++ b/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 :=
diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean
index 7b4bc88ccd8c..d679605ad577 100644
--- a/src/Std/Data/TreeMap/Basic.lean
+++ b/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 :=
diff --git a/src/Std/Data/TreeMap/Raw/Basic.lean b/src/Std/Data/TreeMap/Raw/Basic.lean
index b27cc864d43f..5e40795e6582 100644
--- a/src/Std/Data/TreeMap/Raw/Basic.lean
+++ b/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 :=
diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean
index d87d251fac1d..65bc5fda0c67 100644
--- a/src/Std/Data/TreeSet/Basic.lean
+++ b/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.
diff --git a/src/Std/Data/TreeSet/Raw/Basic.lean b/src/Std/Data/TreeSet/Raw/Basic.lean
index bc814b1b6b78..a1418d233af0 100644
--- a/src/Std/Data/TreeSet/Raw/Basic.lean
+++ b/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 :=