∀ {α : Type u} {β : α → Type v} [Ord α] {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β}
  (hl : (Std.DTreeMap.Internal.Impl.inner sz k v l r).Balanced)
  {h :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size},
  Std.DTreeMap.Internal.Impl.balance k v l r ⋯ ⋯ h = Std.DTreeMap.Internal.Impl.inner sz k v l r