From 8311edc805fe01405a1a28de83ec9bfddeb3aefa Mon Sep 17 00:00:00 2001
From: Seppel3210 <34406239+Seppel3210@users.noreply.github.com>
Date: Sat, 28 Sep 2024 17:14:03 +0200
Subject: [PATCH] fix: remove List.erase_of_forall_bne and replace with
 List.erase_eq_self_iff_forall_bne (#967)

---
 Batteries/Data/Array/Lemmas.lean | 4 ++--
 Batteries/Data/List/Lemmas.lean  | 8 +++-----
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 869c35b37e..d384a334ab 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/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]
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index d211cb04f8..5df9338026 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/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? -/