exact hda₁
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
d : α
ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r fun a => β a
ha₂ys : boundLeft a₂ ys
xs✝ : KVChain r fun a => β a
hda₂ : boundLeft d (KVChain.cons a₂ b₂ ys ha₂ys)
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ :
  (∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
    boundLeft d xs → boundLeft d (mergeWith f xs (KVChain.cons a₂ b₂ ys ha₂ys))
h_ind_ys : ∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)
hda₁ : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
ha₁a₂ : r a₁ a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    ({ fst := a₁, snd := b₁ } ::
      List.reverseAux (insertWithAux f KVChain.nil xs True.intro a₂ b₂ True.intro).val.fst.toList
        (mergeWith f
            (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil True.intro) xs
                  (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil True.intro) xs) a₂ b₂ ha₁a₂).1.snd
            { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
no goals