apply dite (r a a₁) <;> intro haa₁
case e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
c : α
hac : r a c
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
c : α
hac : r a c
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst

case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
c : α
hac : r a c
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst