diff --git a/Std/Data/HashMap/WF.lean b/Std/Data/HashMap/WF.lean
index dce41d1baa..53b9aefaf1 100644
--- a/Std/Data/HashMap/WF.lean
+++ b/Std/Data/HashMap/WF.lean
@@ -278,10 +278,12 @@ theorem WF.mapVal {α β γ} {f : α → β → γ} [BEq α] [Hashable α]
   have ⟨h₁, h₂⟩ := H.out
   simp [Imp.mapVal, Bucket.mapVal, WF_iff, h₁]; refine ⟨?_, ?_, fun i h => ?_⟩
   · simp [Bucket.size]; congr; funext l; simp
-  · simp [List.forall_mem_map_iff, List.pairwise_map]
+  · simp only [Array.map_data, List.forall_mem_map_iff]
+    simp [List.pairwise_map]
     exact fun _ => h₂.1 _
-  · simp [AssocList.All, List.forall_mem_map_iff] at h ⊢
-    exact h₂.2 _ h
+  · simp [AssocList.All] at h ⊢
+    rintro a x hx rfl
+    apply h₂.2 _ _ x hx
 
 theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable α]
     {m : Imp α β} (H : WF m) : WF (filterMap f m) := by
@@ -315,16 +317,14 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable
   simp [Array.mapM_eq_mapM_data, bind, StateT.bind, H2]
   intro bk sz h e'; cases e'
   refine .mk (by simp [Bucket.size]) ⟨?_, fun i h => ?_⟩
-  · simp [List.forall_mem_map_iff]
+  · simp only [List.forall_mem_map_iff, List.toAssocList_toList]
     refine fun l h => (List.pairwise_reverse.2 ?_).imp (mt PartialEquivBEq.symm)
     have := H.out.2.1 _ h
     rw [← List.pairwise_map (R := (¬ · == ·))] at this ⊢
     exact this.sublist (H3 l.toList)
   · simp [Array.getElem_eq_data_get] at h ⊢
     have := H.out.2.2 _ h; simp [AssocList.All] at this ⊢
-    rw [← List.forall_mem_map_iff
-      (P := fun a => ((hash a).toUSize % m.buckets.val.data.length).toNat = i)] at this ⊢
-    exact fun _ h' => this _ ((H3 _).subset h')
+    rintro _ _ h' _ _ rfl; exact this _ h'
 
 end Imp
 
diff --git a/Std/Data/List/Init/Lemmas.lean b/Std/Data/List/Init/Lemmas.lean
index 1b8e158f41..d69ea8d87e 100644
--- a/Std/Data/List/Init/Lemmas.lean
+++ b/Std/Data/List/Init/Lemmas.lean
@@ -15,7 +15,7 @@ These are theorems used in the definitions of `Std.Data.List.Basic`.
 New theorems should be added to `Std.Data.List.Lemmas` if they are not needed by the bootstrap.
 -/
 
-attribute [simp] get get! get? reverseAux eraseIdx map join filterMap dropWhile find? findSome?
+attribute [simp] get get! get? reverseAux eraseIdx map join dropWhile find? findSome?
   replace elem lookup drop take takeWhile foldl foldr zipWith unzip range.loop enumFrom
   intersperse isPrefixOf isEqv dropLast iota mapM.loop mapA List.forM forA filterAuxM
   filterMapM.loop List.foldlM firstM anyM allM findM? findSomeM? forIn.loop forIn'.loop
diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index c196d45eee..3cfba8ee0e 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -68,8 +68,8 @@ theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y ::
 
 theorem mem_singleton_self (a : α) : a ∈ [a] := mem_cons_self _ _
 
-theorem eq_of_mem_singleton : ∀ {a b : α}, a ∈ [b] → a = b
-  | _, _, .head .. => rfl
+theorem eq_of_mem_singleton : a ∈ [b] → a = b
+  | .head .. => rfl
 
 @[simp 1100] theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b :=
   ⟨eq_of_mem_singleton, (by simp [·])⟩
