-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceR!.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.balanceR! k v l r =
    match l with
    | Std.DTreeMap.Internal.Impl.leaf =>
      match r with
      | Std.DTreeMap.Internal.Impl.leaf =>
        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 =>
        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) =>
        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 =>
        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 (rl@h:(Std.DTreeMap.Internal.Impl.inner rls k_1 v_1 l r))
          rr@h_1:(Std.DTreeMap.Internal.Impl.inner size k_2 v_2 l_1 r_1) =>
        Std.DTreeMap.Internal.Impl.inner (1 + rs) rk rv
          (Std.DTreeMap.Internal.Impl.inner (1 + rls) k v Std.DTreeMap.Internal.Impl.leaf rl) rr
    | Std.DTreeMap.Internal.Impl.inner ls k_1 v_1 l_1 r_1 =>
      match r with
      | Std.DTreeMap.Internal.Impl.leaf =>
        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 =>
        if rs > Std.DTreeMap.Internal.delta * ls then
          match rl, rr with
          | Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr, Std.DTreeMap.Internal.Impl.inner rrs k_2 v_2 l_2 r =>
            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 rl) 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 =>
            panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing" "Std.DTreeMap.Internal.Impl.balanceR!" 276 35
              "balanceR! input was not balanced"
          | Std.DTreeMap.Internal.Impl.leaf, x =>
            panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing" "Std.DTreeMap.Internal.Impl.balanceR!" 277 21
              "balanceR! input was not balanced"
        else Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) k v l r