unfold insertWithAux
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a : α
b₁ : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : hingeable xs (KVChain.cons a b₁ ys hays)
b : β a
haxs' : boundLeft a xs
⊢ insertWithAux f xs (KVChain.cons a b₁ ys hays) haxs a b haxs' =
    Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
      { val := (KVChain.cons a bf xs haxs', ys),
        property := (_ : hingeable (KVChain.cons a bf xs haxs') (KVChain.cons a bf xs haxs', ys).snd) }
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a : α
b₁ : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : hingeable xs (KVChain.cons a b₁ ys hays)
b : β a
haxs' : boundLeft a xs
⊢ insertWithAux.loop f a b xs (KVChain.cons a b₁ ys hays).toList
      (_ : List.Ascending (Sigma.relOnFst r) (KVChain.cons a b₁ ys hays).toList)
      (_ :
        List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
          (KVChain.cons a b₁ ys hays).toList)
      haxs' =
    Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
      { val := (KVChain.cons a bf xs haxs', ys),
        property := (_ : hingeable (KVChain.cons a bf xs haxs') (KVChain.cons a bf xs haxs', ys).snd) }