Theorem: KVChain.toList_mergeWith_loop_eq_reverseAux (Algdata/Data/KVChain/MergeWith.lean)

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs_r : KVChain (flip r) β
xs : KVChain r β
hxs : hingeable xs_r xs
⊢ ∀ {ys : List (Sigma β)} {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
Tactic:
intro ys
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs_r : KVChain (flip r) β
xs : KVChain r β
hxs : hingeable xs_r xs
ys : List (Sigma β)
⊢ ∀ {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs_r : KVChain (flip r) β
xs : KVChain r β
hxs : hingeable xs_r xs
ys : List (Sigma β)
⊢ ∀ {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
Tactic:
revert xs_r xs
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : List (Sigma β)
⊢ ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : List (Sigma β)
⊢ ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
Tactic:
induction ys <;> dsimp
State after:
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
⊢ ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) []}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) []},
    (mergeWith.loop f xs_r xs hxs [] hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := [], ascend := hascend }).toList

case cons
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) tail✝}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) tail✝},
    (mergeWith.loop f xs_r xs hxs tail✝ hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := tail✝, ascend := hascend }).toList
⊢ ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) (head✝ :: tail✝)}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (head✝ :: tail✝)},
    (mergeWith.loop f xs_r xs hxs (head✝ :: tail✝) hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := head✝ :: tail✝, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
⊢ ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) []}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) []},
    (mergeWith.loop f xs_r xs hxs [] hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := [], ascend := hascend }).toList
Tactic:
case nil => intros; rfl
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
⊢ ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) []}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) []},
    (mergeWith.loop f xs_r xs hxs [] hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := [], ascend := hascend }).toList
Tactic:
intros
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs_r✝ : KVChain (flip r) β
xs✝ : KVChain r β
hxs✝ : hingeable xs_r✝ xs✝
hascend✝ : List.Ascending (Sigma.relOnFst r) []
hxsys✝ : List.predHead ((fun a => boundLeft a xs_r✝) ∘ Sigma.fst) []
⊢ (mergeWith.loop f xs_r✝ xs✝ hxs✝ [] hascend✝ hxsys✝).toList =
    List.reverseAux xs_r✝.toList (mergeWith f xs✝ { toList := [], ascend := hascend✝ }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs_r✝ : KVChain (flip r) β
xs✝ : KVChain r β
hxs✝ : hingeable xs_r✝ xs✝
hascend✝ : List.Ascending (Sigma.relOnFst r) []
hxsys✝ : List.predHead ((fun a => boundLeft a xs_r✝) ∘ Sigma.fst) []
⊢ (mergeWith.loop f xs_r✝ xs✝ hxs✝ [] hascend✝ hxsys✝).toList =
    List.reverseAux xs_r✝.toList (mergeWith f xs✝ { toList := [], ascend := hascend✝ }).toList
Tactic:
rfl
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
⊢ ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)},
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
Tactic:
intro xs_r xs hxs hascend hyxs
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hxs : hingeable xs_r xs
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
    List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hxs : hingeable xs_r xs
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
    List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