@@ -82,10 +82,25 @@ theorem eq_or_ne_mem_of_mem {a b : α} {l : List α} (h' : a ∈ b :: l) : a = b
 
 theorem ne_nil_of_mem {a : α} {l : List α} (h : a ∈ l) : l ≠ [] := by cases h <;> intro.
 
-theorem mem_constructor : ∀ {a : α} {l : List α}, a ∈ l → ∃ s t : List α, l = s ++ a :: t
-  | _, _, .head l => ⟨[], l, rfl⟩
-  | _, _, .tail b hmem =>
-    let ⟨s, t, h'⟩ := mem_constructor hmem; ⟨b::s, t, by rw [h', cons_append]⟩
+theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l = s ++ a :: t
+  | .head l => ⟨[], l, rfl⟩
+  | .tail b h => let ⟨s, t, h'⟩ := append_of_mem h; ⟨b::s, t, by rw [h', cons_append]⟩
+
+@[simp] theorem elem_iff [DecidableEq α] {a : α} {as : List α} :
+    elem a as ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
+
+theorem mem_of_ne_of_mem {a y : α} {l : List α} (h₁ : a ≠ y) (h₂ : a ∈ y :: l) : a ∈ l :=
+  Or.elim (mem_cons.mp h₂) (absurd · h₁) (·)
+
+theorem ne_of_not_mem_cons {a b : α} {l : List α} : a ∉ b::l → a ≠ b := mt (· ▸ .head _)
+
+theorem not_mem_of_not_mem_cons {a b : α} {l : List α} : a ∉ b::l → a ∉ l := mt (.tail _)
+
+theorem not_mem_cons_of_ne_of_not_mem {a y : α} {l : List α} : a ≠ y → a ∉ l → a ∉ y::l :=
+  mt ∘ mem_of_ne_of_mem
+
+theorem ne_and_not_mem_of_not_mem_cons {a y : α} {l : List α} : a ∉ y::l → a ≠ y ∧ a ∉ l :=
+  fun p => ⟨ne_of_not_mem_cons p, not_mem_of_not_mem_cons p⟩
 
 /-! ### append -/
 
@@ -121,6 +136,9 @@ theorem append_eq_append_iff {a b c d : List α} :
 @[simp] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
   induction s <;> simp_all [or_assoc]
 
+theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t :=
+  mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩
+
 theorem mem_append_eq (a : α) (s t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) :=
   propext mem_append
 
