∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.balanceₘ k v l r =
    if l.size + r.size ≤ 1 then Std.DTreeMap.Internal.Impl.bin k v l r
    else
      if h : r.size > Std.DTreeMap.Internal.delta * l.size then
        match r, h with
        | Std.DTreeMap.Internal.Impl.leaf, h => ⋯.elim
        | Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h => Std.DTreeMap.Internal.Impl.rotateL k v l rk rv rl rr
      else
        if h_1 : l.size > Std.DTreeMap.Internal.delta * r.size then
          match l, h, h_1 with
          | Std.DTreeMap.Internal.Impl.leaf, h, h_2 => ⋯.elim
          | Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_2 =>
            Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll lr r
        else Std.DTreeMap.Internal.Impl.bin k v l r