-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceR!.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 : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
              (size : ℕ) (k_2 : α) (v_2 : β k_2) (l_1 r_1 : Std.DTreeMap.Internal.Impl α β),
              motive Std.DTreeMap.Internal.Impl.leaf
                (Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls k_1 v_1 l r)
                  (Std.DTreeMap.Internal.Impl.inner size k_2 v_2 l_1 r_1))
                (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 k_1 v_1 l r))
                  (Std.DTreeMap.Internal.Impl.inner size k_2 v_2 l_1 r_1))) →
            (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β),
                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) Std.DTreeMap.Internal.Impl.leaf
                  (Std.DTreeMap.Internal.Impl.inner (1 + ls) k v (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
                    Std.DTreeMap.Internal.Impl.leaf)) →
              (∀ (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 α β),
                      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),
                    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 α β),
                        ¬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),
                      ls_1 > Std.DTreeMap.Internal.delta * ls →
                        ∀ (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.balanceR!" 276 35 "balanceR! 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 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.balanceR!" 277 21 "balanceR! 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 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.balanceR! k v l r)