∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] [inst_2 : Hashable α]
  [inst_3 : LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α}
  {h : m.containsₘ a = true},
  m.getEntryₘ a h = Std.Internal.List.getEntry a (Std.DHashMap.Internal.toListModel (↑m).buckets) ⋯