From 08acf5a136b19a1a8a0c9870d8ef4e16fb7e4a78 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 21 Jul 2024 09:51:42 +0200
Subject: [PATCH] fix: remove typeclass assumptions for Nodup.eraseP (#4790)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The `α` in the typeclass assumptions wasn't even the element type of the
list.
---
 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 f21b6fd814..d944952612 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -3082,7 +3082,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) :