feat: port Mathlib.Data.List.Perm (#1478)

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

Mathlib/Data/List/Infix.lean

@@ -680,14 +680,14 @@ theorem insert.def (a : α) (l : List α) : insert a l = if a ∈ l then l else
 #align list.mem_insert_iff List.mem_insert_iff
 
 @[simp]
-theorem suffix_insert (a : α) (l : List α) : l <:+ insert a l := by
+theorem suffix_insert (a : α) (l : List α) : l <:+ l.insert a := by
   by_cases a ∈ l
   · simp only [insert_of_mem h, insert, suffix_refl]
   · simp only [insert_of_not_mem h, suffix_cons, insert]
 
 #align list.suffix_insert List.suffix_insert
 
-theorem infix_insert (a : α) (l : List α) : l <:+: insert a l :=
+theorem infix_insert (a : α) (l : List α) : l <:+: l.insert a :=
   (suffix_insert a l).isInfix
 #align list.infix_insert List.infix_insert
 

Mathlib/Data/List/Nodup.lean

@@ -457,6 +457,19 @@ theorem Nodup.pairwise_coe [IsSymm α r] (hl : l.Nodup) : { a | a ∈ l }.Pairwi
     forall₂_congr this]
 #align list.nodup.pairwise_coe List.Nodup.pairwise_coe
 
+--Porting note: new theorem
+theorem Nodup.take_eq_filter_mem [DecidableEq α] :
+    ∀ {l : List α} {n : ℕ} (_ : l.Nodup), l.take n = l.filter (. ∈ l.take n)
+  | [], n, _ => by simp
+  | b::l, 0, _ => by simp
+  | b::l, n+1, hl => by
+    rw [take_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), List.filter_cons_of_pos]
+    congr 1
+    refine' List.filter_congr' _
+    intro x hx
+    have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
+    simp (config := {contextual := true}) [List.mem_filter, this, hx]
+    simp
 end List
 
 theorem Option.toList_nodup {α} : ∀ o : Option α, o.toList.Nodup