diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 62272a03dc83..2225e85e584a 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -59,6 +59,14 @@ namespace List
 
 open Array
 
+theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
+  cases a with
+  | nil => simpa using h
+  | cons a as =>
+    cases b with
+    | nil => simp at h
+    | cons b bs => simpa using h
+
 @[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
@@ -396,6 +404,11 @@ namespace Array
 
 /-! ## Preliminaries -/
 
+/-! ### toList -/
+
+theorem toList_inj {a b : Array α} (h : a.toList = b.toList) : a = b := by
+  cases a; cases b; simpa using h
+
 /-! ### empty -/
 
 @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 376eaa86cff4..a3d71282a8f5 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -11,6 +11,15 @@ import Init.Data.Vector.Basic
 Lemmas about `Vector α n`
 -/
 
+namespace Array
+
+theorem toVector_inj {a b : Array α} (h₁ : a.size = b.size) (h₂ : a.toVector.cast h₁ = b.toVector) : a = b := by
+  ext i ih₁ ih₂
+  · exact h₁
+  · simpa using congrArg (fun a => a[i]) h₂
+
+end Array
+
 namespace Vector
 
 @[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
@@ -239,6 +248,11 @@ theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by sim
 theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by simp
 
+theorem toList_inj {a b : Vector α n} (h : a.toList = b.toList) : a = b := by
+  rcases a with ⟨⟨a⟩, ha⟩
+  rcases b with ⟨⟨b⟩, hb⟩
+  simpa using h
+
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :