fix

src/Init/Data/Array/DecidableEq.lean

@@ -11,7 +11,7 @@ import Init.ByCases
 
 namespace Array
 
-theorem rel_of_isEqvAux
+private theorem rel_of_isEqvAux
     {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
     (heqv : Array.isEqvAux a b hsz r i hi)
     {j : Nat} (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi))) := by
@@ -27,7 +27,7 @@ theorem rel_of_isEqvAux
       subst hj'
       exact heqv.left
 
-theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
+private theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
     (w : ∀ j, (hj : j < i) → r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux a b hsz r i hi := by
   induction i with
   | zero => simp [Array.isEqvAux]
@@ -35,7 +35,8 @@ theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz : a.size
     simp only [isEqvAux, Bool.and_eq_true]
     exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩
 
-theorem rel_of_isEqv {r : α → α → Bool} {a b : Array α} :
+-- This is private as the forward direction of `isEqv_iff_rel` may be used.
+private theorem rel_of_isEqv {r : α → α → Bool} {a b : Array α} :
     Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := by
   simp only [isEqv]
   split <;> rename_i h
@@ -69,7 +70,7 @@ theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun
   have ⟨h, h'⟩ := rel_of_isEqv h
   exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
 
-theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (a : Array α) (i : Nat) (h : i ≤ a.size) :
+private theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (a : Array α) (i : Nat) (h : i ≤ a.size) :
     Array.isEqvAux a a rfl r i h = true := by
   induction i with
   | zero => simp [Array.isEqvAux]

src/Init/Data/Array/Lemmas.lean

@@ -1002,7 +1002,7 @@ private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a ==
   · intro h
     constructor
     · intro a b h
-      obtain ⟨hs, hi⟩ := rel_of_isEqv h
+      obtain ⟨hs, hi⟩ := isEqv_iff_rel.mp h
       ext i h₁ h₂
       · exact hs
       · simpa using hi _ h₁

src/Init/Data/Vector.lean

@@ -9,3 +9,4 @@ import Init.Data.Vector.Lemmas
 import Init.Data.Vector.Lex
 import Init.Data.Vector.MapIdx
 import Init.Data.Vector.Count
+import Init.Data.Vector.DecidableEq

src/Init/Data/Vector/DecidableEq.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Array.DecidableEq
+import Init.Data.Vector.Lemmas
+
+namespace Vector
+
+theorem isEqv_iff_rel {a b : Vector α n} {r} :
+    Vector.isEqv a b r ↔ ∀ (i : Nat) (h' : i < n), r a[i] b[i] := by
+  rcases a with ⟨a, rfl⟩
+  rcases b with ⟨b, h⟩
+  simp [Array.isEqv_iff_rel, h]
+
+theorem isEqv_eq_decide (a b : Vector α n) (r) :
+    Vector.isEqv a b r = decide (∀ (i : Nat) (h' : i < n), r a[i] b[i]) := by
+  rcases a with ⟨a, rfl⟩
+  rcases b with ⟨b, h⟩
+  simp [Array.isEqv_eq_decide, h]
+
+@[simp] theorem isEqv_toArray [BEq α] (a b : Vector α n) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r) := by
+  simp [isEqv_eq_decide, Array.isEqv_eq_decide]
+
+theorem eq_of_isEqv [DecidableEq α] (a b : Vector α n) (h : Vector.isEqv a b (fun x y => x = y)) : a = b := by
+  rcases a with ⟨a, rfl⟩
+  rcases b with ⟨b, h⟩
+  rw [← Vector.toArray_inj]
+  apply Array.eq_of_isEqv
+  simp_all
+
+theorem isEqv_self_beq [BEq α] [ReflBEq α] (a : Vector α n) : Vector.isEqv a a (· == ·) = true := by
+  rcases a with ⟨a, rfl⟩
+  simp [Array.isEqv_self_beq]
+
+theorem isEqv_self [DecidableEq α] (a : Vector α n) : Vector.isEqv a a (· = ·) = true := by
+  rcases a with ⟨a, rfl⟩
+  simp [Array.isEqv_self]
+
+instance [DecidableEq α] : DecidableEq (Vector α n) :=
+  fun a b =>
+    match h:isEqv a b (fun a b => a = b) with
+    | true  => isTrue (eq_of_isEqv a b h)
+    | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
+
+theorem beq_eq_decide [BEq α] (a b : Vector α n) :
+    (a == b) = decide (∀ (i : Nat) (h' : i < n), a[i] == b[i]) := by
+  simp [BEq.beq, isEqv_eq_decide]
+
+@[simp] theorem beq_toArray [BEq α] (a b : Vector α n) : (a.toArray == b.toArray) = (a == b) := by
+  simp [beq_eq_decide, Array.beq_eq_decide]
+
+@[simp] theorem beq_toList [BEq α] (a b : Vector α n) : (a.toList == b.toList) = (a == b) := by
+  simp [beq_eq_decide, List.beq_eq_decide]
+
+end Vector

src/Init/Data/Vector/Lemmas.lean

@@ -1134,7 +1134,7 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
       constructor
       · rintro ⟨a, ha⟩ ⟨b, hb⟩ h
         simp at h
-        obtain ⟨hs, hi⟩ := Array.rel_of_isEqv h
+        obtain ⟨hs, hi⟩ := Array.isEqv_iff_rel.mp h
         ext i h
         · simpa using hi _ (by omega)
       · rintro ⟨a, ha⟩