-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL!.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.inner size k_1 v_1 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 size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
              Std.DTreeMap.Internal.Impl.leaf)
            Std.DTreeMap.Internal.Impl.leaf)) →
      (∀ (size : ℕ) (lk : α) (lv : β lk) (size_1 : ℕ) (lrk : α) (lrv : β lrk) (l r : Std.DTreeMap.Internal.Impl α β),
          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
            (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))) →
        (∀ (size : ℕ) (lk : α) (lv : β lk) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β),
            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
              (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))) →
          (∀ (ls : ℕ) (lk : α) (lv : β lk) (size : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
              (lrs : ℕ) (k_2 : α) (v_2 : β k_2) (l_1 r_1 : 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 k_2 v_2 l_1 r_1))
                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 k_2 v_2 l_1 r_1)
                    Std.DTreeMap.Internal.Impl.leaf))) →
            (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β),
                motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                  (Std.DTreeMap.Internal.Impl.inner (1 + ls) k v Std.DTreeMap.Internal.Impl.leaf
                    (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr))) →
              (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β) (ls_1 : ℕ) (lk_1 : α)
                  (lv_1 : β lk_1),
                  ls_1 > Std.DTreeMap.Internal.delta * 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_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 ls lk lv ll lr)
                          (Std.DTreeMap.Internal.Impl.inner (1 + ls_1 + ls) lk_1 lv_1
                            (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r)
                            (Std.DTreeMap.Internal.Impl.inner (1 + ls + lrs) k v
                              (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)
                              (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)))) →
                (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β) (ls_1 : ℕ) (lk_1 : α)
                    (lv_1 : β lk_1),
                    ls_1 > Std.DTreeMap.Internal.delta * 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_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 ls lk lv ll lr)
                            (Std.DTreeMap.Internal.Impl.inner (1 + ls_1 + ls) lrk lrv
                              (Std.DTreeMap.Internal.Impl.inner (1 + lls + lrl.size) lk_1 lv_1
                                (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l r) lrl)
                              (Std.DTreeMap.Internal.Impl.inner (1 + ls + lrr.size) k v lrr
                                (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)))) →
                  (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β) (ls_1 : ℕ) (lk_1 : α)
                      (lv_1 : β lk_1),
                      ls_1 > Std.DTreeMap.Internal.delta * ls →
                        ∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
                          motive
                            (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)
                            (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                            (panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing"
                              "Std.DTreeMap.Internal.Impl.balanceL!" 182 35 "balanceL! 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 α β),
                        ls_1 > Std.DTreeMap.Internal.delta * ls →
                          motive (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 Std.DTreeMap.Internal.Impl.leaf lr_1)
                            (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                            (panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Balancing"
                              "Std.DTreeMap.Internal.Impl.balanceL!" 183 21 "balanceL! 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 α β),
                          ¬ls_1 > Std.DTreeMap.Internal.delta * ls →
                            motive (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll_1 lr_1)
                              (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                              (Std.DTreeMap.Internal.Impl.inner (1 + ls_1 + ls) k v
                                (Std.DTreeMap.Internal.Impl.inner ls_1 lk_1 lv_1 ll_1 lr_1)
                                (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr))) →
                        ∀ (l r : Std.DTreeMap.Internal.Impl α β),
                          motive l r (Std.DTreeMap.Internal.Impl.balanceL! k v l r)