Theorem: KVChain.toList_mergeWith_cons_right
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a✝¹ : α
b : β a✝¹
ys : KVChain r β
hays : boundLeft a✝¹ ys
a : α
x : β a
hax : KVChain r fun a => β a
hpa : boundLeft a hax
a✝ :
  (mergeWith f hax (KVChain.cons a✝¹ b ys hays)).toList =
    List.reverseAux (insertWithAux f KVChain.nil hax True.intro a✝¹ b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil hax True.intro a✝¹ b True.intro).val.snd ys).toList
⊢ (mergeWith f (KVChain.cons a x hax hpa) (KVChain.cons a✝¹ b ys hays)).toList =
    List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a x hax hpa) True.intro a✝¹ b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a x hax hpa) True.intro a✝¹ b True.intro).val.snd
          ys).toList
Tactic:
conv =>
  lhs
  unfold mergeWith; unfold mergeWith.loop
  simp
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a✝¹ : α
b : β a✝¹
ys : KVChain r β
hays : boundLeft a✝¹ ys
a : α
x : β a
hax : KVChain r fun a => β a
hpa : boundLeft a hax
a✝ :
  (mergeWith f hax (KVChain.cons a✝¹ b ys hays)).toList =
    List.reverseAux (insertWithAux f KVChain.nil hax True.intro a✝¹ b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil hax True.intro a✝¹ b True.intro).val.snd ys).toList
⊢ (mergeWith.loop f
        (insertWithAux f KVChain.nil (KVChain.cons a x hax hpa) True.intro { fst := a✝¹, snd := b }.fst b
              (_ :
                List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                  (KVChain.cons a✝¹ b ys hays).toList)).1.fst
        (insertWithAux f KVChain.nil (KVChain.cons a x hax hpa) True.intro { fst := a✝¹, snd := b }.fst b
              (_ :
                List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                  (KVChain.cons a✝¹ b ys hays).toList)).1.snd
        (_ :
          hingeable
            (insertWithAux f KVChain.nil (KVChain.cons a x hax hpa) True.intro { fst := a✝¹, snd := b }.fst
                  { fst := a✝¹, snd := b }.snd
                  (_ :
                    List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                      (KVChain.cons a✝¹ b ys hays).toList)).val.fst
            (insertWithAux f KVChain.nil (KVChain.cons a x hax hpa) True.intro { fst := a✝¹, snd := b }.fst
                  { fst := a✝¹, snd := b }.snd
                  (_ :
                    List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                      (KVChain.cons a✝¹ b ys hays).toList)).val.snd)
        ys.toList (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
        (_ :
          List.predHead
            ((fun a_1 =>
                boundLeft a_1
                  (insertWithAux f KVChain.nil (KVChain.cons a x hax hpa) True.intro { fst := a✝¹, snd := b }.fst
                        { fst := a✝¹, snd := b }.snd
                        (_ :
                          List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                            (KVChain.cons a✝¹ b ys hays).toList)).1.fst) ∘
              Sigma.fst)
            ys.toList)).toList =
    List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a x hax hpa) True.intro a✝¹ b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a x hax hpa) True.intro a✝¹ b True.intro).val.snd
          ys).toList