∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size),
  Std.DTreeMap.Internal.Impl.balanceR k v l r hlb hrb hlr =
    match l, hlb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr =>
      match r, hrb, hlr with
      | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr =>
        Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
      | Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
        hrb, hlr => Std.DTreeMap.Internal.Impl.inner 2 k v Std.DTreeMap.Internal.Impl.leaf r
      |
      Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
          rr@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r),
        hrb, hlr =>
        Std.DTreeMap.Internal.Impl.inner 3 rk rv
          (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf) rr
      |
      Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
          Std.DTreeMap.Internal.Impl.leaf,
        hrb, hlr =>
        Std.DTreeMap.Internal.Impl.inner 3 rlk rlv
          (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
          (Std.DTreeMap.Internal.Impl.inner 1 rk rv Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
      |
      Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
          (Std.DTreeMap.Internal.Impl.inner rrs k v l r),
        hrb, hlr => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner ls k_1 v_1 l_1 r_1, hlb, hlr =>
      match r, hrb, hlr with
      | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr =>
        Std.DTreeMap.Internal.Impl.inner (1 + ls) k v l Std.DTreeMap.Internal.Impl.leaf
      | Std.DTreeMap.Internal.Impl.inner rs rk rv rl rr, hrb, hlr =>
        if hrsd : rs > Std.DTreeMap.Internal.delta * ls then
          match rl, rr, hrb, hlr with
          | Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr, Std.DTreeMap.Internal.Impl.inner rrs k_2 v_2 l_2 r,
            hrb, hlr =>
            if rls < Std.DTreeMap.Internal.ratio * rrs then
              Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) rk rv
                (Std.DTreeMap.Internal.Impl.inner (1 + ls + rls) k v l
                  (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr))
                rr
            else
              Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) rlk rlv
                (Std.DTreeMap.Internal.Impl.inner (1 + ls + rll.size) k v l rll)
                (Std.DTreeMap.Internal.Impl.inner (1 + rrs + rlr.size) rk rv rlr rr)
          | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => ⋯.elim
          | Std.DTreeMap.Internal.Impl.leaf, x, hrb, hlr => ⋯.elim
        else Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) k v l (Std.DTreeMap.Internal.Impl.inner rs rk rv rl rr)