∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.erase k Std.DTreeMap.Internal.Impl.leaf hr_1 =
    { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }