-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL!.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.balanceL! k v l r =
    match r with
    | Std.DTreeMap.Internal.Impl.leaf =>
      match l 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 l Std.DTreeMap.Internal.Impl.leaf
      |
      Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
          (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r) =>
        Std.DTreeMap.Internal.Impl.inner 3 lrk lrv
          (Std.DTreeMap.Internal.Impl.inner 1 lk lv Std.DTreeMap.Internal.Impl.leaf 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 lk lv (ll@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r))
          Std.DTreeMap.Internal.Impl.leaf =>
        Std.DTreeMap.Internal.Impl.inner 3 lk lv ll
          (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
      |
      Std.DTreeMap.Internal.Impl.inner ls lk lv (ll@h:(Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l r))
          lr@h_1:(Std.DTreeMap.Internal.Impl.inner lrs k_2 v_2 l_1 r_1) =>
        Std.DTreeMap.Internal.Impl.inner (1 + ls) lk lv ll
          (Std.DTreeMap.Internal.Impl.inner (1 + lrs) k v lr Std.DTreeMap.Internal.Impl.leaf)
    | Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_1 =>
      match l with
      | Std.DTreeMap.Internal.Impl.leaf =>
        Std.DTreeMap.Internal.Impl.inner (1 + rs) k v Std.DTreeMap.Internal.Impl.leaf r
      | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr =>
        if ls > Std.DTreeMap.Internal.delta * rs then
          match ll, lr with
          | Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l r_2, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
            if lrs < Std.DTreeMap.Internal.ratio * lls then
              Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) lk lv ll
                (Std.DTreeMap.Internal.Impl.inner (1 + rs + lrs) k v lr r)
            else
              Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) lrk lrv
                (Std.DTreeMap.Internal.Impl.inner (1 + lls + lrl.size) lk lv ll lrl)
                (Std.DTreeMap.Internal.Impl.inner (1 + rs + lrr.size) k v lrr r)
          | 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.balanceL!" 182 35
              "balanceL! input was not balanced"
          | Std.DTreeMap.Internal.Impl.leaf, x =>
            panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing" "Std.DTreeMap.Internal.Impl.balanceL!" 183 21
              "balanceL! input was not balanced"
        else Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) k v l r