internlm/Lean-Github huggingface dataset:
Theorem: KVChain.mergeWith_cons_flip
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₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ :
  boundLeft a xs →
    (insertWithAux f KVChain.nil xs True.intro a b True.intro).val =
      ({ toList := [{ fst := a, snd := b }],
          ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
        xs)
haa₁ : boundLeft a (KVChain.cons a₁ b₁ xs ha₁xs)
⊢ (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val =
    ({ toList := [{ fst := a, snd := b }],
        ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
      KVChain.cons a₁ b₁ xs ha₁xs)
Tactic:
dsimp [boundLeft, List.predHead] at haa₁
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₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ :
  boundLeft a xs →
    (insertWithAux f KVChain.nil xs True.intro a b True.intro).val =
      ({ toList := [{ fst := a, snd := b }],
          ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
        xs)
haa₁ : r a a₁
⊢ (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val =
    ({ toList := [{ fst := a, snd := b }],
        ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
      KVChain.cons a₁ b₁ xs ha₁xs)
Theorem: KVChain.mergeWith_cons_flip
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₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ :
  boundLeft a xs →
    (insertWithAux f KVChain.nil xs True.intro a b True.intro).val =
      ({ toList := [{ fst := a, snd := b }],
          ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
        xs)
haa₁ : r a a₁
⊢ (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val =
    ({ toList := [{ fst := a, snd := b }],
        ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
      KVChain.cons a₁ b₁ xs ha₁xs)
Tactic:
rw [insertWithAux_cons_flip haa₁]
Proof state after:
no goals
Theorem: KVChain.cons_mergeWith_cons_rfl
Proof 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
Proof 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
Theorem: KVChain.cons_mergeWith_cons_rfl
Proof 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]
Proof 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
Theorem: KVChain.cons_mergeWith_cons_rfl
Proof 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]
Proof 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
Theorem: KVChain.cons_mergeWith_cons_rfl
Proof 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
Proof state after:
no goals
Theorem: KVChain.mergeWith_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs ys x✝ : KVChain r β
⊢ mergeWith f KVChain.nil x✝ = mergeWith (fun a => flip (f a)) x✝ KVChain.nil
Tactic:
simp
Proof state after:
no goals
Theorem: KVChain.mergeWith_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys : KVChain r β
⊢ mergeWith f (KVChain.cons x₁ x₂ xs hxs) KVChain.nil =
    mergeWith (fun a => flip (f a)) KVChain.nil (KVChain.cons x₁ x₂ xs hxs)
Tactic:
simp
Proof state after:
no goals
Theorem: KVChain.mergeWith_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
⊢ mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys) =
    mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)
Tactic:
apply eq_of_toList_eq
Proof state after:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
apply dite (r x₁ y₁) <;> intro hx₁y₁
Proof state after:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList

case a.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList

case a.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
. rw [cons_mergeWith_cons_rel hx₁y₁]
  rw [cons_mergeWith_cons_flip hx₁y₁]
  dsimp
  rw [h_ind_xs]
Proof state after:
case a.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
. apply dite (r y₁ x₁) <;> intro hy₁x₁
  . rw [cons_mergeWith_cons_flip hy₁x₁]
    rw [cons_mergeWith_cons_rel hy₁x₁]
    dsimp
    rw [h_ind_ys]
  . have : x₁ = y₁ := Trichotomous.eq_of_incomp ⟨hx₁y₁, hy₁x₁⟩
    cases this
    rw [cons_mergeWith_cons_rfl, cons_mergeWith_cons_rfl]
    dsimp [flip] at *
    cases f x₁ x₂ y₂ <;> dsimp <;> rw [h_ind_xs]
Proof state after:
no goals
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
rw [cons_mergeWith_cons_rel hx₁y₁]
Proof state after:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : r x₁ y₁
⊢ (KVChain.cons x₁ x₂ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)))).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : r x₁ y₁
⊢ (KVChain.cons x₁ x₂ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)))).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
rw [cons_mergeWith_cons_flip hx₁y₁]
Proof state after:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : r x₁ y₁
⊢ (KVChain.cons x₁ x₂ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)))).toList =
    (KVChain.cons x₁ x₂ (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs)
        (_ : boundLeft x₁ (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs))).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : r x₁ y₁
⊢ (KVChain.cons x₁ x₂ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)))).toList =
    (KVChain.cons x₁ x₂ (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs)
        (_ : boundLeft x₁ (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs))).toList
Tactic:
dsimp
Proof state after:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : r x₁ y₁
⊢ { fst := x₁, snd := x₂ } :: (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)).toList =
    { fst := x₁, snd := x₂ } :: (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : r x₁ y₁
⊢ { fst := x₁, snd := x₂ } :: (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)).toList =
    { fst := x₁, snd := x₂ } :: (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs).toList
Tactic:
rw [h_ind_xs]
Proof state after:
no goals