∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  [inst : Inhabited β] {f : α → β → Bool} {k : α},
  Std.DHashMap.Const.get! (Std.DHashMap.filter f m) k = (Option.filter (f k) (Std.DHashMap.Const.get? m k)).get!