∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] (a : α) (f : β a → β a)
  (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.modify ⟨{ size := size, buckets := buckets }, hm⟩ a f =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, hi⟩ =>
      let bucket := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bucket = true then
        let buckets_1 := buckets.uset i Std.DHashMap.Internal.AssocList.nil hi;
        let bucket := Std.DHashMap.Internal.AssocList.modify a f bucket;
        ⟨{ size := size, buckets := buckets_1.uset i bucket ⋯ }, ⋯⟩
      else ⟨{ size := size, buckets := buckets }, hm⟩