Theorem: KVChain.cons_mergeWith_rel (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)
⊢ ∀ {a : α} {b : β a} {xs : KVChain r β} {haxs : boundLeft a xs} {ys : KVChain r β} (hays : boundLeft a ys),
    mergeWith f (KVChain.cons a b xs haxs) ys =
      KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))
Tactic:
intro a b xs haxs ys
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
xs : KVChain r β
haxs : boundLeft a xs
ys : KVChain r β
⊢ ∀ (hays : boundLeft a ys),
    mergeWith f (KVChain.cons a b xs haxs) ys =
      KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
xs : KVChain r β
haxs : boundLeft a xs
ys : KVChain r β
⊢ ∀ (hays : boundLeft a ys),
    mergeWith f (KVChain.cons a b xs haxs) ys =
      KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))
Tactic:
revert xs
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
⊢ ∀ {xs : KVChain r β} {haxs : boundLeft a xs} (hays : boundLeft a ys),
    mergeWith f (KVChain.cons a b xs haxs) ys =
      KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
⊢ ∀ {xs : KVChain r β} {haxs : boundLeft a xs} (hays : boundLeft a ys),
    mergeWith f (KVChain.cons a b xs haxs) ys =
      KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))
Tactic:
apply ys.recOnList (motive:=λ ys => ∀ xs haxs hays, mergeWith f (xs.cons a b haxs) ys = (mergeWith f xs ys).cons a b (boundLeft_mergeWith a haxs hays))
State after:
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
⊢ ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a KVChain.nil),
    mergeWith f (KVChain.cons a b xs haxs) KVChain.nil =
      KVChain.cons a b (mergeWith f xs KVChain.nil) (_ : boundLeft a (mergeWith f xs KVChain.nil))

case cons
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a ys),
            mergeWith f (KVChain.cons a b xs haxs) ys =
              KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys)))
        xs →
      (fun ys =>
          ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a ys),
            mergeWith f (KVChain.cons a b xs haxs) ys =
              KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys)))
        (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)
a : α
b : β a
ys : KVChain r β
⊢ ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a KVChain.nil),
    mergeWith f (KVChain.cons a b xs haxs) KVChain.nil =
      KVChain.cons a b (mergeWith f xs KVChain.nil) (_ : boundLeft a (mergeWith f xs KVChain.nil))
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)
a : α
b : β a
ys : KVChain r β
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a ys),
            mergeWith f (KVChain.cons a b xs haxs) ys =
              KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys)))
        xs →
      (fun ys =>
          ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a ys),
            mergeWith f (KVChain.cons a b xs haxs) ys =
              KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys)))
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
case cons =>
  intro b y hby hpb _ x hax hab
  apply KVChain.eq_of_toList_eq
  rw [toList_mergeWith_cons_right]
  rw [KVChain.toList_cons]
  rw [toList_mergeWith_cons_right]
  conv =>
    lhs
    rw [insertWithAux_cons_rel hab]
    rw [toList_fst_insertWithAux_eq_append]
    rw [toList_snd_insertWithAux_inv]
    rw [List.reverseAux_append_left]
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
⊢ ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a KVChain.nil),
    mergeWith f (KVChain.cons a b xs haxs) KVChain.nil =
      KVChain.cons a b (mergeWith f xs KVChain.nil) (_ : boundLeft a (mergeWith f xs KVChain.nil))
Tactic:
intros
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
xs✝ : KVChain r fun a => β a
haxs✝ : boundLeft a xs✝
hays✝ : boundLeft a KVChain.nil
⊢ mergeWith f (KVChain.cons a b xs✝ haxs✝) KVChain.nil =
    KVChain.cons a b (mergeWith f xs✝ KVChain.nil) (_ : boundLeft a (mergeWith f xs✝ KVChain.nil))

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
xs✝ : KVChain r fun a => β a
haxs✝ : boundLeft a xs✝
hays✝ : boundLeft a KVChain.nil
⊢ mergeWith f (KVChain.cons a b xs✝ haxs✝) KVChain.nil =
    KVChain.cons a b (mergeWith f xs✝ KVChain.nil) (_ : boundLeft a (mergeWith f xs✝ KVChain.nil))
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)
a : α
b : β a
ys : KVChain r β
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a ys),
            mergeWith f (KVChain.cons a b xs haxs) ys =
              KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys)))
        xs →
      (fun ys =>
          ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a ys),
            mergeWith f (KVChain.cons a b xs haxs) ys =
              KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys)))
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
intro b y hby hpb _ x hax hab
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ mergeWith f (KVChain.cons a b✝ x hax) (KVChain.cons b y hby hpb) =
    KVChain.cons a b✝ (mergeWith f x (KVChain.cons b y hby hpb))
      (_ : boundLeft a (mergeWith f x (KVChain.cons b y hby hpb)))

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ mergeWith f (KVChain.cons a b✝ x hax) (KVChain.cons b y hby hpb) =
    KVChain.cons a b✝ (mergeWith f x (KVChain.cons b y hby hpb))
      (_ : boundLeft a (mergeWith f x (KVChain.cons b y hby hpb)))
Tactic:
apply KVChain.eq_of_toList_eq
State after:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ (mergeWith f (KVChain.cons a b✝ x hax) (KVChain.cons b y hby hpb)).toList =
    (KVChain.cons a b✝ (mergeWith f x (KVChain.cons b y hby hpb))
        (_ : boundLeft a (mergeWith f x (KVChain.cons b y hby hpb)))).toList

State before:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ (mergeWith f (KVChain.cons a b✝ x hax) (KVChain.cons b y hby hpb)).toList =
    (KVChain.cons a b✝ (mergeWith f x (KVChain.cons b y hby hpb))
        (_ : boundLeft a (mergeWith f x (KVChain.cons b y hby hpb)))).toList
Tactic:
rw [toList_mergeWith_cons_right]
State after:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.snd
          hby).toList =
    (KVChain.cons a b✝ (mergeWith f x (KVChain.cons b y hby hpb))
        (_ : boundLeft a (mergeWith f x (KVChain.cons b y hby hpb)))).toList

State before:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.snd
          hby).toList =
    (KVChain.cons a b✝ (mergeWith f x (KVChain.cons b y hby hpb))
        (_ : boundLeft a (mergeWith f x (KVChain.cons b y hby hpb)))).toList
Tactic:
rw [KVChain.toList_cons]
State after:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.snd
          hby).toList =
    { fst := a, snd := b✝ } :: (mergeWith f x (KVChain.cons b y hby hpb)).toList

State before:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.snd
          hby).toList =
    { fst := a, snd := b✝ } :: (mergeWith f x (KVChain.cons b y hby hpb)).toList
Tactic:
rw [toList_mergeWith_cons_right]
State after:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.snd
          hby).toList =
    { fst := a, snd := b✝ } ::
      List.reverseAux (insertWithAux f KVChain.nil x True.intro b y True.intro).val.fst.toList
        (mergeWith f (insertWithAux f KVChain.nil x True.intro b y True.intro).val.snd hby).toList

State before:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b✝ x hax) True.intro b y True.intro).val.snd
          hby).toList =
    { fst := a, snd := b✝ } ::
      List.reverseAux (insertWithAux f KVChain.nil x True.intro b y True.intro).val.fst.toList
        (mergeWith f (insertWithAux f KVChain.nil x True.intro b y True.intro).val.snd hby).toList
Tactic:
conv =>
  lhs
  rw [insertWithAux_cons_rel hab]
  rw [toList_fst_insertWithAux_eq_append]
  rw [toList_snd_insertWithAux_inv]
  rw [List.reverseAux_append_left]
State after:
no goals