@@ -134,19 +152,19 @@ theorem mem_append_right {a : α} (l₁ : List α) {l₂ : List α} (h : a ∈ l
 
 theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl
 
-theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ b = f a
+@[simp] theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b
   | [] => by simp
-  | b :: l => by simp [mem_map (l := l), or_and_right, exists_or]
+  | _ :: l => by simp [mem_map (l := l), eq_comm (a := b)]
 
 theorem mem_map_of_mem (f : α → β) (h : a ∈ l) : f a ∈ map f l := mem_map.2 ⟨_, h, rfl⟩
 
-theorem exists_of_mem_map (h : b ∈ List.map f l) : ∃ a, a ∈ l ∧ b = f a := mem_map.1 h
+theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h
 
 theorem forall_mem_map_iff {f : α → β} {l : List α} {P : β → Prop} :
     (∀ i ∈ l.map f, P i) ↔ ∀ j ∈ l, P (f j) := by
-  simp [mem_map]; exact ⟨fun H j h => H _ _ h rfl, fun H i x h e => e ▸ H _ h⟩
+  simp; exact ⟨fun H j h => H _ _ h rfl, fun H i x h e => e ▸ H _ h⟩
 
-@[simp] theorem map_eq_nil {f : α → β} {l : List α} : List.map f l = [] ↔ l = [] := by
+@[simp] theorem map_eq_nil {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
   constructor <;> exact fun _ => match l with | [] => rfl
 
 @[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
@@ -171,7 +189,7 @@ theorem mem_join_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ join L := mem_join
 /-! ### bind -/
 
 theorem mem_bind {f : α → List β} {b} {l : List α} : b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
-  simp [List.bind, mem_map, mem_join]
+  simp [List.bind, mem_join]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
 
 theorem exists_of_mem_bind {b : β} {l : List α} {f : α → List β} :
@@ -181,7 +199,7 @@ theorem mem_bind_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a
     b ∈ List.bind l f := mem_bind.2 ⟨a, al, h⟩
 
 theorem bind_map (f : β → γ) (g : α → List β) :
-    ∀ l : List α, List.map f (l.bind g) = l.bind fun a => (g a).map f
+    ∀ l : List α, map f (l.bind g) = l.bind fun a => (g a).map f
   | [] => rfl
   | a::l => by simp only [cons_bind, map_append, bind_map _ _ l]
 
@@ -214,10 +232,8 @@ theorem subset_def {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈
 
 @[simp] theorem nil_subset (l : List α) : [] ⊆ l := fun.
 
--- @[refl]
 @[simp] theorem Subset.refl (l : List α) : l ⊆ l := fun _ i => i
 
--- @[trans]
 theorem Subset.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ :=
   fun _ i => h₂ (h₁ i)
 
@@ -267,6 +283,18 @@ theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧
 
 theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
+theorem eq_replicate_of_mem {a : α} :
+    ∀ {l : List α}, (∀ b ∈ l, b = a) → l = replicate l.length a
+  | [], _ => rfl
+  | b :: l, H => by
+    let ⟨rfl, H₂⟩ := forall_mem_cons.1 H
+    rw [length_cons, replicate, ← eq_replicate_of_mem H₂]
+
+theorem eq_replicate {a : α} {n} {l : List α} :
+    l = replicate n a ↔ length l = n ∧ ∀ b ∈ l, b = a :=
+  ⟨fun h => h ▸ ⟨length_replicate .., fun _ => eq_of_mem_replicate⟩,
+   fun ⟨e, al⟩ => e ▸ eq_replicate_of_mem al⟩
+
 /-! ### getLast -/
 
 theorem getLast_cons' {a : α} {l : List α} : ∀ (h₁ : a :: l ≠ nil) (h₂ : l ≠ nil),
@@ -287,7 +315,7 @@ theorem getLast_concat : (h : concat l a ≠ []) → getLast (concat l a) h = a
   | [] => .slnil
   | a :: l => (nil_sublist l).cons a
 
-/- @[refl] -/ @[simp] theorem Sublist.refl : ∀ l : List α, l <+ l
+@[simp] theorem Sublist.refl : ∀ l : List α, l <+ l
   | [] => .slnil
   | a :: l => (Sublist.refl l).cons₂ a
 
@@ -363,17 +391,41 @@ theorem Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse
 theorem Sublist.append (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) : l₁ ++ r₁ <+ l₂ ++ r₂ :=
   (hl.append_right _).trans ((append_sublist_append_left _).2 hr)
 
-theorem Sublist.subset : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → l₁ ⊆ l₂
-  | _, _, .slnil, _, h => h
-  | _, _, .cons _ s, _, h => .tail _ (s.subset h)
-  | _, _, .cons₂ _ _, _, .head .. => .head ..
-  | _, _, .cons₂ _ s, _, .tail _ h => .tail _ (s.subset h)
+theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂
+  | .slnil, _, h => h
+  | .cons _ s, _, h => .tail _ (s.subset h)
+  | .cons₂ .., _, .head .. => .head ..
+  | .cons₂ _ s, _, .tail _ h => .tail _ (s.subset h)
 
 theorem Sublist.length_le : l₁ <+ l₂ → length l₁ ≤ length l₂
   | .slnil => Nat.le_refl 0
   | .cons _l s => le_succ_of_le (length_le s)
   | .cons₂ _ s => succ_le_succ (length_le s)
 
+@[simp] theorem sublist_nil {l : List α} : l <+ [] ↔ l = [] :=
+  ⟨fun s => subset_nil.mp <| s.subset, fun H => H ▸ Sublist.refl _⟩
+
+theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l₁ = l₂
+  | .slnil, _ => rfl
+  | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _)
+  | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)]
+
+theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ :=
+  s.eq_of_length <| Nat.le_antisymm s.length_le h
+
+@[simp] theorem singleton_sublist {a : α} {l} : [a] <+ l ↔ a ∈ l := by
+  refine ⟨fun h => h.subset (mem_singleton_self _), fun h => ?_⟩
+  obtain ⟨_, _, rfl⟩ := append_of_mem h
+  exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..)
+
+@[simp] theorem replicate_sublist_replicate {m n} (a : α) :
+    replicate m a <+ replicate n a ↔ m ≤ n := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · have := h.length_le; simp only [length_replicate] at this ⊢; exact this
+  · induction h with
+    | refl => apply Sublist.refl
+    | step => simp [*, replicate, Sublist.cons]
+
 /-! ### head -/
 
 theorem head!_of_head? [Inhabited α] : ∀ {l : List α}, head? l = some a → head! l = a
