-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL.fun_cases_unfolding : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k)
  (motive :
    (l r : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced →
        r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size → Std.DTreeMap.Internal.Impl α β → Prop),
  (∀ (hrb hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced)
      (hlr :
        Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
          Std.DTreeMap.Internal.Impl.leaf.size),
      Std.DTreeMap.Internal.Impl.leaf.Balanced →
        Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
            Std.DTreeMap.Internal.Impl.leaf.size →
          Std.DTreeMap.Internal.Impl.leaf.Balanced →
            Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
                Std.DTreeMap.Internal.Impl.leaf.size →
              motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf hlb hrb hlr
                (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf
                  Std.DTreeMap.Internal.Impl.leaf)) →
    (∀ (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) (size : ℕ) (k_1 : α) (v_1 : β k_1)
        (hlb :
          (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
              Std.DTreeMap.Internal.Impl.leaf).Balanced)
        (hlr :
          Std.DTreeMap.Internal.Impl.BalanceLPrecond
            (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                Std.DTreeMap.Internal.Impl.leaf).size
            Std.DTreeMap.Internal.Impl.leaf.size),
        (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
              Std.DTreeMap.Internal.Impl.leaf).Balanced →
          Std.DTreeMap.Internal.Impl.BalanceLPrecond
              (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                  Std.DTreeMap.Internal.Impl.leaf).size
              Std.DTreeMap.Internal.Impl.leaf.size →
            Std.DTreeMap.Internal.Impl.leaf.Balanced →
              Std.DTreeMap.Internal.Impl.BalanceLPrecond
                  (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                      Std.DTreeMap.Internal.Impl.leaf).size
                  Std.DTreeMap.Internal.Impl.leaf.size →
                motive
                  (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                    Std.DTreeMap.Internal.Impl.leaf)
                  Std.DTreeMap.Internal.Impl.leaf hlb hrb hlr
                  (Std.DTreeMap.Internal.Impl.inner 2 k v
                    (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                      Std.DTreeMap.Internal.Impl.leaf)
                    Std.DTreeMap.Internal.Impl.leaf)) →
      (∀ (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) (size : ℕ) (lk : α) (lv : β lk) (size_1 : ℕ) (lrk : α)
          (lrv : β lrk) (l r : Std.DTreeMap.Internal.Impl α β)
          (hlb :
            (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r)).Balanced)
          (hlr :
            Std.DTreeMap.Internal.Impl.BalanceLPrecond
              (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                  (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r)).size
              Std.DTreeMap.Internal.Impl.leaf.size),
          (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r)).Balanced →
            Std.DTreeMap.Internal.Impl.BalanceLPrecond
                (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                    (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r)).size
                Std.DTreeMap.Internal.Impl.leaf.size →
              Std.DTreeMap.Internal.Impl.leaf.Balanced →
                Std.DTreeMap.Internal.Impl.BalanceLPrecond
                    (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                        (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r)).size
                    Std.DTreeMap.Internal.Impl.leaf.size →
                  motive
                    (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.leaf hlb hrb hlr
                    (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))) →
        (∀ (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) (size : ℕ) (lk : α) (lv : β lk) (size_1 : ℕ) (k_1 : α)
            (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
            (hlb :
              (Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                  Std.DTreeMap.Internal.Impl.leaf).Balanced)
            (hlr :
              Std.DTreeMap.Internal.Impl.BalanceLPrecond
                (Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                    Std.DTreeMap.Internal.Impl.leaf).size
                Std.DTreeMap.Internal.Impl.leaf.size),
            (Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                  Std.DTreeMap.Internal.Impl.leaf).Balanced →
              Std.DTreeMap.Internal.Impl.BalanceLPrecond
                  (Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                      Std.DTreeMap.Internal.Impl.leaf).size
                  Std.DTreeMap.Internal.Impl.leaf.size →
                Std.DTreeMap.Internal.Impl.leaf.Balanced →
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond
                      (Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                          Std.DTreeMap.Internal.Impl.leaf).size
                      Std.DTreeMap.Internal.Impl.leaf.size →
                    motive
                      (Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                        Std.DTreeMap.Internal.Impl.leaf)
                      Std.DTreeMap.Internal.Impl.leaf hlb hrb hlr
                      (Std.DTreeMap.Internal.Impl.inner 3 lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                        (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf
                          Std.DTreeMap.Internal.Impl.leaf))) →
          (∀ (rs : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
              (hrb : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced)
              (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced)
              (hlr :
                Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
                  (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size),
              Std.DTreeMap.Internal.Impl.leaf.Balanced →
                Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
                    (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                  (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced →
                    Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                      motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r) hlb hrb
                        hlr
                        (Std.DTreeMap.Internal.Impl.inner (1 + rs) k v Std.DTreeMap.Internal.Impl.leaf
                          (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r))) →
            (∀ (rs : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
                (hrb : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced) (ls : ℕ) (lk : α) (lv : β lk),
                Std.DTreeMap.Internal.delta * rs < ls →
                  ∀ (lls : ℕ) (k_2 : α) (v_2 : β k_2) (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α)
                    (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β)
                    (hlb :
                      (Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                          (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced)
                    (hlr :
                      Std.DTreeMap.Internal.Impl.BalanceLPrecond
                        (Std.DTreeMap.Internal.Impl.inner ls lk lv
                            (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                            (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size),
                    lrs < Std.DTreeMap.Internal.ratio * lls →
                      (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced →
                        (Std.DTreeMap.Internal.Impl.inner ls lk lv
                              (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                              (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced →
                          Std.DTreeMap.Internal.Impl.BalanceLPrecond
                              (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                  (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                  (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                              (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                            (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                  (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                  (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced →
                              Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                  (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                      (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                  (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                                Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                    (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                        (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                        (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                    (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                                  motive
                                    (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                      (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
                                    (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r) hlb hrb hlr
                                    (Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) lk lv
                                      (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                      (Std.DTreeMap.Internal.Impl.inner (1 + rs + lrs) k v
                                        (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)
                                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r)))) →
              (∀ (rs : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
                  (hrb : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced) (ls : ℕ) (lk : α) (lv : β lk),
                  Std.DTreeMap.Internal.delta * rs < ls →
                    ∀ (lls : ℕ) (k_2 : α) (v_2 : β k_2) (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α)
                      (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β)
                      (hlb :
                        (Std.DTreeMap.Internal.Impl.inner ls lk lv
                            (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                            (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced)
                      (hlr :
                        Std.DTreeMap.Internal.Impl.BalanceLPrecond
                          (Std.DTreeMap.Internal.Impl.inner ls lk lv
                              (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                              (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                          (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size),
                      ¬lrs < Std.DTreeMap.Internal.ratio * lls →
                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced →
                          (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced →
                            Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                    (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                    (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                              (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                    (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                    (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced →
                                Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                    (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                        (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                        (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                    (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                                  Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                      (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                          (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                          (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                      (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                                    motive
                                      (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                        (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                        (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
                                      (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r) hlb hrb hlr
                                      (Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) lrk lrv
                                        (Std.DTreeMap.Internal.Impl.inner (1 + lls + lrl.size) lk lv
                                          (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1) lrl)
                                        (Std.DTreeMap.Internal.Impl.inner (1 + rs + lrr.size) k v lrr
                                          (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r)))) →
                (∀ (rs : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
                    (hrb : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced) (ls : ℕ) (lk : α) (lv : β lk)
                    (ll lr : Std.DTreeMap.Internal.Impl α β)
                    (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced)
                    (hlr :
                      Std.DTreeMap.Internal.Impl.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size),
                    ¬Std.DTreeMap.Internal.delta * rs < ls →
                      (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced →
                        Std.DTreeMap.Internal.Impl.BalanceLPrecond
                            (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                            (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                          (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced →
                            Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                                (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                              motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                                (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r) hlb hrb hlr
                                (Std.DTreeMap.Internal.Impl.inner (1 + ls + rs) k v
                                  (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                                  (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r))) →
                  ∀ (l r : Std.DTreeMap.Internal.Impl α β) (hlb : l.Balanced) (hrb : r.Balanced)
                    (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size),
                    motive l r hlb hrb hlr (Std.DTreeMap.Internal.Impl.balanceL k v l r hlb hrb hlr)