Tactic:
unfold mergeWith.loop
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hxs : hingeable xs_r xs
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ (match xs.toList with
      | [] =>
        hinge xs_r { toList := y :: ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) (y :: ys)) }
          (_ : hingeable xs_r { toList := y :: ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) (y :: ys)) })
      | head :: tail =>
        match hmatch : insertWithAux f xs_r xs hxs y.fst y.snd hyxs with
        | { val := (xs_r', xs'), property := h } =>
          mergeWith.loop f xs_r' xs' h ys (_ : List.Ascending (Sigma.relOnFst r) ys)
            (_ : List.predHead ((fun a => boundLeft a xs_r') ∘ Sigma.fst) ys)).toList =
    List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hxs : hingeable xs_r xs
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ (match xs.toList with
      | [] =>
        hinge xs_r { toList := y :: ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) (y :: ys)) }
          (_ : hingeable xs_r { toList := y :: ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) (y :: ys)) })
      | head :: tail =>
        match hmatch : insertWithAux f xs_r xs hxs y.fst y.snd hyxs with
        | { val := (xs_r', xs'), property := h } =>
          mergeWith.loop f xs_r' xs' h ys (_ : List.Ascending (Sigma.relOnFst r) ys)
            (_ : List.predHead ((fun a => boundLeft a xs_r') ∘ Sigma.fst) ys)).toList =
    List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
Tactic:
revert hxs
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ ∀ {hxs : hingeable xs_r xs},
    (match xs.toList with
        | [] =>
          hinge xs_r { toList := y :: ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) (y :: ys)) }
            (_ : hingeable xs_r { toList := y :: ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) (y :: ys)) })
        | head :: tail =>
          match hmatch : insertWithAux f xs_r xs hxs y.fst y.snd hyxs with
          | { val := (xs_r', xs'), property := h } =>
            mergeWith.loop f xs_r' xs' h ys (_ : List.Ascending (Sigma.relOnFst r) ys)
              (_ : List.predHead ((fun a => boundLeft a xs_r') ∘ Sigma.fst) ys)).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ ∀ {hxs : hingeable xs_r xs},
    (match xs.toList with
        | [] =>
          hinge xs_r { toList := y :: ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) (y :: ys)) }
            (_ : hingeable xs_r { toList := y :: ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) (y :: ys)) })
        | head :: tail =>
          match hmatch : insertWithAux f xs_r xs hxs y.fst y.snd hyxs with
          | { val := (xs_r', xs'), property := h } =>
            mergeWith.loop f xs_r' xs' h ys (_ : List.Ascending (Sigma.relOnFst r) ys)
              (_ : List.predHead ((fun a => boundLeft a xs_r') ∘ Sigma.fst) ys)).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
Tactic:
apply xs.recOnList (motive:=λ xs=> ∀ hxs, (mergeWith.loop f xs_r xs hxs (y::ys) hascend hyxs).toList = List.reverseAux xs_r.toList (mergeWith f xs ⟨(y::ys), hascend⟩).toList)
State after:
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ ∀ (hxs : hingeable xs_r KVChain.nil),
    (mergeWith.loop f xs_r KVChain.nil hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f KVChain.nil { toList := y :: ys, ascend := hascend }).toList

case cons
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ ∀ (a : α) (b : β a) (xs : KVChain r fun a => β a) (haxs : boundLeft a xs),
    (fun xs =>
          ∀ (hxs : hingeable xs_r xs),
            (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
              List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList)
        xs →
      (fun xs =>
          ∀ (hxs : hingeable xs_r xs),
            (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
              List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList)
        (KVChain.cons a b xs haxs)

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ ∀ (hxs : hingeable xs_r KVChain.nil),
    (mergeWith.loop f xs_r KVChain.nil hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f KVChain.nil { toList := y :: ys, ascend := hascend }).toList
Tactic:
case nil =>
  intro hxy; rfl
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ ∀ (hxs : hingeable xs_r KVChain.nil),
    (mergeWith.loop f xs_r KVChain.nil hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f KVChain.nil { toList := y :: ys, ascend := hascend }).toList
Tactic:
intro hxy
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
hxy : hingeable xs_r KVChain.nil
⊢ (mergeWith.loop f xs_r KVChain.nil hxy (y :: ys) hascend hyxs).toList =
    List.reverseAux xs_r.toList (mergeWith f KVChain.nil { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
hxy : hingeable xs_r KVChain.nil
⊢ (mergeWith.loop f xs_r KVChain.nil hxy (y :: ys) hascend hyxs).toList =
    List.reverseAux xs_r.toList (mergeWith f KVChain.nil { toList := y :: ys, ascend := hascend }).toList
Tactic:
rfl
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ ∀ (a : α) (b : β a) (xs : KVChain r fun a => β a) (haxs : boundLeft a xs),
    (fun xs =>
          ∀ (hxs : hingeable xs_r xs),
            (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
              List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList)
        xs →
      (fun xs =>
          ∀ (hxs : hingeable xs_r xs),
            (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
              List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList)
        (KVChain.cons a b xs haxs)
Tactic:
intro a b  xs haxs _ hxs
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ (mergeWith.loop f xs_r (KVChain.cons a b xs haxs) hxs (y :: ys) hascend hyxs).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ (mergeWith.loop f xs_r (KVChain.cons a b xs haxs) hxs (y :: ys) hascend hyxs).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
dsimp [mergeWith.loop]
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ (mergeWith.loop f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.fst
        (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
        (_ :
          hingeable (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).val.fst
            (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).val.snd)
        ys (_ : List.Ascending (Sigma.relOnFst r) ys)
        (_ :
          List.predHead
            ((fun a_1 => boundLeft a_1 (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.fst) ∘
              Sigma.fst)
            ys)).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ (mergeWith.loop f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.fst
        (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
        (_ :
          hingeable (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).val.fst
            (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).val.snd)
        ys (_ : List.Ascending (Sigma.relOnFst r) ys)
        (_ :
          List.predHead
            ((fun a_1 => boundLeft a_1 (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.fst) ∘
              Sigma.fst)
            ys)).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
rw [h_ind]
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.fst.toList
      (mergeWith f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.fst.toList
      (mergeWith f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
rw [toList_fst_insertWithAux_eq_append]
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList ++
        xs_r.toList)
      (mergeWith f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList ++
        xs_r.toList)
      (mergeWith f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
rw [toList_snd_insertWithAux_inv]
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList ++
        xs_r.toList)
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList ++
        xs_r.toList)
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
rw [List.reverseAux_append_left]
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverse xs_r.toList ++
      List.reverseAux
        (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList
        (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
            { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverse xs_r.toList ++
      List.reverseAux
        (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList
        (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
            { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
rw [List.reverseAux_eq_append (as:=xs_r.toList)]
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverse xs_r.toList ++
      List.reverseAux
        (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList
        (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
            { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList [] ++
      (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
conv =>
  rhs
  unfold mergeWith
  unfold mergeWith.loop
  rw [h_ind]
State after:
no goals