-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.balance! 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 (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
          rr@h:(Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l r) =>
        Std.DTreeMap.Internal.Impl.inner (1 + rs) rk rv
          (Std.DTreeMap.Internal.Impl.inner (1 + rls) k v Std.DTreeMap.Internal.Impl.leaf
            (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr))
          rr
    | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr =>
      match r with
      | Std.DTreeMap.Internal.Impl.leaf =>
        match ll, lr with
        | 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.leaf, Std.DTreeMap.Internal.Impl.inner size 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 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 size k_1 v_1 l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
          Std.DTreeMap.Internal.Impl.inner (1 + ls) lk lv ll
            (Std.DTreeMap.Internal.Impl.inner (1 + lrs) k v (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)
              Std.DTreeMap.Internal.Impl.leaf)
      | Std.DTreeMap.Internal.Impl.inner rs rk rv rl rr =>
        if x : Std.DTreeMap.Internal.delta * ls < rs then
          match rl, rr with
          | Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr, Std.DTreeMap.Internal.Impl.inner rrs k_1 v_1 l_1 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.balance!" 383 36
              "balance! input was not balanced"
          | Std.DTreeMap.Internal.Impl.leaf, x =>
            panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing" "Std.DTreeMap.Internal.Impl.balance!" 384 22
              "balance! input was not balanced"
        else
          if x : Std.DTreeMap.Internal.delta * rs < ls then
            match ll, lr with
            | Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r_1,
              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.balance!" 393 36
                "balance! input was not balanced"
            | Std.DTreeMap.Internal.Impl.leaf, x =>
              panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing" "Std.DTreeMap.Internal.Impl.balance!" 394 22
                "balance! input was not balanced"
          else Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) k v l r