-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.link.fun_cases_unfolding : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k)
  (motive :
    (l r : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced → r.Balanced → Std.DTreeMap.Internal.Impl.Tree α β (l.size + 1 + r.size) → Prop),
  (∀ (r : Std.DTreeMap.Internal.Impl α β) (hr : r.Balanced) (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
      let d := Std.DTreeMap.Internal.Impl.insertMin k v r ⋯;
      Std.DTreeMap.Internal.Impl.leaf.Balanced →
        motive Std.DTreeMap.Internal.Impl.leaf r hr_1 hr { impl := d.impl, balanced_impl := ⋯, size_impl := ⋯ }) →
    (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
        (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced)
        (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
        let d := Std.DTreeMap.Internal.Impl.insertMax k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') ⋯;
        (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced →
          Std.DTreeMap.Internal.Impl.leaf.Balanced →
            motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') Std.DTreeMap.Internal.Impl.leaf hr hr_1
              { impl := d.impl, balanced_impl := ⋯, size_impl := ⋯ }) →
      (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
          (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) (sz_1 : ℕ) (k'_1 : α) (v'_1 : β k'_1)
          (l'_1 r'_1 : Std.DTreeMap.Internal.Impl α β)
          (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1).Balanced)
          (h : Std.DTreeMap.Internal.delta * sz < sz_1) (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced)
          (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').size + 1 + l'_1.size),
          Std.DTreeMap.Internal.Impl.link k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') l'_1 ⋯ ⋯ =
              { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } →
            (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced →
              (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1).Balanced →
                motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')
                  (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1) hr hr_1
                  { impl := Std.DTreeMap.Internal.Impl.balanceLErase k'_1 v'_1 ℓ r'_1 ⋯ ⋯ ⋯, balanced_impl := ⋯,
                    size_impl := ⋯ }) →
        (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) (sz_1 : ℕ) (k'_1 : α) (v'_1 : β k'_1)
            (l'_1 r'_1 : Std.DTreeMap.Internal.Impl α β)
            (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1).Balanced)
            (h : ¬Std.DTreeMap.Internal.delta * sz < sz_1) (h_1 : Std.DTreeMap.Internal.delta * sz_1 < sz)
            (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced)
            (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1).size),
            Std.DTreeMap.Internal.Impl.link k v r' (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1) ⋯ ⋯ =
                { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } →
              (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced →
                (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1).Balanced →
                  motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')
                    (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1) hr hr_1
                    { impl := Std.DTreeMap.Internal.Impl.balanceRErase k' v' l' ℓ ⋯ ⋯ ⋯, balanced_impl := ⋯,
                      size_impl := ⋯ }) →
          (∀ (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
              (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) (sz_1 : ℕ) (k'_1 : α) (v'_1 : β k'_1)
              (l'_1 r'_1 : Std.DTreeMap.Internal.Impl α β)
              (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1).Balanced)
              (h : ¬Std.DTreeMap.Internal.delta * sz < sz_1) (h_1 : ¬Std.DTreeMap.Internal.delta * sz_1 < sz),
              (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced →
                (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1).Balanced →
                  motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')
                    (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1) hr hr_1
                    {
                      impl :=
                        Std.DTreeMap.Internal.Impl.inner (sz + 1 + sz_1) k v
                          (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')
                          (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1),
                      balanced_impl := ⋯, size_impl := ⋯ }) →
            ∀ (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced),
              motive l r hl hr (Std.DTreeMap.Internal.Impl.link k v l r hl hr)