∀ {α : Type u_1} {β : α → Type u_2} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (size : ℕ)
  (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size)
  (dt : Std.DTreeMap.Internal.Impl α β) (hdt : dt.Balanced) (hdt' : dt.size = l'.size + r'.size),
  (Std.DTreeMap.Internal.Impl.balanceLErase k v l dt ⋯ ⋯ ⋯).size =
    l.size + (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size