∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).keys.Perm
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.DHashMap.Raw.Const.get m x ⋯))
        m.keys.attach).unattach