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