rw [insertWithAux_cons_flip haa₁]
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ :
  boundLeft a xs →
    (insertWithAux f KVChain.nil xs True.intro a b True.intro).val =
      ({ toList := [{ fst := a, snd := b }],
          ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
        xs)
haa₁ : r a a₁
⊢ (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val =
    ({ toList := [{ fst := a, snd := b }],
        ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
      KVChain.cons a₁ b₁ xs ha₁xs)
no goals