-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!.match_1.congr_eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (r : 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 : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rr : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    rr = Std.DTreeMap.Internal.Impl.inner size_1 k v l r →
                      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)))
  (h_4 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (size_1 : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  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))
  (h_5 :
    (rs : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rls : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (rll rlr rr : Std.DTreeMap.Internal.Impl α β) →
                  (size : ℕ) →
                    (k : α) →
                      (v : β k) →
                        (l r : Std.DTreeMap.Internal.Impl α β) →
                          rr = Std.DTreeMap.Internal.Impl.inner size k v l r →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
                                (Std.DTreeMap.Internal.Impl.inner size k v l r)))
  (size : ℕ) (rk : α) (rv : β rk) (size_1 : ℕ) (k : α) (v : β k) (l r_1 : Std.DTreeMap.Internal.Impl α β),
  r =
      Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
        (Std.DTreeMap.Internal.Impl.inner size_1 k v l r_1) →
    (match r 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 rk rv Std.DTreeMap.Internal.Impl.leaf
          rr@h:(Std.DTreeMap.Internal.Impl.inner size_2 k v l r) =>
        h_3 size rk rv rr size_2 k v l r h
      |
      Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_2 rlk rlv l r)
          Std.DTreeMap.Internal.Impl.leaf =>
        h_4 size rk rv size_2 rlk rlv l r
      |
      Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
          rr@h:(Std.DTreeMap.Internal.Impl.inner size k v l r) =>
        h_5 rs rk rv rls rlk rlv rll rlr rr size k v l r h) ≍
      h_3 size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 k v l r_1) size_1 k v l r_1 ⋯