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)
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]
Proof 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