-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL.match_3.congr_eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (rs : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (ls : ℕ) (lk : α)
  (lv : β lk)
  (motive :
    (ll lr : Std.DTreeMap.Internal.Impl α β) →
      (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced →
        Std.DTreeMap.Internal.Impl.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
            (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
          Sort u_3)
  (ll lr : Std.DTreeMap.Internal.Impl α β) (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
      (Std.DTreeMap.Internal.Impl.inner rs k v l r).size)
  (h_1 :
    (lls : ℕ) →
      (k_1 : α) →
        (v_1 : β k_1) →
          (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    (hlb :
                        (Std.DTreeMap.Internal.Impl.inner ls lk lv
                            (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l_1 r_1)
                            (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced) →
                      (hlr :
                          Std.DTreeMap.Internal.Impl.BalanceLPrecond
                            (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l_1 r_1)
                                (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                            (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                        motive (Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l_1 r_1)
                          (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr) hlb hlr)
  (h_2 :
    (size : ℕ) →
      (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 size k_1 v_1 l_1 r_1)
                    Std.DTreeMap.Internal.Impl.leaf).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond
                    (Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l_1 r_1)
                        Std.DTreeMap.Internal.Impl.leaf).size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l_1 r_1) Std.DTreeMap.Internal.Impl.leaf hlb hlr)
  (h_3 :
    (x : Std.DTreeMap.Internal.Impl α β) →
      (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv Std.DTreeMap.Internal.Impl.leaf x).Balanced) →
        (hlr :
            Std.DTreeMap.Internal.Impl.BalanceLPrecond
              (Std.DTreeMap.Internal.Impl.inner ls lk lv Std.DTreeMap.Internal.Impl.leaf x).size
              (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
          motive Std.DTreeMap.Internal.Impl.leaf x hlb hlr)
  (x : Std.DTreeMap.Internal.Impl α β)
  (hlb_1 : (Std.DTreeMap.Internal.Impl.inner ls lk lv Std.DTreeMap.Internal.Impl.leaf x).Balanced)
  (hlr_1 :
    Std.DTreeMap.Internal.Impl.BalanceLPrecond
      (Std.DTreeMap.Internal.Impl.inner ls lk lv Std.DTreeMap.Internal.Impl.leaf x).size
      (Std.DTreeMap.Internal.Impl.inner rs k v l r).size),
  ll = Std.DTreeMap.Internal.Impl.leaf →
    lr = x →
      hlb ≍ hlb_1 →
        hlr = hlr_1 →
          (match ll, lr, hlb, hlr with
            | Std.DTreeMap.Internal.Impl.inner lls k_1 v_1 l_1 r_1,
              Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr, hlb, hlr =>
              h_1 lls k_1 v_1 l_1 r_1 lrs lrk lrv lrl lrr hlb hlr
            | Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l_1 r_1, Std.DTreeMap.Internal.Impl.leaf, hlb, hlr =>
              h_2 size k_1 v_1 l_1 r_1 hlb hlr
            | Std.DTreeMap.Internal.Impl.leaf, x, hlb, hlr => h_3 x hlb hlr) ≍
            h_3 x hlb_1 hlr_1