∀ {α : Type u_1} {β : α → Type u_2} [inst : BEq α] [inst_1 : Hashable α]
  (motive :
    (m : Std.DHashMap.Internal.Raw₀ α β) →
      Std.DHashMap.Internal.Raw.WFImp ↑m →
        ¬Std.DHashMap.Internal.numBucketsForCapacity✝ m.1.size ≤ m.1.buckets.size → Prop)
  (m : Std.DHashMap.Internal.Raw₀ α β) (h : Std.DHashMap.Internal.Raw.WFImp ↑m)
  (h_1 : ¬Std.DHashMap.Internal.numBucketsForCapacity✝¹ m.1.size ≤ m.1.buckets.size),
  (∀ (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β))
      (hm : 0 < { size := size, buckets := buckets }.buckets.size)
      (h : Std.DHashMap.Internal.Raw.WFImp ↑⟨{ size := size, buckets := buckets }, hm⟩)
      (h_2 :
        ¬Std.DHashMap.Internal.numBucketsForCapacity✝² ⟨{ size := size, buckets := buckets }, hm⟩.1.size ≤
            ⟨{ size := size, buckets := buckets }, hm⟩.1.buckets.size),
      motive ⟨{ size := size, buckets := buckets }, hm⟩ h h_2) →
    motive m h h_1