-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL.match_1.congr_eq_4 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size → Sort u_3)
  (l : Std.DTreeMap.Internal.Impl α β) (hlb : l.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size)
  (h_1 :
    (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
            Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hlb hlr)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (hlb :
              (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf
                  Std.DTreeMap.Internal.Impl.leaf).Balanced) →
            (hlr :
                Std.DTreeMap.Internal.Impl.BalanceLPrecond
                  (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)
                hlb hlr)
  (h_3 :
    (size : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (size_1 : ℕ) →
            (lrk : α) →
              (lrv : β lrk) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  (hlb :
                      (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                          (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r)).Balanced) →
                    (hlr :
                        Std.DTreeMap.Internal.Impl.BalanceLPrecond
                          (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                              (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r)).size
                          Std.DTreeMap.Internal.Impl.leaf.size) →
                      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))
                        hlb hlr)
  (h_4 :
    (size : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    ll = Std.DTreeMap.Internal.Impl.inner size_1 k v l r →
                      (hlb :
                          (Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k v l r)
                              Std.DTreeMap.Internal.Impl.leaf).Balanced) →
                        (hlr :
                            Std.DTreeMap.Internal.Impl.BalanceLPrecond
                              (Std.DTreeMap.Internal.Impl.inner size lk lv
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k v l r)
                                  Std.DTreeMap.Internal.Impl.leaf).size
                              Std.DTreeMap.Internal.Impl.leaf.size) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size lk lv
                              (Std.DTreeMap.Internal.Impl.inner size_1 k v l r) Std.DTreeMap.Internal.Impl.leaf)
                            hlb hlr)
  (h_5 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (lls : ℕ) →
            (k : α) →
              (v : β k) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  (lrs : ℕ) →
                    (k_1 : α) →
                      (v_1 : β k_1) →
                        (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                          (hlb :
                              (Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                                  (Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_1 r_1)).Balanced) →
                            (hlr :
                                Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                  (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                      (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                                      (Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_1 r_1)).size
                                  Std.DTreeMap.Internal.Impl.leaf.size) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                  (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                                  (Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_1 r_1))
                                hlb hlr)
  (size : ℕ) (lk : α) (lv : β lk) (size_1 : ℕ) (k : α) (v : β k) (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (hlb_1 :
    (Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k v l_1 r)
        Std.DTreeMap.Internal.Impl.leaf).Balanced)
  (hlr_1 :
    Std.DTreeMap.Internal.Impl.BalanceLPrecond
      (Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k v l_1 r)
          Std.DTreeMap.Internal.Impl.leaf).size
      Std.DTreeMap.Internal.Impl.leaf.size),
  l =
      Std.DTreeMap.Internal.Impl.inner size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k v l_1 r)
        Std.DTreeMap.Internal.Impl.leaf →
    hlb ≍ hlb_1 →
      hlr ≍ hlr_1 →
        (match l, hlb, hlr with
          | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr => h_1 hlb hlr
          | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
            hlb, hlr => h_2 size k v hlb hlr
          |
          Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
              (Std.DTreeMap.Internal.Impl.inner size_2 lrk lrv l r),
            hlb, hlr => h_3 size lk lv size_2 lrk lrv l r hlb hlr
          |
          Std.DTreeMap.Internal.Impl.inner size lk lv (ll@h:(Std.DTreeMap.Internal.Impl.inner size_2 k v l r))
              Std.DTreeMap.Internal.Impl.leaf,
            hlb, hlr => h_4 size lk lv ll size_2 k v l r h hlb hlr
          |
          Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner lls k v l r)
              (Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_2 r_1),
            hlb, hlr => h_5 ls lk lv lls k v l r lrs k_1 v_1 l_2 r_1 hlb hlr) ≍
          h_4 size lk lv (Std.DTreeMap.Internal.Impl.inner size_1 k v l_1 r) size_1 k v l_1 r ⋯ hlb_1 hlr_1