∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (b : β a) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨{ size := size, buckets := buckets }, hm⟩ a b =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bkt = true then
        let buckets' := buckets.uset i Std.DHashMap.Internal.AssocList.nil h;
        (true, ⟨{ size := size, buckets := buckets'.uset i (Std.DHashMap.Internal.AssocList.replace a b bkt) ⋯ }, ⋯⟩)
      else
        have size' := size + 1;
        let buckets' := buckets.uset i (Std.DHashMap.Internal.AssocList.cons a b bkt) h;
        (false, Std.DHashMap.Internal.Raw₀.expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)