-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL!.match_1.congr_eq_5 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (l : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          motive
            (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (size_1 : ℕ) →
            (lrk : α) →
              (lrv : β lrk) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  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)))
  (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 →
                      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))
  (h_5 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll : Std.DTreeMap.Internal.Impl α β) →
            (size : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    ll = Std.DTreeMap.Internal.Impl.inner size k v l r →
                      (lr : Std.DTreeMap.Internal.Impl α β) →
                        (lrs : ℕ) →
                          (k_1 : α) →
                            (v_1 : β k_1) →
                              (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                                lr = Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_1 r_1 →
                                  motive
                                    (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                      (Std.DTreeMap.Internal.Impl.inner size k v l r)
                                      (Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_1 r_1)))
  (ls : ℕ) (lk : α) (lv : β lk) (size : ℕ) (k : α) (v : β k) (l_1 r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ)
  (k_1 : α) (v_1 : β k_1) (l_2 r_1 : Std.DTreeMap.Internal.Impl α β),
  l =
      Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner size k v l_1 r)
        (Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_2 r_1) →
    (match l with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf =>
        h_2 size k v
      |
      Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
          (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r) =>
        h_3 size lk lv size_1 lrk lrv l r
      |
      Std.DTreeMap.Internal.Impl.inner size lk lv (ll@h:(Std.DTreeMap.Internal.Impl.inner size_1 k v l r))
          Std.DTreeMap.Internal.Impl.leaf =>
        h_4 size lk lv ll size_1 k v l r h
      |
      Std.DTreeMap.Internal.Impl.inner ls lk lv (ll@h:(Std.DTreeMap.Internal.Impl.inner size k v l r))
          lr@h_6:(Std.DTreeMap.Internal.Impl.inner lrs k_2 v_2 l_3 r_2) =>
        h_5 ls lk lv ll size k v l r h lr lrs k_2 v_2 l_3 r_2 h_6) ≍
      h_5 ls lk lv (Std.DTreeMap.Internal.Impl.inner size k v l_1 r) size k v l_1 r ⋯
        (Std.DTreeMap.Internal.Impl.inner lrs k_1 v_1 l_2 r_1) lrs k_1 v_1 l_2 r_1 ⋯