∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited γ]
  {f : α → β → Option γ} {k : α} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.filterMap f m) k =
    ((Std.DHashMap.Internal.Raw₀.Const.get? m k).pbind fun x h' => f (m.getKey k ⋯) x).get!