∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : Option β → Option β)
  (hl_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.Const.alter k f Std.DTreeMap.Internal.Impl.leaf hl_2 =
    match f none with
    | none =>
      { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | some v =>
      { impl := Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
        balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }