fix: mis-stated lemmas about empty raw maps

Author: kim-em

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

@@ -219,7 +219,7 @@ theorem containsThenInsertIfNew_snd [TransCmp cmp] (h : t.WF) {k : α} {v : β k
 
 @[simp, grind =]
 theorem get?_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
-    (∅ : DTreeMap α β cmp).get? a = none :=
+    (∅ : Raw α β cmp).get? a = none :=
   Impl.get?_empty
 
 theorem get?_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
@@ -537,7 +537,7 @@ end Const
 
 @[simp, grind =]
 theorem getD_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
-    (∅ : DTreeMap α β cmp).getD a fallback = fallback :=
+    (∅ : Raw α β cmp).getD a fallback = fallback :=
   Impl.getD_empty
 
 theorem getD_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fallback : β a} :
@@ -666,7 +666,7 @@ theorem getD_congr [TransCmp cmp] (h : t.WF) {a b : α} {fallback : β} (hab : c
 end Const
 
 @[simp, grind =]
-theorem getKey?_emptyc {a : α} : (∅ : DTreeMap α β cmp).getKey? a = none :=
+theorem getKey?_emptyc {a : α} : (∅ : Raw α β cmp).getKey? a = none :=
   Impl.getKey?_empty
 
 theorem getKey?_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} :

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

@@ -204,7 +204,7 @@ theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} :
   TreeMap.Raw.size_le_size_erase h
 
 @[simp, grind =]
-theorem get?_emptyc {a : α} : (∅ : TreeSet α cmp).get? a = none :=
+theorem get?_emptyc {a : α} : (∅ : Raw α cmp).get? a = none :=
   TreeMap.Raw.getKey?_emptyc
 
 theorem get?_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} :
@@ -313,7 +313,7 @@ theorem get_eq [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} (h' : k ∈
 
 @[simp, grind =]
 theorem get!_emptyc {a : α} [Inhabited α] :
-    (∅ : TreeSet α cmp).get! a = default :=
+    (∅ : Raw α cmp).get! a = default :=
   TreeMap.Raw.getKey!_emptyc
 
 theorem get!_of_isEmpty [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
@@ -373,7 +373,7 @@ theorem get!_eq_of_mem [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF
 
 @[simp, grind =]
 theorem getD_emptyc {a : α} {fallback : α} :
-    (∅ : TreeSet α cmp).getD a fallback = fallback :=
+    (∅ : Raw α cmp).getD a fallback = fallback :=
   TreeMap.Raw.getKeyD_emptyc
 
 theorem getD_of_isEmpty [TransCmp cmp] (h : t.WF) {a fallback : α} :