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