Theorem: KVChain.cons_mergeWith_cons_rfl (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₁ b₂ : β a
xs ys : KVChain r β
haxs : boundLeft a xs
hays : boundLeft a ys
⊢ mergeWith f (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays) =
    Option.casesOn (f a b₁ b₂) (mergeWith f xs ys) fun bf =>
      KVChain.cons a bf (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))
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₁ b₂ : β a
xs ys : KVChain r β
haxs : boundLeft a xs
hays : boundLeft a ys
⊢ (mergeWith f (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)).toList =
    (Option.casesOn (f a b₁ b₂) (mergeWith f xs ys) fun bf =>
        KVChain.cons a bf (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).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₁ b₂ : β a
xs ys : KVChain r β
haxs : boundLeft a xs
hays : boundLeft a ys
⊢ (mergeWith f (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)).toList =
    (Option.casesOn (f a b₁ b₂) (mergeWith f xs ys) fun bf =>
        KVChain.cons a bf (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).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₁ b₂ : β a
xs ys : KVChain r β
haxs : boundLeft a xs
hays : boundLeft a ys
⊢ List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a b₁ xs haxs) True.intro a b₂ True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b₁ xs haxs) True.intro a b₂ True.intro).val.snd
          ys).toList =
    (Option.casesOn (f a b₁ b₂) (mergeWith f xs ys) fun bf =>
        KVChain.cons a bf (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).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₁ b₂ : β a
xs ys : KVChain r β
haxs : boundLeft a xs
hays : boundLeft a ys
⊢ List.reverseAux (insertWithAux f KVChain.nil (KVChain.cons a b₁ xs haxs) True.intro a b₂ True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b₁ xs haxs) True.intro a b₂ True.intro).val.snd
          ys).toList =
    (Option.casesOn (f a b₁ b₂) (mergeWith f xs ys) fun bf =>
        KVChain.cons a bf (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList
Tactic:
rw [insertWithAux_cons_rfl]
State after:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b₁ b₂ : β a
xs ys : KVChain r β
haxs : boundLeft a xs
hays : boundLeft a ys
⊢ List.reverseAux
      (Option.casesOn (f a b₁ b₂)
              { val := (KVChain.nil, xs), property := (_ : hingeable (KVChain.nil, xs).fst (KVChain.nil, xs).snd) }
              fun bf =>
              { val := (KVChain.cons a bf KVChain.nil True.intro, xs),
                property :=
                  (_ :
                    hingeable (KVChain.cons a bf KVChain.nil True.intro)
                      (KVChain.cons a bf KVChain.nil True.intro, xs).snd) }).val.fst.toList
      (mergeWith f
          (Option.casesOn (f a b₁ b₂)
                { val := (KVChain.nil, xs), property := (_ : hingeable (KVChain.nil, xs).fst (KVChain.nil, xs).snd) }
                fun bf =>
                { val := (KVChain.cons a bf KVChain.nil True.intro, xs),
                  property :=
                    (_ :
                      hingeable (KVChain.cons a bf KVChain.nil True.intro)
                        (KVChain.cons a bf KVChain.nil True.intro, xs).snd) }).val.snd
          ys).toList =
    (Option.casesOn (f a b₁ b₂) (mergeWith f xs ys) fun bf =>
        KVChain.cons a bf (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).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₁ b₂ : β a
xs ys : KVChain r β
haxs : boundLeft a xs
hays : boundLeft a ys
⊢ List.reverseAux
      (Option.casesOn (f a b₁ b₂)
              { val := (KVChain.nil, xs), property := (_ : hingeable (KVChain.nil, xs).fst (KVChain.nil, xs).snd) }
              fun bf =>
              { val := (KVChain.cons a bf KVChain.nil True.intro, xs),
                property :=
                  (_ :
                    hingeable (KVChain.cons a bf KVChain.nil True.intro)
                      (KVChain.cons a bf KVChain.nil True.intro, xs).snd) }).val.fst.toList
      (mergeWith f
          (Option.casesOn (f a b₁ b₂)
                { val := (KVChain.nil, xs), property := (_ : hingeable (KVChain.nil, xs).fst (KVChain.nil, xs).snd) }
                fun bf =>
                { val := (KVChain.cons a bf KVChain.nil True.intro, xs),
                  property :=
                    (_ :
                      hingeable (KVChain.cons a bf KVChain.nil True.intro)
                        (KVChain.cons a bf KVChain.nil True.intro, xs).snd) }).val.snd
          ys).toList =
    (Option.casesOn (f a b₁ b₂) (mergeWith f xs ys) fun bf =>
        KVChain.cons a bf (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList
Tactic:
cases f a b₁ b₂ <;> rfl
State after:
no goals