fix: remove List.erase_of_forall_bne and replace with List.erase_eq_s…

…elf_iff_forall_bne (#967)

Batteries/Data/Array/Lemmas.lean

@@ -165,8 +165,8 @@ theorem eraseIdx_data_swap {l : Array α} (i : Nat) (lt : i + 1 < size l) :
   | none =>
     simp only [erase, h]
     apply Eq.symm
-    apply List.erase_of_forall_bne
-    rw [←List.indexOf?_eq_none_iff, indexOf?_data, h, Option.map_none']
+    rw [List.erase_eq_self_iff_forall_bne, ←List.indexOf?_eq_none_iff, indexOf?_data,
+        h, Option.map_none']
   | some i =>
     simp only [erase, h]
     rw [data_feraseIdx, ←List.eraseIdx_indexOf_eq_erase]

Batteries/Data/List/Lemmas.lean

@@ -244,11 +244,9 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
 
 @[deprecated (since := "2024-04-22")] alias sublist.erase := Sublist.erase
 
-theorem erase_of_forall_bne [BEq α] (a : α) (xs : List α) (h : ∀ (x : α), x ∈ xs → ¬x == a) :
-    xs.erase a = xs := by
-  rw [erase_eq_eraseP', eraseP_of_forall_not h]
-
--- TODO a version of the above theorem with LawfulBEq and ∉
+theorem erase_eq_self_iff_forall_bne [BEq α] (a : α) (xs : List α) :
+    xs.erase a = xs ↔ ∀ (x : α), x ∈ xs → ¬x == a := by
+  rw [erase_eq_eraseP', eraseP_eq_self_iff]
 
 /-! ### findIdx? -/