From 9dcbc330fd08a5ae455a6e5a5c6b30b877bb2917 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sun, 5 Jan 2025 10:43:23 +1100
Subject: [PATCH] chore: fix signature of perm_insertIdx (#6532)

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

diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean
index 5eef4cc036..57fc5b45e7 100644
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -510,7 +510,7 @@ theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
     refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
     exact fun h h₁ h₂ => h h₂ h₁
 
-theorem perm_insertIdx [DecidableEq α] {α} (x : α) (l : List α) {n} (h : n ≤ l.length) :
+theorem perm_insertIdx {α} (x : α) (l : List α) {n} (h : n ≤ l.length) :
     insertIdx n x l ~ x :: l := by
   induction l generalizing n with
   | nil =>