∀ {α : Type u_1} {β : α → Type u_2} (l r : Std.DTreeMap.Internal.Impl α β) (szl : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β) (hl : (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').Balanced)
  (hl' : l = Std.DTreeMap.Internal.Impl.inner szl k' v' l' r') (szr : ℕ) (k'' : α) (v'' : β k'')
  (l'' r'' : Std.DTreeMap.Internal.Impl α β) (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced)
  (hr' : r = Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') (h₁ : Std.DTreeMap.Internal.delta * szl < szr)
  (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced) (hℓ₂ : ℓ.size = l.size + l''.size),
  (Std.DTreeMap.Internal.Impl.balanceLErase k'' v'' ℓ r'' ⋯ ⋯ ⋯).size =
    (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size +
      (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size