Remove redudant theorem

Author: jt0202

src/Init/Data/List/Pairwise.lean

@@ -299,14 +299,6 @@ grind_pattern Nodup.sublist => l₁ <+ l₂, Nodup l₂
 theorem Sublist.nodup : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Nodup.sublist
 
-theorem nodup_filter_of_nodup {α : Type u} {l : List α} (h : l.Nodup) {p : α → Bool} :
-    (l.filter p).Nodup := by
-  induction l with
-  | nil => simp
-  | cons hd tl ih =>
-    simp only [List.nodup_cons, List.filter] at h ⊢
-    split <;> simp [h, ih]
-
 theorem getElem?_inj {xs : List α}
     (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs[i]? = xs[j]?) : i = j := by
   induction xs generalizing i j with

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -5301,9 +5301,8 @@ theorem fst_partition_equiv_filter [EquivBEq α] [LawfulHashable α]
   rw [equiv_iff_toList_perm_toList]
   apply List.Perm.trans _ (toList_filter m).symm
   apply List.Perm.of_nodup_of_nodup_of_forall_mem_iff_mem
-  · apply nodup_toList
-    apply Raw.WF.fst_partition₀
-  · apply List.nodup_filter_of_nodup (nodup_toList _ h)
+  · apply nodup_toList _ Raw.WF.fst_partition₀
+  · apply List.Sublist.nodup List.filter_sublist (nodup_toList m h)
   · intro a
     simp [mem_toList_fst_partition _ h]