congruence lemma

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

src/Init/Data/List/Lemmas.lean

@@ -1053,6 +1053,9 @@ theorem getLast?_tail {l : List α} : (tail l).getLast? = if l.length = 1 then n
   | nil => simp [List.map]
   | cons _ as ih => simp [List.map, ih]
 
+@[simp] theorem isEmpty_map {l : List α} {f : α → β} : (l.map f).isEmpty = l.isEmpty := by
+  cases l <;> simp
+
 @[simp] theorem getElem?_map {f : α → β} : ∀ {l : List α} {i : Nat}, (map f l)[i]? = Option.map f l[i]?
   | [], _ => rfl
   | _ :: _, 0 => by simp

src/Init/Data/Option/Attach.lean

@@ -257,6 +257,15 @@ and simplifies these to the function directly taking the value.
     o.map f = o.unattach.map g := by
   cases o <;> simp [hf]
 
+theorem Option.map_subtype' {α β : Type _} {o : Option α}
+    {f : α → β} : o.attach.map (fun a => f a.1) = o.map f := by
+  cases o <;> rfl
+
+theorem Option.map_subtype'' {α β : Type _} {o : Option α}
+    {f : { x // x ∈ o } → β} {g : α → β} (hf : ∀ (x : α) (h : x ∈ o), f ⟨x, h⟩ = g x) :
+    Option.map f o.attach = Option.map g o := by
+  rw [Option.map_subtype hf, Option.unattach_attach]
+
 @[simp] theorem bind_subtype {p : α → Prop} {o : Option { x // p x }}
     {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (o.bind f) = o.unattach.bind g := by

src/Init/Data/Option/Instances.lean

@@ -144,6 +144,13 @@ none
   | none => b
   | some a => f a rfl
 
+/-- Partial filter. If `o : Option α`, `p : (a : α) → a ∈ x → Bool`, then `o.pfilter p` is
+the same as `o.filter p` but `p` is passed the proof that `a ∈ o`. -/
+@[inline] def pfilter (o : Option α) (p : (a : α) → o = some a → Bool) : Option α :=
+  match o with
+  | none => none
+  | some a => bif p a rfl then o else none
+
 /--
 Executes a monadic action on an optional value if it is present, or does nothing if there is no
 value.

src/Init/Data/Option/Lemmas.lean

@@ -59,6 +59,15 @@ theorem get!_eq_getD [Inhabited α] (o : Option α) : o.get! = o.getD default :=
 
 @[deprecated get!_eq_getD (since := "2024-11-18")] abbrev get!_eq_getD_default := @get!_eq_getD
 
+theorem get_congr {o o' : Option α} {ho : o.isSome} (h : o = o') :
+    o.get ho = o'.get (h ▸ ho) := by
+  cases h; rfl
+
+theorem get_inj {o1 o2 : Option α} {h1} {h2} :
+    o1.get h1 = o2.get h2 ↔ o1 = o2 := by
+  match o1, o2, h1, h2 with
+  | some a, some b, _, _ => simp only [Option.get_some, Option.some.injEq]
+
 theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b :=
   some.inj <| ha ▸ hb
 
@@ -75,6 +84,12 @@ theorem isSome_iff_exists : isSome x ↔ ∃ a, x = some a := by cases x <;> sim
 theorem isSome_eq_isSome : (isSome x = isSome y) ↔ (x = none ↔ y = none) := by
   cases x <;> cases y <;> simp
 
+theorem isSome_of_mem {x : Option α} {y : α} (h : y ∈ x) : x.isSome := by
+  cases x <;> trivial
+
+theorem isSome_of_eq_some {x : Option α} {y : α} (h : x = some y) : x.isSome := by
+  cases x <;> trivial
+
 @[simp] theorem not_isSome : isSome a = false ↔ a.isNone = true := by
   cases a <;> simp
 
@@ -142,6 +157,23 @@ theorem bind_congr {α β} {o : Option α} {f g : α → Option β} :
     (h : ∀ a, o = some a → f a = g a) → o.bind f = o.bind g := by
   cases o <;> simp
 
+theorem isSome_bind {α β : Type _} (x : Option α) (f : α → Option β) :
+    (x.bind f).isSome = x.any (fun x => (f x).isSome) := by
+  cases x <;> rfl
+
+theorem isSome_of_isSome_bind {α β : Type _} {x : Option α} {f : α → Option β}
+    (h : (x.bind f).isSome) : x.isSome := by
+  cases x <;> trivial
+
+theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α → Option β}
+    (h : (x.bind f).isSome) : (f (x.get (isSome_of_isSome_bind h))).isSome := by
+  cases x <;> trivial
+
+theorem get_bind {α β : Type _} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome) :
+    (x.bind f).get h = (f (x.get (isSome_of_isSome_bind h))).get
+      (isSome_apply_of_isSome_bind h) := by
+  cases x <;> trivial
+
 theorem join_eq_some : x.join = some a ↔ x = some (some a) := by
   simp [bind_eq_some]
 
@@ -262,6 +294,10 @@ theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
     a ∈ o.filter p ↔ a ∈ o ∧ p a := by
   simp
 
+theorem filter_eq_bind (x : Option α) (p : α → Bool) :
+    x.filter p = x.bind (Option.guard (fun a => p a)) := by
+  cases x <;> rfl
+
 @[simp] theorem all_guard (p : α → Prop) [DecidablePred p] (a : α) :
     Option.all q (guard p a) = (!p a || q a) := by
   simp only [guard]
@@ -272,6 +308,21 @@ theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
   simp only [guard]
   split <;> simp_all
 
+theorem all_eq_true (p : α → Bool) (x : Option α) :
+    x.all p = true ↔ ∀ y, x = some y → p y := by
+  cases x <;> simp
+
+theorem any_eq_true (p : α → Bool) (x : Option α) :
+    x.any p = true ↔ ∃ y, x = some y ∧  p y := by
+  cases x <;> simp
+
+theorem isSome_of_any {x : Option α} {p : α → Bool} (h : x.any p) : x.isSome := by
+  cases x <;> trivial
+
+theorem any_map {α β : Type _} {x : Option α} {f : α → β} {p : β → Bool} :
+    (x.map f).any p = x.any (fun a => p (f a)) := by
+  cases x <;> rfl
+
 theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
     x.bind (Option.map f) = (x.map (Option.map f)).bind id := by cases x <;> simp
 
@@ -335,6 +386,15 @@ theorem guard_comp {p : α → Prop} [DecidablePred p] {f : β → α} :
   ext1 b
   simp [guard]
 
+theorem bind_guard (x : Option α) (p : α → Prop) [DecidablePred p] :
+    x.bind (Option.guard p) = x.filter p := by
+  simp only [Option.filter_eq_bind, decide_eq_true_eq]
+
+theorem guard_eq_map (p : α  → Prop) [DecidablePred p] :
+    Option.guard p = fun x => Option.map (fun _ => x) (if p x then some x else none) := by
+  funext x
+  simp [Option.guard]
+
 theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
     ∀ o₁ o₂, liftOrGet f o₁ o₂ = o₁ ∨ liftOrGet f o₁ o₂ = o₂
   | none, none => .inl rfl
@@ -585,6 +645,20 @@ theorem mem_ite_none_right {x : α} [Decidable p] {l : Option α} :
 
 end ite
 
+theorem isSome_filter {α : Type _} {x : Option α} {f : α → Bool} :
+    (x.filter f).isSome = x.any f := by
+  cases x
+  · rfl
+  · rw [Bool.eq_iff_iff]
+    simp only [Option.any_some, Option.filter, Option.isSome_ite]
+
+theorem get_filter {α : Type _} {x : Option α} {f : α → Bool} (h : (x.filter f).isSome) :
+    (x.filter f).get h = x.get (isSome_of_isSome_filter f x h) := by
+  cases x
+  · contradiction
+  · unfold Option.filter
+    simp only [Option.get_ite, Option.get_some]
+
 /-! ### pbind -/
 
 @[simp] theorem pbind_none : pbind none f = none := rfl
@@ -691,6 +765,65 @@ theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p
        o.pelim g (fun a h => g' (f a (H a h))) := by
   cases o <;> simp
 
+/-! ### pfilter -/
+
+@[congr]
+theorem pfilter_congr {α : Type u} {o o' : Option α} (ho : o = o')
+    {f : (a : α) → o = some a → Bool} {g : (a : α) → o' = some a → Bool}
+    (hf : ∀ a ha, f a (ho.trans ha) = g a ha) :
+    o.pfilter f = o'.pfilter g := by
+  cases ho
+  congr; funext a ha
+  exact hf a ha
+
+theorem pfilter_none {α : Type _} {p : (a : α) → none = some a → Bool} :
+    none.pfilter p = none := by
+  simp [pfilter]
+
+theorem pfilter_some {α : Type _} {x : α} {p : (a : α) → some x = some a → Bool} :
+    (some x).pfilter p = if p x rfl then some x else none := by
+  simp [pfilter]
+
+theorem pfilter_eq_none {α : Type _} {o : Option α} {p : (a : α) → o = some a → Bool} :
+    o.pfilter p = none ↔ o = none ∨ ∃ (a : α) (ha : a ∈ o), p a ha = false := by
+  simp [Option.pfilter]
+  cases o with
+  | none => simp
+  | some a' =>
+    simp only [cond_eq_if, ite_eq_right_iff, reduceCtorEq, imp_false, Bool.not_eq_true,
+      Option.some.injEq, false_or]
+    constructor
+    · intro h
+      exists a'
+      exists rfl
+    · intro h
+      rcases h with ⟨a, ha, h⟩
+      simp [ha, h]
+
+theorem pfilter_eq_some {α : Type _} {o : Option α} {p : (a : α) → o = some a → Bool}
+    {a : α} (ha : a ∈ o) :
+    o.pfilter p = some a ↔ p a ha = true := by
+  simp only [Option.pfilter]
+  cases o with
+  | none => simp at ha
+  | some a' =>
+    simp only [Option.mem_def, Option.some.injEq] at ha
+    simp [cond_eq_if, ha]
+
+theorem pfilter_eq_filter {α : Type _} {o : Option α} {p : α → Bool} :
+    o.pfilter (fun a _ => p a) = o.filter p := by
+  cases o with
+  | none => simp [Option.pfilter]
+  | some a =>
+    simp [Option.pfilter, Option.filter]
+
+theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
+    {p : (a : α) → o = some a → Bool} :
+    o.pfilter p = o.pbind (fun a h => if p a h then some a else none) := by
+  cases o
+  · rfl
+  · simp only [Option.pfilter, Bool.cond_eq_ite, Option.pbind_some]
+
 /-! ### LT and LE -/
 
 @[simp] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]

src/Std/Data/DHashMap/AdditionalOperations.lean

@@ -31,23 +31,20 @@ open Internal.Raw
 
 theorem WF.filterMap [BEq α] [Hashable α] {m : Raw α β} (h : m.WF)
     {f : (a : α) → β a → Option (δ a)} : (m.filterMap f).WF := by
-  simpa only [filterMap_eq h] using
-    .wf (Raw₀.filterMap f ⟨m, h.size_buckets_pos⟩).2 (Raw₀.wfImp_filterMap (WF.out h))
+  simpa only [filterMap_eq h] using Raw₀.wf_filterMap₀ h
 
 theorem WF.map [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → δ a} :
     (m.map f).WF := by
-  simpa only [map_eq h] using .wf (Raw₀.map f ⟨m, h.size_buckets_pos⟩).2 (Raw₀.wfImp_map (WF.out h))
+  simpa only [map_eq h] using Raw₀.wf_map₀ h
 
 end Raw
 
 @[inline, inherit_doc Raw.filterMap] def filterMap [BEq α] [Hashable α]
     (f : (a : α) → β a → Option (δ a)) (m : DHashMap α β) : DHashMap α δ :=
-  ⟨Raw₀.filterMap f ⟨m.1, m.2.size_buckets_pos⟩,
-   .wf (Raw₀.filterMap f ⟨m.1, m.2.size_buckets_pos⟩).2 (Raw₀.wfImp_filterMap (Raw.WF.out m.2))⟩
+  ⟨Raw₀.filterMap f ⟨m.1, m.2.size_buckets_pos⟩, Raw₀.wf_filterMap₀ m.2⟩
 
 @[inline, inherit_doc Raw.map] def map [BEq α] [Hashable α] (f : (a : α) → β a → δ a)
     (m : DHashMap α β) : DHashMap α δ :=
-  ⟨Raw₀.map f ⟨m.1, m.2.size_buckets_pos⟩,
-   .wf (Raw₀.map f ⟨m.1, m.2.size_buckets_pos⟩).2 (Raw₀.wfImp_map (Raw.WF.out m.2))⟩
+  ⟨Raw₀.map f ⟨m.1, m.2.size_buckets_pos⟩, Raw₀.wf_map₀ m.2⟩
 
 end Std.DHashMap

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

@@ -97,8 +97,7 @@ macro_rules
       | apply Raw.WF.constAlter₀ | apply Raw.WF.constModify₀
       | apply Raw₀.wf_insertMany₀ | apply Raw₀.Const.wf_insertMany₀
       | apply Raw₀.Const.wf_insertManyIfNewUnit₀
-      | apply Raw.WF.filter₀
-      -- TODO: map₀ and filterMap₀
+      | apply Raw.WF.filter₀ | apply Raw₀.wf_map₀ | apply Raw₀.wf_filterMap₀
       | apply Raw.WF.emptyWithCapacity₀) <;> wf_trivial)
 
 /-- Internal implementation detail of the hash map -/
@@ -122,6 +121,10 @@ private def modifyMap : Std.DHashMap Name (fun _ => Name) :=
      ⟨`map, ``toListModel_map⟩,
      ⟨`filterMap, ``toListModel_filterMap⟩]
 
+private theorem perm_map_congr_left {α : Type u} {β : Type v} {l l' : List α} {f : α → β}
+    {l₂ : List β} (h : l.Perm l') : (l.map f).Perm l₂ ↔ (l'.map f).Perm l₂ :=
+  (h.map f).congr_left _
+
 private def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (TSyntax `term))) :=
   .ofList
     [⟨`isEmpty, (``Raw.isEmpty_eq_isEmpty, #[`(_root_.List.Perm.isEmpty_eq)])⟩,
@@ -141,7 +144,7 @@ private def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (TSynta
      ⟨`getKey!, (``getKey!_eq_getKey!, #[`(getKey!_of_perm _)])⟩,
      ⟨`toList, (``Raw.toList_eq_toListModel, #[])⟩,
      ⟨`keys, (``Raw.keys_eq_keys_toListModel, #[])⟩,
-     ⟨`Const.toList, (``Raw.Const.toList_eq_toListModel_map, #[])⟩,
+     ⟨`Const.toList, (``Raw.Const.toList_eq_toListModel_map, #[`(perm_map_congr_left)])⟩,
      ⟨`foldM, (``Raw.foldM_eq_foldlM_toListModel, #[])⟩,
      ⟨`fold, (``Raw.fold_eq_foldl_toListModel, #[])⟩,
      ⟨`foldRevM, (``Raw.foldRevM_eq_foldrM_toListModel, #[])⟩,
@@ -666,6 +669,11 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.1.WF
     m.contains a = (m.getKey? a).isSome := by
   simp_to_model [getKey?, contains] using List.containsKey_eq_isSome_getKey?
 
+theorem contains_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
+    {a a' : α} (h : m.1.WF) :
+    m.getKey? a = some a' → m.contains a' = true := by
+  simp_to_model using List.containsKey_of_getKey?_eq_some
+
 theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
     m.contains a = false → m.getKey? a = none := by
   simp_to_model [getKey?, contains] using List.getKey?_eq_none
@@ -3065,6 +3073,500 @@ end Const
 
 end Equiv
 
+section filterMap
+
+variable {γ : α → Type w}
+
+theorem isEmpty_filterMap_iff [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} (h : m.1.WF) :
+    (m.filterMap f).1.isEmpty = true ↔
+      ∀ (k : α) (h : m.contains k = true), f k (m.get k h) = none := by
+  simp_to_model [filterMap] using List.isEmpty_filterMap_eq_true
+
+theorem isEmpty_filterMap_eq_false_iff [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} (h : m.1.WF) :
+    (m.filterMap f).1.isEmpty = false ↔
+      ∃ (k : α) (h : m.contains k = true), (f k (m.get k h)).isSome := by
+  simp_to_model [filterMap] using List.isEmpty_filterMap_eq_false
+
+theorem contains_filterMap [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.1.WF) :
+    (m.filterMap f).contains k = (m.get? k).any (f k · |>.isSome) := by
+  simp_to_model [filterMap] using List.containsKey_filterMap
+
+theorem contains_of_contains_filterMap [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.1.WF) :
+    (m.filterMap f).contains k = true → m.contains k = true := by
+  simp_to_model [filterMap] using containsKey_of_containsKey_filterMap
+
+theorem size_filterMap_le_size [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Option (γ a)} (h : m.1.WF) :
+    (m.filterMap f).1.size ≤ m.1.size := by
+  simp_to_model [filterMap] using List.length_filterMap_le
+
+theorem size_filterMap_eq_size_iff [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} (h : m.1.WF) :
+    (m.filterMap f).1.size = m.1.size ↔ ∀ (a : α) (h : m.contains a), (f a (m.get a h)).isSome := by
+  simp_to_model [filterMap] using List.length_filterMap_eq_length_iff
+
+theorem get?_filterMap [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.1.WF) :
+    (m.filterMap f).get? k = (m.get? k).bind (f k) := by
+  simp_to_model [filterMap] using List.getValueCast?_filterMap
+
+theorem isSome_apply_of_contains_filterMap [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.1.WF) :
+    ∀ (h' : (m.filterMap f).contains k = true),
+      (f k (m.get k (contains_of_contains_filterMap m h h'))).isSome := by
+  simp_to_model [filterMap] using List.isSome_apply_of_containsKey_filterMap
+
+theorem get_filterMap [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.1.WF) {h'} :
+    (m.filterMap f).get k h' =
+      (f k (m.get k (contains_of_contains_filterMap m h h'))).get
+        (isSome_apply_of_contains_filterMap m h h') := by
+  simp_to_model [filterMap] using List.getValueCast_filterMap
+
+theorem get!_filterMap [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} [Inhabited (γ k)] (h : m.1.WF) :
+    (m.filterMap f).get! k = ((m.get? k).bind (f k)).get! := by
+  simp_to_model [filterMap] using List.getValueCast!_filterMap
+
+theorem getD_filterMap [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k} (h : m.1.WF) :
+    (m.filterMap f).getD k fallback = ((m.get? k).bind (f k)).getD fallback := by
+  simp_to_model [filterMap] using List.getValueCastD_filterMap
+
+omit [BEq α] [Hashable α] in
+theorem toList_filterMap
+    {f : (a : α) → β a → Option (γ a)} :
+    (m.filterMap f).1.toList.Perm
+      (m.1.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩))) := by
+  simp_to_model [filterMap, toList, Equiv] using List.Perm.rfl
+
+theorem getKey?_filterMap [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.1.WF) :
+    (m.filterMap f).getKey? k =
+    (m.getKey? k).pfilter (fun x h' =>
+      (f x (m.get x (contains_of_getKey?_eq_some m h h'))).isSome) := by
+  simp_to_model [filterMap] using List.getKey?_filterMap
+
+theorem getKey_filterMap [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.1.WF) {h'}:
+    (m.filterMap f).getKey k h' = m.getKey k (contains_of_contains_filterMap m h h') := by
+  simp_to_model [filterMap] using List.getKey_filterMap
+
+theorem getKey!_filterMap [LawfulBEq α] [Inhabited α]
+    {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.1.WF) :
+    (m.filterMap f).getKey! k =
+    ((m.getKey? k).pfilter (fun x h' =>
+      (f x (m.get x (contains_of_getKey?_eq_some m h h'))).isSome)).get! := by
+  simp_to_model [filterMap] using List.getKey!_filterMap
+
+theorem getKeyD_filterMap [LawfulBEq α]
+    {f : (a : α) → β a → Option (γ a)} {k fallback : α} (h : m.1.WF) :
+    (m.filterMap f).getKeyD k fallback =
+    ((m.getKey? k).pfilter (fun x h' =>
+      (f x (m.get x (contains_of_getKey?_eq_some m h h'))).isSome)).getD fallback := by
+  simp_to_model [filterMap] using List.getKeyD_filterMap
+
+namespace Const
+
+variable {β : Type v} {γ : Type w} (m : Raw₀ α (fun _ => β))
+
+theorem isEmpty_filterMap_iff [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} (h : m.1.WF) :
+    (m.filterMap f).1.isEmpty = true ↔
+      ∀ (k : α) (h : m.contains k = true), f (m.getKey k h) (Const.get m k h) = none := by
+  simp_to_model [filterMap] using List.Const.isEmpty_filterMap_eq_true
+
+theorem isEmpty_filterMap_eq_false_iff [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} (h : m.1.WF) :
+    (m.filterMap f).1.isEmpty = false ↔
+      ∃ (k : α) (h : m.contains k = true), (f (m.getKey k h) (Const.get m k h)).isSome := by
+  simp_to_model [filterMap] using List.Const.isEmpty_filterMap_eq_false
+
+theorem contains_filterMap_eq_true [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} {k : α} (h : m.1.WF) :
+    (m.filterMap f).contains k = true ↔ ∃ (h' : m.contains k = true),
+      (f (m.getKey k h') (Const.get m k h')).isSome := by
+  simp_to_model [filterMap] using List.Const.containsKey_filterMap_iff
+
+theorem contains_filterMap_eq_false [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} {k : α} (h : m.1.WF) :
+    (m.filterMap f).contains k = false ↔ ∀ (h' : m.contains k = true),
+      (f (m.getKey k h') (Const.get m k h')) = none := by
+  simp_to_model [filterMap] using List.Const.containsKey_filterMap_eq_false
+
+theorem size_filterMap_eq_size_iff [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} (h : m.1.WF) :
+    (m.filterMap f).1.size = m.1.size ↔ ∀ (a : α) (h : m.contains a),
+      (f (m.getKey a h) (Const.get m a h)).isSome := by
+  simp_to_model [filterMap] using List.Const.length_filterMap_eq_length_iff
+
+theorem get?_filterMap [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} {k : α} (h : m.1.WF) :
+    Const.get? (m.filterMap f) k = (m.getKey? k).bind (fun x => (Const.get? m k).bind (f x)) := by
+  simp_to_model [filterMap] using List.Const.getValue?_filterMap
+
+theorem isSome_apply_of_contains_filterMap [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} {k : α} (h : m.1.WF) :
+    ∀ (h' : (m.filterMap f).contains k = true),
+      (f (m.getKey k (contains_of_contains_filterMap m h h'))
+        (Const.get m k (contains_of_contains_filterMap m h h'))).isSome := by
+  simp_to_model [filterMap] using List.Const.isSome_apply_of_containsKey_filterMap
+
+theorem get_filterMap [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} {k : α} (h : m.1.WF) {h'} :
+    Const.get (m.filterMap f) k h' =
+      (f (m.getKey k (contains_of_contains_filterMap m h h'))
+        (Const.get m k (contains_of_contains_filterMap m h h'))).get
+          (isSome_apply_of_contains_filterMap m h h') := by
+  simp_to_model [filterMap] using List.getValue_filterMap
+
+theorem get!_filterMap [EquivBEq α] [LawfulHashable α] [Inhabited γ]
+    {f : (a : α) → β → Option γ} {k : α} (h : m.1.WF) :
+    Const.get! (m.filterMap f) k =
+      ((m.getKey? k).bind (fun x => (Const.get? m k).bind (f x))).get! := by
+  simp_to_model [filterMap] using List.Const.getValue!_filterMap
+
+theorem getD_filterMap [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} {k : α} {fallback : γ} (h : m.1.WF) :
+    Const.getD (m.filterMap f) k fallback =
+      ((m.getKey? k).bind (fun x => (Const.get? m k).bind (f x))).getD fallback := by
+  simp_to_model [filterMap] using List.Const.getValueD_filterMap
+
+theorem toList_filterMap [EquivBEq α] [LawfulHashable α]
+   {f : (a : α) → β → Option γ} (h : m.1.WF) :
+   (Raw.Const.toList (m.filterMap f).1).Perm
+     ((Raw.Const.toList m.1).filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩))) := by
+ simp_to_model [filterMap, Const.toList, Equiv]
+ simp [List.map_filterMap]
+ rfl
+
+theorem getKey?_filterMap [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} {k : α} (h : m.1.WF) :
+    (m.filterMap f).getKey? k =
+    (m.getKey? k).pfilter (fun x h' =>
+      (f x (Const.get m x (contains_of_getKey?_eq_some m h h'))).isSome) := by
+  simp_to_model [filterMap] using List.Const.getKey?_filterMap
+
+theorem getKey_filterMap [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} {k : α} (h : m.1.WF) {h'}:
+    (m.filterMap f).getKey k h' = m.getKey k (contains_of_contains_filterMap m h h') := by
+  simp_to_model [filterMap] using List.getKey_filterMap
+
+theorem getKey!_filterMap [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    {f : (a : α) → β → Option γ} {k : α} (h : m.1.WF) :
+    (m.filterMap f).getKey! k =
+    ((m.getKey? k).pfilter (fun x h' =>
+      (f x (Const.get m x (contains_of_getKey?_eq_some m h h'))).isSome)).get! := by
+  simp_to_model [filterMap] using List.Const.getKey!_filterMap
+
+theorem getKeyD_filterMap [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Option γ} {k fallback : α} (h : m.1.WF) :
+    (m.filterMap f).getKeyD k fallback =
+    ((m.getKey? k).pfilter (fun x h' =>
+      (f x (Const.get m x (contains_of_getKey?_eq_some m h h'))).isSome)).getD fallback := by
+  simp_to_model [filterMap] using List.Const.getKeyD_filterMap
+
+end Const
+
+end filterMap
+
+section filter
+
+theorem isEmpty_filter_iff [LawfulBEq α]
+    {f : (a : α) → β a → Bool} (h : m.1.WF) :
+    (m.filter f).1.isEmpty = true ↔
+      ∀ (k : α) (h : m.contains k = true), f k (m.get k h) = false := by
+  simp_to_model [filter] using List.isEmpty_filter_eq_true
+
+theorem isEmpty_filter_eq_false_iff [LawfulBEq α]
+    {f : (a : α) → β a → Bool} (h : m.1.WF) :
+    (m.filter f).1.isEmpty = false ↔
+      ∃ (k : α) (h : m.contains k = true), f k (m.get k h) = true := by
+  simp_to_model [filter] using List.isEmpty_filter_eq_false
+
+theorem contains_filter [LawfulBEq α]
+    {f : (a : α) → β a → Bool} {k : α} (h : m.1.WF) :
+    (m.filter f).contains k = (m.get? k).any (f k ·) := by
+  simp_to_model [filter] using List.containsKey_filter
+
+theorem contains_of_contains_filter [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Bool} {k : α} (h : m.1.WF) :
+    (m.filter f).contains k = true → m.contains k = true := by
+  simp_to_model [filter] using containsKey_of_containsKey_filter
+
+theorem size_filter_le_size [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Bool} (h : m.1.WF) :
+    (m.filter f).1.size ≤ m.1.size := by
+  simp_to_model [filter] using List.length_filter_le
+
+theorem size_filter_eq_size_iff [LawfulBEq α]
+    {f : (a : α) → β a → Bool} (h : m.1.WF) :
+    (m.filter f).1.size = m.1.size ↔ ∀ (a : α) (h : m.contains a), (f a (m.get a h)) = true := by
+  simp_to_model [filter] using Internal.List.length_filter_eq_length_iff
+
+theorem get?_filter [LawfulBEq α]
+    {f : (a : α) → β a → Bool} {k : α} (h : m.1.WF) :
+    (m.filter f).get? k = (m.get? k).filter (f k) := by
+  simp_to_model [filter] using List.getValueCast?_filter
+
+theorem get_filter [LawfulBEq α]
+    {f : (a : α) → β a → Bool} {k : α} (h : m.1.WF) {h'} :
+    (m.filter f).get k h' =
+      m.get k (contains_of_contains_filter m h h') := by
+  simp_to_model [filter] using List.getValueCast_filter
+
+theorem get!_filter [LawfulBEq α]
+    {f : (a : α) → β a → Bool} {k : α} [Inhabited (β k)] (h : m.1.WF) :
+    (m.filter f).get! k = ((m.get? k).filter (f k)).get! := by
+  simp_to_model [filter] using List.getValueCast!_filter
+
+theorem getD_filter [LawfulBEq α]
+    {f : (a : α) → β a → Bool} {k : α} {fallback : β k} (h : m.1.WF) :
+    (m.filter f).getD k fallback = ((m.get? k).filter (f k)).getD fallback := by
+  simp_to_model [filter] using List.getValueCastD_filter
+
+omit [BEq α] [Hashable α] in
+theorem toList_filter
+    {f : (a : α) → β a → Bool} :
+    (m.filter f).1.toList.Perm
+      (m.1.toList.filter (fun p => (f p.1 p.2))) := by
+  simp_to_model [filter, toList, Equiv] using List.Perm.rfl
+
+theorem getKey?_filter [LawfulBEq α]
+    {f : (a : α) → β a → Bool} {k : α} (h : m.1.WF) :
+    (m.filter f).getKey? k =
+    (m.getKey? k).pfilter (fun x h' =>
+      f x (m.get x (contains_of_getKey?_eq_some m h h'))) := by
+  simp_to_model [filter] using List.getKey?_filter
+
+theorem getKey_filter [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Bool} {k : α} (h : m.1.WF) {h'}:
+    (m.filter f).getKey k h' = m.getKey k (contains_of_contains_filter m h h') := by
+  simp_to_model [filter] using List.getKey_filter
+
+theorem getKey!_filter [LawfulBEq α] [Inhabited α]
+    {f : (a : α) → β a → Bool} {k : α} (h : m.1.WF) :
+    (m.filter f).getKey! k =
+    ((m.getKey? k).pfilter (fun x h' =>
+      f x (m.get x (contains_of_getKey?_eq_some m h h')))).get! := by
+  simp_to_model [filter] using List.getKey!_filter
+
+theorem getKeyD_filter [LawfulBEq α]
+    {f : (a : α) → β a → Bool} {k fallback : α} (h : m.1.WF) :
+    (m.filter f).getKeyD k fallback =
+    ((m.getKey? k).pfilter (fun x h' =>
+      f x (m.get x (contains_of_getKey?_eq_some m h h')))).getD fallback := by
+  simp_to_model [filter] using List.getKeyD_filter
+
+namespace Const
+
+variable {β : Type v} {γ : Type w} (m : Raw₀ α (fun _ => β))
+
+theorem isEmpty_filter_iff [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} (h : m.1.WF) :
+    (m.filter f).1.isEmpty = true ↔
+      ∀ (k : α) (h : m.contains k = true), f (m.getKey k h) (Const.get m k h) = false := by
+  simp_to_model [filter] using List.Const.isEmpty_filter_eq_true
+
+theorem isEmpty_filter_eq_false_iff [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} (h : m.1.WF) :
+    (m.filter f).1.isEmpty = false ↔
+      ∃ (k : α) (h : m.contains k = true), (f (m.getKey k h) (Const.get m k h)) = true := by
+  simp_to_model [filter] using List.Const.isEmpty_filter_eq_false
+
+theorem contains_filter_iff [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} {k : α} (h : m.1.WF) :
+    (m.filter f).contains k = true ↔ ∃ (h' : m.contains k = true),
+      (f (m.getKey k h') (Const.get m k h')) := by
+  simp_to_model [filter] using List.Const.containsKey_filter_iff
+
+theorem contains_filter_eq_false_iff [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} {k : α} (h : m.1.WF) :
+    (m.filter f).contains k = false ↔ ∀ (h' : m.contains k = true),
+      (f (m.getKey k h') (Const.get m k h')) = false := by
+  simp_to_model [filter] using List.Const.containsKey_filter_eq_false_iff
+
+theorem size_filter_eq_size_iff [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} (h : m.1.WF) :
+    (m.filter f).1.size = m.1.size ↔ ∀ (a : α) (h : m.contains a),
+      f (m.getKey a h) (Const.get m a h) := by
+  simp_to_model [filter] using List.Const.length_filter_eq_length_iff
+
+theorem get?_filter [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} {k : α} (h : m.1.WF) :
+    Const.get? (m.filter f) k = (m.getKey? k).bind (fun x => (Const.get? m k).filter (f x)) := by
+  simp_to_model [filter] using List.Const.getValue?_filter
+
+theorem get_filter [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} {k : α} (h : m.1.WF) {h'} :
+    Const.get (m.filter f) k h' = Const.get m k (contains_of_contains_filter m h h') := by
+  simp_to_model [filter] using List.getValue_filter
+
+theorem get!_filter [EquivBEq α] [LawfulHashable α] [Inhabited β]
+    {f : (a : α) → β → Bool} {k : α} (h : m.1.WF) :
+    Const.get! (m.filter f) k =
+      ((m.getKey? k).bind (fun x => (Const.get? m k).filter (f x))).get! := by
+  simp_to_model [filter] using List.Const.getValue!_filter
+
+theorem getD_filter [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} {k : α} {fallback : β} (h : m.1.WF) :
+    Const.getD (m.filter f) k fallback =
+      ((m.getKey? k).bind (fun x => (Const.get? m k).filter (f x))).getD fallback := by
+  simp_to_model [filter] using List.Const.getValueD_filter
+
+--theorem toList_filter [EquivBEq α] [LawfulHashable α]
+--    {f : (a : α) → β → Bool} (h : m.1.WF) :
+--    (Raw.Const.toList (m.filter f).1).Perm
+--      ((Raw.Const.toList m.1).filter (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩))) := by
+--  simp_to_model [filter, Const.toList, Equiv]
+--  sorry
+
+theorem getKey?_filter [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} {k : α} (h : m.1.WF) :
+    (m.filter f).getKey? k =
+    (m.getKey? k).pfilter (fun x h' =>
+      (f x (Const.get m x (contains_of_getKey?_eq_some m h h')))) := by
+  simp_to_model [filter] using List.Const.getKey?_filter
+
+theorem getKey_filter [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} {k : α} (h : m.1.WF) {h'}:
+    (m.filter f).getKey k h' = m.getKey k (contains_of_contains_filter m h h') := by
+  simp_to_model [filter] using List.getKey_filter
+
+theorem getKey!_filter [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    {f : (a : α) → β → Bool} {k : α} (h : m.1.WF) :
+    (m.filter f).getKey! k =
+    ((m.getKey? k).pfilter (fun x h' =>
+      (f x (Const.get m x (contains_of_getKey?_eq_some m h h'))))).get! := by
+  simp_to_model [filter] using List.Const.getKey!_filter
+
+theorem getKeyD_filter [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → Bool} {k fallback : α} (h : m.1.WF) :
+    (m.filter f).getKeyD k fallback =
+    ((m.getKey? k).pfilter (fun x h' =>
+      (f x (Const.get m x (contains_of_getKey?_eq_some m h h'))))).getD fallback := by
+  simp_to_model [filter] using List.Const.getKeyD_filter
+
+end Const
+
+end filter
+
+section map
+
+variable {γ : α →  Type w}
+
+theorem isEmpty_map_iff [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → γ a} (h : m.1.WF) :
+    (m.map f).1.isEmpty = m.1.isEmpty := by
+  simp_to_model [map] using List.isEmpty_map
+
+theorem contains_map [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → γ a} {k : α} (h : m.1.WF) :
+    (m.map f).contains k = m.contains k := by
+  simp_to_model [map] using List.containsKey_map
+
+theorem contains_of_contains_map [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → γ a} {k : α} (h : m.1.WF) :
+    (m.map f).contains k = true → m.contains k = true := by
+  simp [contains_map m h]
+
+theorem size_map_eq_size [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → γ a} (h : m.1.WF) :
+    (m.map f).1.size = m.1.size := by
+  simp_to_model [map] using List.length_map
+
+theorem get?_map [LawfulBEq α]
+    {f : (a : α) → β a → γ a} {k : α} (h : m.1.WF) :
+    (m.map f).get? k = (m.get? k).map (f k) := by
+  simp_to_model [map] using List.getValueCast?_map
+
+theorem get_map [LawfulBEq α]
+    {f : (a : α) → β a → γ a} {k : α} (h : m.1.WF) {h'} :
+    (m.map f).get k h' =
+      f k (m.get k (contains_of_contains_map m h h')) := by
+  simp_to_model [map] using List.getValueCast_map
+
+theorem get!_map [LawfulBEq α]
+    {f : (a : α) → β a → γ a} {k : α} [Inhabited (γ k)] (h : m.1.WF) :
+    (m.map f).get! k = ((m.get? k).map (f k)).get! := by
+  simp_to_model [map] using List.getValueCast!_map
+
+theorem getD_map [LawfulBEq α]
+    {f : (a : α) → β a → γ a} {k : α} {fallback : γ k} (h : m.1.WF) :
+    (m.map f).getD k fallback = ((m.get? k).map (f k)).getD fallback := by
+  simp_to_model [map] using List.getValueCastD_map
+
+omit [BEq α] [Hashable α] in
+theorem toList_map
+    {f : (a : α) → β a → γ a} :
+    (m.map f).1.toList.Perm
+      (m.1.toList.map (fun p => ⟨p.1,f p.1 p.2⟩)) := by
+  simp_to_model [map, toList, Equiv] using List.Perm.rfl
+
+theorem getKey?_map [LawfulBEq α]
+    {f : (a : α) → β a → γ a} {k : α} (h : m.1.WF) :
+    (m.map f).getKey? k = m.getKey? k := by
+  simp_to_model [map] using List.getKey?_map
+
+theorem getKey_map [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → γ a} {k : α} (h : m.1.WF) {h'}:
+    (m.map f).getKey k h' = m.getKey k (contains_of_contains_map m h h') := by
+  simp_to_model [map] using List.getKey_map
+
+theorem getKey!_map [LawfulBEq α] [Inhabited α]
+    {f : (a : α) → β a → γ a} {k : α} (h : m.1.WF) :
+    (m.map f).getKey! k = m.getKey! k := by
+  simp_to_model [map] using List.getKey!_map
+
+theorem getKeyD_map [LawfulBEq α]
+    {f : (a : α) → β a → γ a} {k fallback : α} (h : m.1.WF) :
+    (m.map f).getKeyD k fallback = m.getKeyD k fallback := by
+  simp_to_model [map] using List.getKeyD_map
+
+namespace Const
+
+variable {β : Type v} {γ : Type w} (m : Raw₀ α (fun _ => β))
+
+--theorem get?_map [EquivBEq α] [LawfulHashable α]
+--    {f : (a : α) → β → γ} {k : α} (h : m.1.WF) :
+--    Const.get? (m.map f) k = (Const.get? m k).pmap (fun v h' => f (m.getKey k h') v)
+--      (fun _ h' => (contains_eq_isSome_get? m h).trans (Option.isSome_of_mem h')) := by
+--  simp_to_model [map]
+--  rw [← List.Const.getValue?_map (by wf_trivial)]
+
+theorem get_map [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β → γ} {k : α} (h : m.1.WF) {h'} :
+    Const.get (m.map f) k h' =
+      (f (m.getKey k (contains_of_contains_map m h h'))
+        (Const.get m k (contains_of_contains_map m h h'))) := by
+  simp_to_model [map] using List.getValue_map
+
+--theorem get!_map [EquivBEq α] [LawfulHashable α] [Inhabited γ]
+--    {f : (a : α) → β → γ} {k : α} (h : m.1.WF) :
+--    Const.get! (m.map f) k =
+--      ((m.getKey? k).bind (fun x => (Const.get? m k).map (f x))).get! := by
+--  simp_to_model [map] using List.Const.getValue!_map
+
+--theorem getD_map [EquivBEq α] [LawfulHashable α]
+--    {f : (a : α) → β → γ} {k : α} {fallback : γ} (h : m.1.WF) :
+--    Const.getD (m.map f) k fallback =
+--      ((m.getKey? k).bind (fun x => (Const.get? m k).map (f x))).getD fallback := by
+--  simp_to_model [map] using List.Const.getValueD_map
+
+--theorem toList_map [EquivBEq α] [LawfulHashable α]
+--    {f : (a : α) → β → γ} (h : m.1.WF) :
+--    (Raw.Const.toList (m.map f).1).Perm
+--      ((Raw.Const.toList m.1).map (fun p => ⟨p.1, f p.1 p.2⟩)) := by
+--  simp_to_model [map, Const.toList, Equiv] using List.Const.toList_map
+
+end Const
+
+end map
+
 end Raw₀
 
 end Std.DHashMap.Internal

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

@@ -951,76 +951,6 @@ theorem wfImp_erase [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m
   rw [erase_eq_eraseₘ]
   exact wfImp_eraseₘ h
 
-/-! # `filterMapₘ` -/
-
-theorem toListModel_filterMapₘ {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :
-    Perm (toListModel (m.filterMapₘ f).1.buckets)
-      ((toListModel m.1.buckets).filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) :=
-  toListModel_updateAllBuckets AssocList.toList_filterMap
-    (by simp [List.filterMap_append])
-
-theorem isHashSelf_filterMapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
-    {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) :
-    IsHashSelf (m.filterMapₘ f).1.buckets := by
-  refine h.buckets_hash_self.updateAllBuckets (fun l p hp => ?_)
-  have hp := AssocList.toList_filterMap.mem_iff.1 hp
-  simp only [mem_filterMap, Option.map_eq_some'] at hp
-  obtain ⟨p, ⟨hkv, ⟨d, ⟨-, rfl⟩⟩⟩⟩ := hp
-  exact containsKey_of_mem hkv
-
-theorem wfImp_filterMapₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
-    {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) : Raw.WFImp (m.filterMapₘ f).1 where
-  buckets_hash_self := isHashSelf_filterMapₘ h
-  size_eq := by simp [filterMapₘ]
-  distinct := h.distinct.filterMap.perm toListModel_filterMapₘ
-
-/-! # `filterMap` -/
-
-theorem toListModel_filterMap {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :
-    Perm (toListModel (m.filterMap f).1.buckets)
-      ((toListModel m.1.buckets).filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) := by
-  rw [filterMap_eq_filterMapₘ]
-  exact toListModel_filterMapₘ
-
-theorem wfImp_filterMap [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
-    {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) :
-    Raw.WFImp (m.filterMap f).1 := by
-  rw [filterMap_eq_filterMapₘ]
-  exact wfImp_filterMapₘ h
-
-/-! # `mapₘ` -/
-
-theorem toListModel_mapₘ {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
-    Perm (toListModel (m.mapₘ f).1.buckets)
-      ((toListModel m.1.buckets).map fun p => ⟨p.1, f p.1 p.2⟩) :=
-  toListModel_updateAllBuckets AssocList.toList_map (by simp)
-
-theorem isHashSelf_mapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
-    {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : IsHashSelf (m.mapₘ f).1.buckets := by
-  refine h.buckets_hash_self.updateAllBuckets (fun l p hp => ?_)
-  have hp := AssocList.toList_map.mem_iff.1 hp
-  obtain ⟨p, hp₁, rfl⟩ := mem_map.1 hp
-  exact containsKey_of_mem hp₁
-
-theorem wfImp_mapₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
-    {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : Raw.WFImp (m.mapₘ f).1 where
-  buckets_hash_self := isHashSelf_mapₘ h
-  size_eq := by rw [toListModel_mapₘ.length_eq, List.length_map, ← h.size_eq, mapₘ]
-  distinct := h.distinct.map.perm toListModel_mapₘ
-
-/-! # `map` -/
-
-theorem toListModel_map {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
-    Perm (toListModel (m.map f).1.buckets)
-      ((toListModel m.1.buckets).map fun p => ⟨p.1, f p.1 p.2⟩) := by
-  rw [map_eq_mapₘ]
-  exact toListModel_mapₘ
-
-theorem wfImp_map [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
-    {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : Raw.WFImp (m.map f).1 := by
-  rw [map_eq_mapₘ]
-  exact wfImp_mapₘ h
-
 /-! # `filterₘ` -/
 
 theorem toListModel_filterₘ {m : Raw₀ α β} {f : (a : α) → β a → Bool} :
@@ -1094,6 +1024,84 @@ end Raw
 
 namespace Raw₀
 
+/-! # `filterMapₘ` -/
+
+theorem toListModel_filterMapₘ {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :
+    Perm (toListModel (m.filterMapₘ f).1.buckets)
+      ((toListModel m.1.buckets).filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) :=
+  toListModel_updateAllBuckets AssocList.toList_filterMap
+    (by simp [List.filterMap_append])
+
+theorem isHashSelf_filterMapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) :
+    IsHashSelf (m.filterMapₘ f).1.buckets := by
+  refine h.buckets_hash_self.updateAllBuckets (fun l p hp => ?_)
+  have hp := AssocList.toList_filterMap.mem_iff.1 hp
+  simp only [mem_filterMap, Option.map_eq_some'] at hp
+  obtain ⟨p, ⟨hkv, ⟨d, ⟨-, rfl⟩⟩⟩⟩ := hp
+  exact containsKey_of_mem hkv
+
+theorem wfImp_filterMapₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) : Raw.WFImp (m.filterMapₘ f).1 where
+  buckets_hash_self := isHashSelf_filterMapₘ h
+  size_eq := by simp [filterMapₘ]
+  distinct := h.distinct.filterMap.perm toListModel_filterMapₘ
+
+/-! # `filterMap` -/
+
+theorem toListModel_filterMap {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :
+    Perm (toListModel (m.filterMap f).1.buckets)
+      ((toListModel m.1.buckets).filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) := by
+  rw [filterMap_eq_filterMapₘ]
+  exact toListModel_filterMapₘ
+
+theorem wfImp_filterMap [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) :
+    Raw.WFImp (m.filterMap f).1 := by
+  rw [filterMap_eq_filterMapₘ]
+  exact wfImp_filterMapₘ h
+
+theorem wf_filterMap₀ [BEq α] [Hashable α] {m : Raw₀ α β} (h : m.1.WF)
+    {f : (a : α) → β a → Option (δ a)} : (m.filterMap f).1.WF :=
+  .wf (Raw₀.filterMap f ⟨m, h.size_buckets_pos⟩).2 (wfImp_filterMap (Raw.WF.out h))
+
+/-! # `mapₘ` -/
+
+theorem toListModel_mapₘ {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
+    Perm (toListModel (m.mapₘ f).1.buckets)
+      ((toListModel m.1.buckets).map fun p => ⟨p.1, f p.1 p.2⟩) :=
+  toListModel_updateAllBuckets AssocList.toList_map (by simp)
+
+theorem isHashSelf_mapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : IsHashSelf (m.mapₘ f).1.buckets := by
+  refine h.buckets_hash_self.updateAllBuckets (fun l p hp => ?_)
+  have hp := AssocList.toList_map.mem_iff.1 hp
+  obtain ⟨p, hp₁, rfl⟩ := mem_map.1 hp
+  exact containsKey_of_mem hp₁
+
+theorem wfImp_mapₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : Raw.WFImp (m.mapₘ f).1 where
+  buckets_hash_self := isHashSelf_mapₘ h
+  size_eq := by rw [toListModel_mapₘ.length_eq, List.length_map, ← h.size_eq, mapₘ]
+  distinct := h.distinct.map.perm toListModel_mapₘ
+
+/-! # `map` -/
+
+theorem toListModel_map {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
+    Perm (toListModel (m.map f).1.buckets)
+      ((toListModel m.1.buckets).map fun p => ⟨p.1, f p.1 p.2⟩) := by
+  rw [map_eq_mapₘ]
+  exact toListModel_mapₘ
+
+theorem wfImp_map [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : Raw.WFImp (m.map f).1 := by
+  rw [map_eq_mapₘ]
+  exact wfImp_mapₘ h
+
+theorem wf_map₀ [BEq α] [Hashable α] {m : Raw₀ α β} (h : m.1.WF) {f : (a : α) → β a → δ a} :
+    (m.map f).1.WF :=
+  .wf (Raw₀.map f ⟨m, h.size_buckets_pos⟩).2 (Raw₀.wfImp_map (Raw.WF.out h))
+
 /-! # `insertMany` -/
 
 theorem wfImp_insertMany [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}