.

src/Init/Data/ByteArray/Basic.lean

@@ -34,6 +34,12 @@ instance : Inhabited ByteArray where
 instance : EmptyCollection ByteArray where
   emptyCollection := ByteArray.empty
 
+@[simp, grind =]
+theorem empty_eq_emptyc : @empty = ∅ := rfl
+
+@[simp, grind =]
+theorem emptyWithCapacity_eq_emptyc : @emptyWithCapacity n = ∅ := rfl
+
 @[extern "lean_sarray_size", simp]
 def usize (a : @& ByteArray) : USize :=
   a.size.toUSize

src/Init/Data/ByteArray/Lemmas.lean

@@ -11,9 +11,11 @@ public import Init.Data.Array.Extract
 
 public section
 
-@[simp]
 theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
 
+@[simp]
+theorem ByteArray.data_emptyc : (∅ : ByteArray).data = #[] := rfl
+
 @[simp]
 theorem ByteArray.data_extract {a : ByteArray} {b e : Nat} :
     (a.extract b e).data = a.data.extract b e := by
@@ -28,7 +30,7 @@ theorem ByteArray.extract_zero_size {b : ByteArray} : b.extract 0 b.size = b :=
   simp
 
 @[simp]
-theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by
+theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = ∅ := by
   ext1
   simp [Nat.min_le_left]
 
@@ -50,16 +52,19 @@ theorem ByteArray.data_append {l l' : ByteArray} :
     (l ++ l').data = l.data ++ l'.data := by
   simp [← Array.toList_inj]
 
-@[simp]
 theorem ByteArray.size_empty : ByteArray.empty.size = 0 := by
   simp [← ByteArray.size_data]
 
+@[simp]
+theorem ByteArray.size_emptyc : (∅ : ByteArray).size = 0 := by
+  simp [← ByteArray.size_data]
+
 @[simp]
 theorem List.data_toByteArray {l : List UInt8} :
     l.toByteArray.data = l.toArray := by
   rw [List.toByteArray]
   suffices ∀ a b, (List.toByteArray.loop a b).data = b.data ++ a.toArray by
-    simpa using this l ByteArray.empty
+    simpa using this l ∅
   intro a b
   fun_induction List.toByteArray.loop a b with simp_all
 
@@ -69,15 +74,15 @@ theorem List.size_toByteArray {l : List UInt8} :
   simp [← ByteArray.size_data]
 
 @[simp]
-theorem List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl
+theorem List.toByteArray_nil : List.toByteArray [] = ∅ := rfl
 
 @[simp]
-theorem ByteArray.empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by
+theorem ByteArray.empty_append {b : ByteArray} : ∅ ++ b = b := by
   ext1
   simp
 
 @[simp]
-theorem ByteArray.append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by
+theorem ByteArray.append_empty {b : ByteArray} : b ++ ∅ = b := by
   ext1
   simp
 
@@ -86,7 +91,7 @@ theorem ByteArray.size_append {a b : ByteArray} : (a ++ b).size = a.size + b.siz
   simp [← size_data]
 
 @[simp]
-theorem ByteArray.size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ByteArray.empty := by
+theorem ByteArray.size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ∅ := by
   refine ⟨fun h => ?_, fun h => h ▸ ByteArray.size_empty⟩
   ext1
   simp [← Array.size_eq_zero_iff, h]
@@ -121,23 +126,23 @@ theorem ByteArray.size_extract {a : ByteArray} {b e : Nat} :
   simp [← size_data]
 
 @[simp]
-theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ByteArray.empty ↔ min j b.size ≤ i := by
+theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ∅ ↔ min j b.size ≤ i := by
   rw [← size_eq_zero_iff, size_extract]
   omega
 
 @[simp]
-theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ByteArray.empty := by
+theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ∅ := by
   simp only [extract_eq_empty_iff]
   exact Nat.le_trans (Nat.min_le_left _ _) (by simp)
 
 @[simp]
 theorem ByteArray.append_eq_empty_iff {a b : ByteArray} :
-    a ++ b = ByteArray.empty ↔ a = ByteArray.empty ∧ b = ByteArray.empty := by
+    a ++ b = ∅ ↔ a = ∅ ∧ b = ∅ := by
   simp [← size_eq_zero_iff, size_append]
 
 @[simp]
 theorem List.toByteArray_eq_empty {l : List UInt8} :
-    l.toByteArray = ByteArray.empty ↔ l = [] := by
+    l.toByteArray = ∅ ↔ l = [] := by
   simp [← ByteArray.size_eq_zero_iff]
 
 theorem ByteArray.append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) :
@@ -242,8 +247,10 @@ theorem ByteArray.append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c)
   simp
 
 @[simp]
-theorem ByteArray.toList_empty : ByteArray.empty.toList = [] := by
-  simp [ByteArray.toList, ByteArray.toList.loop]
+theorem ByteArray.toList_empty : (∅ : ByteArray).toList = [] := by
+  simp [ByteArray.toList]
+  rw [toList.loop]
+  simp
 
 theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {destOff len : Nat} {exact : Bool} :
     ByteArray.copySlice src srcOff dest destOff len exact =