-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!.fun_cases_unfolding : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k)
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop),
  motive 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) →
    (∀ (size : ℕ) (k_1 : α) (v_1 : β k_1),
        motive 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
            (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
              Std.DTreeMap.Internal.Impl.leaf))) →
      (∀ (size : ℕ) (rk : α) (rv : β rk) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β),
          motive Std.DTreeMap.Internal.Impl.leaf
            (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
              (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)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r))) →
        (∀ (size : ℕ) (rk : α) (rv : β rk) (size_1 : ℕ) (rlk : α) (rlv : β rlk) (l r : Std.DTreeMap.Internal.Impl α β),
            motive Std.DTreeMap.Internal.Impl.leaf
              (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))) →
          (∀ (rs : ℕ) (rk : α) (rv : β rk) (rls : ℕ) (rlk : α) (rlv : β rlk) (rll rlr : Std.DTreeMap.Internal.Impl α β)
              (size : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β),
              motive 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 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))
                  (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l r))) →
            (∀ (ls : ℕ) (lk : α) (lv : β lk),
                motive
                  (Std.DTreeMap.Internal.Impl.inner ls lk lv Std.DTreeMap.Internal.Impl.leaf
                    Std.DTreeMap.Internal.Impl.leaf)
                  Std.DTreeMap.Internal.Impl.leaf
                  (Std.DTreeMap.Internal.Impl.inner 2 k v
                    (Std.DTreeMap.Internal.Impl.inner ls lk lv Std.DTreeMap.Internal.Impl.leaf
                      Std.DTreeMap.Internal.Impl.leaf)
                    Std.DTreeMap.Internal.Impl.leaf)) →
              (∀ (ls : ℕ) (lk : α) (lv : β lk) (size : ℕ) (lrk : α) (lrv : β lrk)
                  (l r : Std.DTreeMap.Internal.Impl α β),
                  motive
                    (Std.DTreeMap.Internal.Impl.inner ls lk lv Std.DTreeMap.Internal.Impl.leaf
                      (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r))
                    Std.DTreeMap.Internal.Impl.leaf
                    (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))) →
                (∀ (ls : ℕ) (lk : α) (lv : β lk) (size : ℕ) (k_1 : α) (v_1 : β k_1)
                    (l r : Std.DTreeMap.Internal.Impl α β),
                    motive
                      (Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l r)
                        Std.DTreeMap.Internal.Impl.leaf)
                      Std.DTreeMap.Internal.Impl.leaf
                      (Std.DTreeMap.Internal.Impl.inner 3 lk lv (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l r)
                        (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf
                          Std.DTreeMap.Internal.Impl.leaf))) →
                  (∀ (ls : ℕ) (lk : α) (lv : β lk) (size : ℕ) (k_1 : α) (v_1 : β k_1)
                      (l r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α) (lrv : β lrk)
                      (lrl lrr : Std.DTreeMap.Internal.Impl α β),
                      motive
                        (Std.DTreeMap.Internal.Impl.inner ls lk lv (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.leaf
                        (Std.DTreeMap.Internal.Impl.inner (1 + ls) lk lv
                          (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l r)
                          (Std.DTreeMap.Internal.Impl.inner (1 + lrs) k v
                            (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr) Std.DTreeMap.Internal.Impl.leaf))) →
                    (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β) (ls_1 : ℕ) (lk_1 : α)
                        (lv_1 : β lk_1),
                        Std.DTreeMap.Internal.delta * ls < ls_1 →
                          ∀ (lls : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α)
                            (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β),
                            lls < Std.DTreeMap.Internal.ratio * lrs →
                              motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                                (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1
                                  (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r)
                                  (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
                                (Std.DTreeMap.Internal.Impl.inner (1 + ls + ls_1) lk_1 lv_1
                                  (Std.DTreeMap.Internal.Impl.inner (1 + ls + lls) k v
                                    (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                                    (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r))
                                  (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))) →
                      (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β) (ls_1 : ℕ) (lk_1 : α)
                          (lv_1 : β lk_1),
                          Std.DTreeMap.Internal.delta * ls < ls_1 →
                            ∀ (lls : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ)
                              (lrk : α) (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β),
                              ¬lls < Std.DTreeMap.Internal.ratio * lrs →
                                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                                  (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1
                                    (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r)
                                    (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
                                  (Std.DTreeMap.Internal.Impl.inner (1 + ls + ls_1) k_1 v_1
                                    (Std.DTreeMap.Internal.Impl.inner (1 + ls + l.size) k v
                                      (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) l)
                                    (Std.DTreeMap.Internal.Impl.inner (1 + lrs + r.size) lk_1 lv_1 r
                                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)))) →
                        (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β) (ls_1 : ℕ) (lk_1 : α)
                            (lv_1 : β lk_1),
                            Std.DTreeMap.Internal.delta * ls < ls_1 →
                              ∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
                                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                                  (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1
                                    (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")) →
                          (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β) (ls_1 : ℕ)
                              (lk_1 : α) (lv_1 : β lk_1) (lr_1 : Std.DTreeMap.Internal.Impl α β),
                              Std.DTreeMap.Internal.delta * ls < ls_1 →
                                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                                  (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 Std.DTreeMap.Internal.Impl.leaf lr_1)
                                  (panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing"
                                    "Std.DTreeMap.Internal.Impl.balance!" 384 22 "balance! input was not balanced")) →
                            (∀ (ls : ℕ) (lk : α) (lv : β lk) (ls_1 : ℕ) (lk_1 : α) (lv_1 : β lk_1)
                                (ll lr : Std.DTreeMap.Internal.Impl α β),
                                ¬Std.DTreeMap.Internal.delta * ls < ls_1 →
                                  Std.DTreeMap.Internal.delta * ls_1 < ls →
                                    ∀ (lls : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ)
                                      (lrk : α) (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β),
                                      lrs < Std.DTreeMap.Internal.ratio * lls →
                                        motive
                                          (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                            (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r)
                                            (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
                                          (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll lr)
                                          (Std.DTreeMap.Internal.Impl.inner (1 + ls + ls_1) lk lv
                                            (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r)
                                            (Std.DTreeMap.Internal.Impl.inner (1 + ls_1 + lrs) k v
                                              (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)
                                              (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll lr)))) →
                              (∀ (ls : ℕ) (lk : α) (lv : β lk) (ls_1 : ℕ) (lk_1 : α) (lv_1 : β lk_1)
                                  (ll lr : Std.DTreeMap.Internal.Impl α β),
                                  ¬Std.DTreeMap.Internal.delta * ls < ls_1 →
                                    Std.DTreeMap.Internal.delta * ls_1 < ls →
                                      ∀ (lls : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
                                        (lrs : ℕ) (lrk : α) (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β),
                                        ¬lrs < Std.DTreeMap.Internal.ratio * lls →
                                          motive
                                            (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                              (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r)
                                              (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
                                            (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll lr)
                                            (Std.DTreeMap.Internal.Impl.inner (1 + ls + ls_1) lrk lrv
                                              (Std.DTreeMap.Internal.Impl.inner (1 + lls + lrl.size) lk lv
                                                (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r) lrl)
                                              (Std.DTreeMap.Internal.Impl.inner (1 + ls_1 + lrr.size) k v lrr
                                                (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll lr)))) →
                                (∀ (ls : ℕ) (lk : α) (lv : β lk) (ls_1 : ℕ) (lk_1 : α) (lv_1 : β lk_1)
                                    (ll lr : Std.DTreeMap.Internal.Impl α β),
                                    ¬Std.DTreeMap.Internal.delta * ls < ls_1 →
                                      Std.DTreeMap.Internal.delta * ls_1 < ls →
                                        ∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
                                          motive
                                            (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                              (Std.DTreeMap.Internal.Impl.inner size k v l r)
                                              Std.DTreeMap.Internal.Impl.leaf)
                                            (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll lr)
                                            (panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing"
                                              "Std.DTreeMap.Internal.Impl.balance!" 393 36
                                              "balance! input was not balanced")) →
                                  (∀ (ls : ℕ) (lk : α) (lv : β lk) (lr : Std.DTreeMap.Internal.Impl α β) (ls_1 : ℕ)
                                      (lk_1 : α) (lv_1 : β lk_1) (ll lr_1 : Std.DTreeMap.Internal.Impl α β),
                                      ¬Std.DTreeMap.Internal.delta * ls < ls_1 →
                                        Std.DTreeMap.Internal.delta * ls_1 < ls →
                                          motive
                                            (Std.DTreeMap.Internal.Impl.inner ls lk lv Std.DTreeMap.Internal.Impl.leaf
                                              lr)
                                            (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll lr_1)
                                            (panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing"
                                              "Std.DTreeMap.Internal.Impl.balance!" 394 22
                                              "balance! input was not balanced")) →
                                    (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β) (ls_1 : ℕ)
                                        (lk_1 : α) (lv_1 : β lk_1) (ll_1 lr_1 : Std.DTreeMap.Internal.Impl α β),
                                        ¬Std.DTreeMap.Internal.delta * ls < ls_1 →
                                          ¬Std.DTreeMap.Internal.delta * ls_1 < ls →
                                            motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                                              (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll_1 lr_1)
                                              (Std.DTreeMap.Internal.Impl.inner (1 + ls + ls_1) k v
                                                (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                                                (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll_1 lr_1))) →
                                      ∀ (l r : Std.DTreeMap.Internal.Impl α β),
                                        motive l r (Std.DTreeMap.Internal.Impl.balance! k v l r)