∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [ReflBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Bool},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.IsHashSelf (↑(m.filterₘ f)).buckets