-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceRErase.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive :
        (r : Std.DTreeMap.Internal.Impl α β) →
          r.Balanced →
            Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size Std.DTreeMap.Internal.Impl.leaf.size → Sort u_3) →
      (r : Std.DTreeMap.Internal.Impl α β) →
        (hrb : r.Balanced) →
          (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size Std.DTreeMap.Internal.Impl.leaf.size) →
            ((hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                (hlr :
                    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond Std.DTreeMap.Internal.Impl.leaf.size
                      Std.DTreeMap.Internal.Impl.leaf.size) →
                  motive Std.DTreeMap.Internal.Impl.leaf hrb hlr) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (hrb :
                          (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf
                              Std.DTreeMap.Internal.Impl.leaf).Balanced) →
                        (hlr :
                            Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                              (Std.DTreeMap.Internal.Impl.inner size k v 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 v Std.DTreeMap.Internal.Impl.leaf
                              Std.DTreeMap.Internal.Impl.leaf)
                            hrb hlr) →
                ((size : ℕ) →
                    (rk : α) →
                      (rv : β rk) →
                        (size_1 : ℕ) →
                          (k : α) →
                            (v : β k) →
                              (l r : Std.DTreeMap.Internal.Impl α β) →
                                (hrb :
                                    (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                                        (Std.DTreeMap.Internal.Impl.inner size_1 k v l r)).Balanced) →
                                  (hlr :
                                      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                                        (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                                            (Std.DTreeMap.Internal.Impl.inner size_1 k v l r)).size
                                        Std.DTreeMap.Internal.Impl.leaf.size) →
                                    motive
                                      (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                                        (Std.DTreeMap.Internal.Impl.inner size_1 k v l r))
                                      hrb hlr) →
                  ((size : ℕ) →
                      (rk : α) →
                        (rv : β rk) →
                          (size_1 : ℕ) →
                            (rlk : α) →
                              (rlv : β rlk) →
                                (l r : Std.DTreeMap.Internal.Impl α β) →
                                  (hrb :
                                      (Std.DTreeMap.Internal.Impl.inner size rk rv
                                          (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                                          Std.DTreeMap.Internal.Impl.leaf).Balanced) →
                                    (hlr :
                                        Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                                          (Std.DTreeMap.Internal.Impl.inner size rk rv
                                              (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                                              Std.DTreeMap.Internal.Impl.leaf).size
                                          Std.DTreeMap.Internal.Impl.leaf.size) →
                                      motive
                                        (Std.DTreeMap.Internal.Impl.inner size rk rv
                                          (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                                          Std.DTreeMap.Internal.Impl.leaf)
                                        hrb hlr) →
                    ((rs : ℕ) →
                        (rk : α) →
                          (rv : β rk) →
                            (rls : ℕ) →
                              (rlk : α) →
                                (rlv : β rlk) →
                                  (rll rlr : Std.DTreeMap.Internal.Impl α β) →
                                    (rrs : ℕ) →
                                      (k : α) →
                                        (v : β k) →
                                          (l r : Std.DTreeMap.Internal.Impl α β) →
                                            (hrb :
                                                (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                                    (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
                                                    (Std.DTreeMap.Internal.Impl.inner rrs k v l r)).Balanced) →
                                              (hlr :
                                                  Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                                                    (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                                        (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
                                                        (Std.DTreeMap.Internal.Impl.inner rrs k v l r)).size
                                                    Std.DTreeMap.Internal.Impl.leaf.size) →
                                                motive
                                                  (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                                    (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
                                                    (Std.DTreeMap.Internal.Impl.inner rrs k v l r))
                                                  hrb hlr) →
                      motive r hrb hlr