∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k fallback : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filter f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x h' => f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯)).getD fallback