@@ -508,8 +560,7 @@ theorem get?_inj
   | _ :: _, 0 => rfl
   | _ :: l, n+1 => get?_map f l n
 
-@[simp]
-theorem get_map (f : α → β) {l n} : get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) :=
+@[simp] theorem get_map (f : α → β) {l n} : get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) :=
   Option.some.inj <| by rw [← get?_eq_get, get?_map, get?_eq_get]; rfl
 
 /--
@@ -552,7 +603,7 @@ theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.lengt
     l.get ⟨n, get_of_append_proof eq h⟩ = a := Option.some.inj <| by
   rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]; rfl
 
-@[simp] theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (List.replicate n a).get m = a :=
+@[simp] theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a :=
   eq_of_mem_replicate (get_mem _ _ _)
 
 theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
@@ -634,7 +685,7 @@ theorem length_take_le (n) (l : List α) : length (take n l) ≤ n := by simp [N
 
 theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
 
-theorem get_cons_drop : ∀ (l : List α) i, List.get l i :: List.drop (i + 1) l = List.drop i l
+theorem get_cons_drop : ∀ (l : List α) i, get l i :: drop (i + 1) l = drop i l
   | _::_, ⟨0, _⟩ => rfl
   | _::_, ⟨i+1, _⟩ => get_cons_drop _ ⟨i, _⟩
 
@@ -732,7 +783,7 @@ theorem exists_of_set {l : List α} (h : n < l.length) :
 
 theorem exists_of_set' {l : List α} (h : n < l.length) :
     ∃ l₁ l₂, l = l₁ ++ l.get ⟨n, h⟩ :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ :=
-  have ⟨_, _, _, h₁, h₂, h₃⟩ := List.exists_of_set h; ⟨_, _, get_of_append h₁ h₂ ▸ h₁, h₂, h₃⟩
+  have ⟨_, _, _, h₁, h₂, h₃⟩ := exists_of_set h; ⟨_, _, get_of_append h₁ h₂ ▸ h₁, h₂, h₃⟩
 
 theorem get?_set_eq (a : α) (n) (l : List α) : (set l n a).get? n = (fun _ => a) <$> l.get? n := by
   simp only [set_eq_modifyNth, get?_modifyNth_eq]
@@ -775,7 +826,7 @@ theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m →
 @[simp] theorem get_set_ne {l : List α} {i j : Nat} (h : i ≠ j) (a : α)
     (hj : j < (l.set i a).length) :
     (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ := by
-  rw [← Option.some_inj, ← List.get?_eq_get, List.get?_set_ne _ _ h, List.get?_eq_get]
+  rw [← Option.some_inj, ← get?_eq_get, get?_set_ne _ _ h, get?_eq_get]
 
 theorem get_set (a : α) {m n} (l : List α) (h) :
     (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by
@@ -906,7 +957,7 @@ theorem eraseP_append_left {a : α} (pa : p a) :
 theorem eraseP_append_right :
     ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p
   | [],      l₂, _ => rfl
-  | (x::xs), l₂, h => by
+  | x :: xs, l₂, h => by
     simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]
 
 theorem eraseP_sublist (l : List α) : l.eraseP p <+ l := by
@@ -916,12 +967,12 @@ theorem eraseP_sublist (l : List α) : l.eraseP p <+ l := by
 
 theorem eraseP_subset (l : List α) : l.eraseP p ⊆ l := (eraseP_sublist l).subset
 
-theorem Sublist.eraseP : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP p
-  | _, _, .slnil => Sublist.refl _
-  | _, _, .cons a s => by
+theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP p
+  | .slnil => Sublist.refl _
+  | .cons a s => by
     by_cases h : p a <;> simp [h]
     exacts [s.eraseP.trans (eraseP_sublist _), s.eraseP.cons _]
-  | _, _, .cons₂ a s => by
+  | .cons₂ a s => by
     by_cases h : p a <;> simp [h]
     exacts [s, s.eraseP.cons₂ _]
 
@@ -953,6 +1004,7 @@ theorem eraseP_map (f : β → α) : ∀ (l : List β), (map f l).eraseP p = map
 /-! ### erase -/
 
 section erase
+-- FIXME: this should use a `BEq` assumption
 variable [DecidableEq α]
 
 @[simp] theorem erase_nil (a : α) : [].erase a = [] := rfl
@@ -973,6 +1025,9 @@ theorem erase_eq_eraseP (a : α) : ∀ l : List α, l.erase a = l.eraseP (Eq a)
   | b :: l => by
     if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP a l]
 
+theorem Sublist.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₁.erase a <+ l₂.erase a := by
+  simp [erase_eq_eraseP]; exact Sublist.eraseP h
+
 theorem erase_of_not_mem {a : α} : ∀ {l : List α}, a ∉ l → l.erase a = l
   | [], _ => rfl
   | b :: l, h => by
@@ -1029,13 +1084,30 @@ end erase
 
 /-! ### filter and partition -/
 
+@[simp] theorem filter_nil (p : α → Bool) : filter p [] = [] := rfl
+
+@[simp] theorem filter_cons_of_pos {p : α → Bool} {a : α} (l) (pa : p a) :
+    filter p (a :: l) = a :: filter p l := by rw [filter, pa]
+
+@[simp] theorem filter_cons_of_neg {p : α → Bool} {a : α} (l) (pa : ¬ p a) :
+    filter p (a :: l) = filter p l := by rw [filter, eq_false_of_ne_true pa]
+
+@[simp] theorem filter_append {p : α → Bool} :
+    ∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
+  | [], l₂ => rfl
+  | a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
+
+@[simp] theorem filter_sublist {p : α → Bool} : ∀ (l : List α), filter p l <+ l
+  | [] => .slnil
+  | a :: l => by rw [filter]; split <;> simp [Sublist.cons, Sublist.cons₂, filter_sublist l]
+
 theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
   induction as with
   | nil => simp [filter]
   | cons a as ih =>
-    unfold filter; split <;> simp only [*, mem_cons, or_and_right]
-    · exact or_congr_left (and_iff_left_of_imp fun | rfl => ‹_›).symm
-    · exact (or_iff_right fun ⟨rfl, h⟩ => (Bool.not_eq_true _).mpr ‹_› h).symm
+    by_cases h : p a <;> simp [*, or_and_right]
+    · exact or_congr_left (and_iff_left_of_imp fun | rfl => h).symm
+    · exact (or_iff_right fun ⟨rfl, h'⟩ => h h').symm
 
 @[simp] theorem partition_eq_filter_filter (p : α → Bool) (l : List α) :
     partition p l = (filter p l, filter (not ∘ p) l) := by simp [partition, aux] where
@@ -1044,6 +1116,142 @@ theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
   | [] => by simp [partition.loop, filter]
   | a :: l => by cases pa : p a <;> simp [partition.loop, pa, aux, filter, append_assoc]
 
+theorem filter_congr' {p q : α → Bool} :
+    ∀ {l : List α}, (∀ x ∈ l, p x ↔ q x) → filter p l = filter q l
+  | [], _ => rfl
+  | a :: l, h => by
+    rw [forall_mem_cons] at h; by_cases pa : p a
+    · simp [pa, h.1.1 pa, filter_congr' h.2]
+    · simp [pa, mt h.1.2 pa, filter_congr' h.2]
+
+/-! ### filterMap -/
+
+@[simp] theorem filterMap_nil (f : α → Option β) : filterMap f [] = [] := rfl
+
+@[simp] theorem filterMap_cons (f : α → Option β) (a : α) (l : List α) :
+    filterMap f (a :: l) =
+      match f a with
+      | none => filterMap f l
+      | some b => b :: filterMap f l := rfl
+
+theorem filterMap_cons_none {f : α → Option β} (a : α) (l : List α) (h : f a = none) :
+    filterMap f (a :: l) = filterMap f l := by simp only [filterMap, h]
+
+theorem filterMap_cons_some (f : α → Option β) (a : α) (l : List α) {b : β} (h : f a = some b) :
+    filterMap f (a :: l) = b :: filterMap f l := by simp only [filterMap, h]
+
+theorem filterMap_append {α β : Type _} (l l' : List α) (f : α → Option β) :
+    filterMap f (l ++ l') = filterMap f l ++ filterMap f l' := by
+  induction l <;> simp; split <;> simp [*]
+
+theorem filterMap_eq_map (f : α → β) : filterMap (some ∘ f) = map f := by
+  funext l; induction l <;> simp [*]
+
+theorem filterMap_eq_filter (p : α → Bool) :
+    filterMap (Option.guard (p ·)) = filter p := by
+  funext l
+  induction l with
+  | nil => rfl
+  | cons a l IH => by_cases pa : p a <;> simp [Option.guard, pa, ← IH]
+
+theorem filterMap_filterMap (f : α → Option β) (g : β → Option γ) (l : List α) :
+    filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l := by
+  induction l with
+  | nil => rfl
+  | cons a l IH => cases h : f a <;> simp [*]
+
+theorem map_filterMap (f : α → Option β) (g : β → γ) (l : List α) :
+    map g (filterMap f l) = filterMap (fun x => (f x).map g) l := by
+  simp only [← filterMap_eq_map, filterMap_filterMap, Option.map_eq_bind]
+
+theorem filterMap_map (f : α → β) (g : β → Option γ) (l : List α) :
+    filterMap g (map f l) = filterMap (g ∘ f) l := by
+  rw [← filterMap_eq_map, filterMap_filterMap]; rfl
+
+theorem filter_filterMap (f : α → Option β) (p : β → Bool) (l : List α) :
+    filter p (filterMap f l) = filterMap (fun x => (f x).filter p) l := by
+  rw [← filterMap_eq_filter, filterMap_filterMap]
+  congr; funext x; cases f x <;> simp [Option.filter, Option.guard]
+
+theorem filterMap_filter (p : α → Bool) (f : α → Option β) (l : List α) :
+    filterMap f (filter p l) = filterMap (fun x => if p x then f x else none) l := by
+  rw [← filterMap_eq_filter, filterMap_filterMap]
+  congr; funext x; by_cases h : p x <;> simp [Option.guard, h]
+
+@[simp] theorem filterMap_some (l : List α) : filterMap some l = l := by
+  erw [filterMap_eq_map, map_id]
+
+theorem map_filterMap_some_eq_filter_map_is_some (f : α → Option β) (l : List α) :
+    (l.filterMap f).map some = (l.map f).filter fun b => b.isSome := by
+  induction l <;> simp; split <;> simp [*]
+
+@[simp] theorem mem_filterMap (f : α → Option β) (l : List α) {b : β} :
+    b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
+  induction l <;> simp; split <;> simp [*, eq_comm]
+
+@[simp] theorem filterMap_join (f : α → Option β) (L : List (List α)) :
+    filterMap f (join L) = join (map (filterMap f) L) := by
+  induction L <;> simp [*, filterMap_append]
+
+theorem map_filterMap_of_inv (f : α → Option β) (g : β → α) (H : ∀ x : α, (f x).map g = some x)
+    (l : List α) : map g (filterMap f l) = l := by simp only [map_filterMap, H, filterMap_some]
+
+theorem length_filter_le (p : α → Bool) (l : List α) :
+    (l.filter p).length ≤ l.length := (filter_sublist _).length_le
+
+theorem length_filterMap_le (f : α → Option β) (l : List α) :
+    (filterMap f l).length ≤ l.length := by
+  rw [← length_map _ some, map_filterMap_some_eq_filter_map_is_some, ← length_map _ f]
+  apply length_filter_le
+
+theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) : filterMap f l₁ <+ filterMap f l₂ := by
+  induction s <;> simp <;> split <;> simp [*, cons, cons₂]
+
+theorem Sublist.filter {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
+  rw [← filterMap_eq_filter]; apply s.filterMap
+
+theorem map_filter (f : β → α) (l : List β) : filter p (map f l) = map f (filter (p ∘ f) l) := by
+  rw [← filterMap_eq_map, filter_filterMap, filterMap_filter]; rfl
+
+@[simp] theorem filter_filter (q) : ∀ l, filter p (filter q l) = filter (fun a => p a ∧ q a) l
+  | [] => rfl
+  | a :: l => by by_cases hp : p a <;> by_cases hq : q a <;> simp [hp, hq, filter_filter _ l]
+
+theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a ∈ l, ¬p a := by
+  simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
+
+theorem filter_eq_self {l} : filter p l = l ↔ ∀ a ∈ l, p a := by
+  induction l with simp
+  | cons a l ih =>
+    cases h : p a <;> simp [*]
+    intro h; exact Nat.lt_irrefl _ (h ▸ length_filter_le p l)
+
+theorem filter_length_eq_length {l} : (filter p l).length = l.length ↔ ∀ a ∈ l, p a :=
+  Iff.trans ⟨l.filter_sublist.eq_of_length, congrArg length⟩ filter_eq_self
+
+/-! ### find? -/
+
+theorem find?_cons_of_pos (l) (h : p a) : find? p (a :: l) = some a :=
+  by simp [find?, h]
+
+theorem find?_cons_of_neg (l) (h : ¬p a) : find? p (a :: l) = find? p l :=
+  by simp [find?, h]
+
+theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
+  induction l <;> simp; split <;> simp [*]
+
+theorem find?_some : ∀ {l}, find? p l = some a → p a
+  | b :: l, H => by
+    by_cases h : p b <;> simp [find?, h] at H
+    · exact H ▸ h
+    · exact find?_some H
+
+@[simp] theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
+  | b :: l, H => by
+    by_cases h : p b <;> simp [find?, h] at H
+    · exact H ▸ .head _
+    · exact .tail _ (mem_of_find?_eq_some H)
+
 /-! ### pairwise -/
 
 theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
@@ -1052,8 +1260,10 @@ theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
   | .cons₂ _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h)
 
 theorem pairwise_map {l : List α} :
-    (l.map f).Pairwise R ↔ l.Pairwise (fun a b => R (f a) (f b)) := by
-  induction l <;> simp [forall_mem_map_iff, *]
+    (l.map f).Pairwise R ↔ l.Pairwise fun a b => R (f a) (f b) := by
+  induction l
+  . simp
+  . simp only [map, pairwise_cons, forall_mem_map_iff, *]
 
 theorem pairwise_append {l₁ l₂ : List α} :
     (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, R a b := by
@@ -1093,10 +1303,10 @@ theorem disjoint_of_subset_right (ss : l₂ ⊆ l) (d : Disjoint l₁ l) : Disjo
   fun _ m m₁ => d m (ss m₁)
 
 theorem disjoint_of_disjoint_cons_left {l₁ l₂} : Disjoint (a :: l₁) l₂ → Disjoint l₁ l₂ :=
-disjoint_of_subset_left (List.subset_cons _ _)
+disjoint_of_subset_left (subset_cons _ _)
 
 theorem disjoint_of_disjoint_cons_right {l₁ l₂} : Disjoint l₁ (a :: l₂) → Disjoint l₁ l₂ :=
-disjoint_of_subset_right (List.subset_cons _ _)
+disjoint_of_subset_right (subset_cons _ _)
 
 @[simp] theorem disjoint_nil_left (l : List α) : Disjoint [] l := fun a => (not_mem_nil a).elim
 
@@ -1187,8 +1397,8 @@ end union
 /-- List.prod satisfies a specification of cartesian product on lists. -/
 theorem pair_mem_product {xs : List α} {ys : List β} {x : α} {y : β} :
     (x, y) ∈ product xs ys ↔ x ∈ xs ∧ y ∈ ys := by
-  simp only [List.product, and_imp, exists_prop, List.mem_map, Prod.mk.injEq,
-    exists_eq_right_right', List.mem_bind, iff_self]
+  simp only [product, and_imp, exists_prop, mem_map, Prod.mk.injEq,
+    exists_eq_right_right, mem_bind, iff_self]
 
 /-! ### leftpad -/
 
@@ -1220,3 +1430,74 @@ theorem forIn_eq_bindList [Monad m] [LawfulMonad m]
 
 @[simp] theorem forM_append [Monad m] [LawfulMonad m] (l₁ l₂ : List α) (f : α → m PUnit) :
     (l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by induction l₁ <;> simp [*]
+
+/-! ### diff -/
+
+section Diff
+-- TODO: theorems about `BEq`
+variable [DecidableEq α]
+
+@[simp] theorem diff_nil (l : List α) : l.diff [] = l := rfl
+
+@[simp] theorem diff_cons (l₁ l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.erase a).diff l₂ := by
+  simp [List.diff]; split <;> simp [*, erase_of_not_mem]
+
+theorem diff_cons_right (l₁ l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.diff l₂).erase a := by
+  apply Eq.symm; induction l₂ generalizing l₁ <;> simp [erase_comm, *]
+
+theorem diff_erase (l₁ l₂ : List α) (a : α) : (l₁.diff l₂).erase a = (l₁.erase a).diff l₂ := by
+  rw [← diff_cons_right, diff_cons]
+
+@[simp] theorem nil_diff (l : List α) : [].diff l = [] := by
+  induction l <;> simp [*, erase_of_not_mem]
+
+theorem cons_diff (a : α) (l₁ l₂ : List α) :
+    (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂ := by
+  induction l₂ generalizing l₁ with
+  | nil => rfl
+  | cons b l₂ ih => by_cases h : a = b <;> simp [*, eq_comm]
+
+theorem cons_diff_of_mem {a : α} {l₂ : List α} (h : a ∈ l₂) (l₁ : List α) :
+    (a :: l₁).diff l₂ = l₁.diff (l₂.erase a) := by rw [cons_diff, if_pos h]
+
+theorem cons_diff_of_not_mem {a : α} {l₂ : List α} (h : a ∉ l₂) (l₁ : List α) :
+    (a :: l₁).diff l₂ = a :: l₁.diff l₂ := by rw [cons_diff, if_neg h]
+
+theorem diff_eq_foldl : ∀ l₁ l₂ : List α, l₁.diff l₂ = foldl List.erase l₁ l₂
+  | _, [] => rfl
+  | l₁, a :: l₂ => (diff_cons l₁ l₂ a).trans (diff_eq_foldl _ _)
+
+@[simp] theorem diff_append (l₁ l₂ l₃ : List α) : l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃ := by
+  simp only [diff_eq_foldl, foldl_append]
+
+theorem diff_sublist : ∀ l₁ l₂ : List α, l₁.diff l₂ <+ l₁
+  | _, [] => .refl _
+  | l₁, a :: l₂ =>
+    calc
+      l₁.diff (a :: l₂) = (l₁.erase a).diff l₂ := diff_cons ..
+      _ <+ l₁.erase a := diff_sublist ..
+      _ <+ l₁ := erase_sublist ..
+
+theorem diff_subset (l₁ l₂ : List α) : l₁.diff l₂ ⊆ l₁ := (diff_sublist ..).subset
+
+theorem mem_diff_of_mem {a : α} : ∀ {l₁ l₂ : List α}, a ∈ l₁ → a ∉ l₂ → a ∈ l₁.diff l₂
+  | _, [], h₁, _ => h₁
+  | l₁, b :: l₂, h₁, h₂ => by
+    rw [diff_cons]
+    exact mem_diff_of_mem ((mem_erase_of_ne <| ne_of_not_mem_cons h₂).2 h₁) (mt (.tail _) h₂)
+
+theorem Sublist.diff_right : ∀ {l₁ l₂ l₃ : List α}, l₁ <+ l₂ → l₁.diff l₃ <+ l₂.diff l₃
+  | _,  _, [], h => h
+  | l₁, l₂, a :: l₃, h => by simp only [diff_cons, (h.erase _).diff_right]
+
+theorem Sublist.erase_diff_erase_sublist {a : α} :
+    ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → (l₂.erase a).diff (l₁.erase a) <+ l₂.diff l₁
+  | [], l₂, _ => erase_sublist _ _
+  | b :: l₁, l₂, h => by
+    if heq : b = a then
+      simp [heq]
+    else
+      simp [heq, erase_comm a]
+      exact (erase_cons_head b _ ▸ h.erase b).erase_diff_erase_sublist
+
+end Diff