∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β)
  {f : (a : α) → β a → Option (γ a)},
  (↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).toList.Perm
    (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) (↑m).toList)