∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (f : Option (β a) → Option (β a)),
  m.alterₘ a f =
    if h : m.containsₘ a = true then
      let buckets' :=
        Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a fun l => Std.DHashMap.Internal.AssocList.alter a f l;
      have size' :=
        if Std.DHashMap.Internal.Raw₀.containsₘ ⟨Std.DHashMap.Internal.withComputedSize buckets', ⋯⟩ a = true then
          (↑m).size
        else (↑m).size - 1;
      ⟨{ size := size', buckets := buckets' }, ⋯⟩
    else
      match f none with
      | none => m
      | some b => (m.consₘ a b).expandIfNecessary