Theorem: KVChain.toList_mergeWith_cons_right (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 : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
⊢ (mergeWith f xs (KVChain.cons a b ys hays)).toList =
    List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList
Tactic:
apply xs.recOnList (motive:=λ xs=>(mergeWith f xs (ys.cons a b hays)).toList=List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
State after:
case nil
α : 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
⊢ (mergeWith f KVChain.nil (KVChain.cons a b ys hays)).toList =
    List.reverseAux (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd ys).toList

case cons
α : 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_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs =>
          (mergeWith f xs (KVChain.cons a b ys hays)).toList =
            List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
              (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
        xs →
      (fun xs =>
          (mergeWith f xs (KVChain.cons a b ys hays)).toList =
            List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
              (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
        (KVChain.cons a_1 b_1 xs haxs)

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
⊢ (mergeWith f KVChain.nil (KVChain.cons a b ys hays)).toList =
    List.reverseAux (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd ys).toList
Tactic:
case nil =>
  rw [nil_mergeWith]
  dsimp [List.reverseAux]
  rw [nil_mergeWith]
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 : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs =>
          (mergeWith f xs (KVChain.cons a b ys hays)).toList =
            List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
              (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
        xs →
      (fun xs =>
          (mergeWith f xs (KVChain.cons a b ys hays)).toList =
            List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
              (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
case cons =>
  intro a x hax hpa _
  conv =>
    lhs
    unfold mergeWith; unfold mergeWith.loop
    simp
  rw [toList_mergeWith_loop_eq_reverseAux]
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 : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
⊢ (mergeWith f KVChain.nil (KVChain.cons a b ys hays)).toList =
    List.reverseAux (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd ys).toList
Tactic:
rw [nil_mergeWith]
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
⊢ (KVChain.cons a b ys hays).toList =
    List.reverseAux (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd ys).toList

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
⊢ (KVChain.cons a b ys hays).toList =
    List.reverseAux (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd ys).toList
Tactic:
dsimp [List.reverseAux]
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
⊢ { fst := a, snd := b } :: ys.toList = { fst := a, snd := b } :: (mergeWith f KVChain.nil ys).toList

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
⊢ { fst := a, snd := b } :: ys.toList = { fst := a, snd := b } :: (mergeWith f KVChain.nil ys).toList
Tactic:
rw [nil_mergeWith]
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 : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs =>
          (mergeWith f xs (KVChain.cons a b ys hays)).toList =
            List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
              (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
        xs →
      (fun xs =>
          (mergeWith f xs (KVChain.cons a b ys hays)).toList =
            List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
              (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
intro a x hax hpa _
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 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

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
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

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.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
Tactic:
rw [toList_mergeWith_loop_eq_reverseAux]
State after:
no goals