chore(Data/List/Basic): remove some long-deprecated unused lemmas (#1…

…2367)
leanprover-community · Apr 24, 2024 · 72b62af · 72b62af
1 parent 51ee739
commit 72b62af
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 19 deletions.
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -3623,11 +3623,7 @@ theorem get_attach (L : List α) (i) :
       by rw [get_map]
     _ = L.get { val := i, isLt := _ } := by congr 2 <;> simp
 
-set_option linter.deprecated false in
-@[simp, deprecated get_attach]
-theorem nthLe_attach (L : List α) (i) (H : i < L.attach.length) :
-    (L.attach.nthLe i H).1 = L.nthLe i (length_attach L ▸ H) := get_attach ..
-#align list.nth_le_attach List.nthLe_attach
+#align list.nth_le_attach List.get_attach
 
 @[simp 1100]
 theorem mem_map_swap (x : α) (y : β) (xs : List (α × β)) :

diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean
@@ -150,15 +150,7 @@ theorem not_nodup_of_get_eq_of_ne (xs : List α) (n m : Fin xs.length)
     (h : xs.get n = xs.get m) (hne : n ≠ m) : ¬Nodup xs := by
   rw [nodup_iff_injective_get]
   exact fun hinj => hne (hinj h)
-
-set_option linter.deprecated false in
-@[deprecated not_nodup_of_get_eq_of_ne]
-theorem nthLe_eq_of_ne_imp_not_nodup (xs : List α) (n m : ℕ) (hn : n < xs.length)
-    (hm : m < xs.length) (h : xs.nthLe n hn = xs.nthLe m hm) (hne : n ≠ m) : ¬Nodup xs := by
-  rw [nodup_iff_nthLe_inj]
-  simp only [exists_prop, exists_and_right, not_forall]
-  exact ⟨n, m, ⟨hn, hm, h⟩, hne⟩
-#align list.nth_le_eq_of_ne_imp_not_nodup List.nthLe_eq_of_ne_imp_not_nodup
+#align list.nth_le_eq_of_ne_imp_not_nodup List.not_nodup_of_get_eq_of_ne
 
 -- Porting note (#10756): new theorem
 theorem get_indexOf [DecidableEq α] {l : List α} (H : Nodup l) (i : Fin l.length) :

diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean
@@ -559,11 +559,6 @@ theorem perm_lookmap (f : α → Option α) {l₁ l₂ : List α}
     apply h d hd c hc
 #align list.perm_lookmap List.perm_lookmap
 
-@[deprecated Perm.eraseP]
-theorem Perm.erasep (f : α → Prop) [DecidablePred f] {l₁ l₂ : List α}
-    (H : Pairwise (fun a b => f a → f b → False) l₁) (p : l₁ ~ l₂) :
-    List.eraseP f l₁ ~ List.eraseP f l₂ :=
-  p.eraseP f (by simp [H])
 #align list.perm.erasep List.Perm.eraseP
 
 theorem Perm.take_inter {α : Type*} [DecidableEq α] {xs ys : List α} (n : ℕ) (h : xs ~ ys)