Theorem: KVChain.toList_mergeWith_loop_eq_reverseAux
Proof 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)
Proof 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)