From 2c6cb66edb211cad4bb35749ddcd64a55d4301d9 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Fri, 19 Jul 2024 16:08:14 +0200
Subject: [PATCH] fix: remove typeclass assumptions for Nodup.eraseP

---
 src/Init/Data/List/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 61e75805c433..2ca05842502f 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -3066,7 +3066,7 @@ theorem eraseP_eq_iff {p} {l : List α} :
     (replicate n a).eraseP p = replicate n a := by
   rw [eraseP_of_forall_not (by simp_all)]
 
-theorem Nodup.eraseP [BEq α] [LawfulBEq α] (p) : Nodup l → Nodup (l.eraseP p) :=
+theorem Nodup.eraseP (p) : Nodup l → Nodup (l.eraseP p) :=
   Nodup.sublist <| eraseP_sublist _
 
 theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :