-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceRErase.match_1.eq_4 : ∀ {α : 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)
  (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)
  (h_1 :
    (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)
  (h_2 :
    (r : Std.DTreeMap.Internal.Impl α β) →
      (size : ℕ) →
        (k : α) →
          (v : β k) →
            r =
                Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf
                  Std.DTreeMap.Internal.Impl.leaf →
              (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)
  (h_3 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rr : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    rr = Std.DTreeMap.Internal.Impl.inner size_2 k v l r →
                      (hrb :
                          (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                              (Std.DTreeMap.Internal.Impl.inner size_2 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_2 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_2 k v l r))
                            hrb hlr)
  (h_4 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (size_2 : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  (hrb :
                      (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_2 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_2 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_2 rlk rlv l r) Std.DTreeMap.Internal.Impl.leaf)
                        hrb hlr)
  (h_5 :
    (rs : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rl : Std.DTreeMap.Internal.Impl α β) →
            (rls : ℕ) →
              (rlk : α) →
                (rlv : β rlk) →
                  (rll rlr : Std.DTreeMap.Internal.Impl α β) →
                    rl = Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr →
                      (rr : Std.DTreeMap.Internal.Impl α β) →
                        (rrs : ℕ) →
                          (k : α) →
                            (v : β k) →
                              (l r : Std.DTreeMap.Internal.Impl α β) →
                                rr = Std.DTreeMap.Internal.Impl.inner rrs k v l r →
                                  (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),
  (match
      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 with
    | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => h_1 hrb hlr
    | r@h:(Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf),
      hrb, hlr => h_2 r size k v h hrb hlr
    |
    Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
        rr@h:(Std.DTreeMap.Internal.Impl.inner size_2 k v l r),
      hrb, hlr => h_3 size rk rv rr size_2 k v l r h hrb hlr
    |
    Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_2 rlk rlv l r)
        Std.DTreeMap.Internal.Impl.leaf,
      hrb, hlr => h_4 size rk rv size_2 rlk rlv l r hrb hlr
    |
    Std.DTreeMap.Internal.Impl.inner rs rk rv (rl@h:(Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr))
        rr@h_6:(Std.DTreeMap.Internal.Impl.inner rrs k v l r),
      hrb, hlr => h_5 rs rk rv rl rls rlk rlv rll rlr h rr rrs k v l r h_6 hrb hlr) =
    h_4 size rk rv size_1 rlk rlv l r hrb hlr