internlm/Lean-Github huggingface dataset:
Theorem: KVChain.cons_mergeWith_rel
Proof 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
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✝ : β 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
Theorem: KVChain.cons_mergeWith_rel
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✝ : β 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]
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✝ : β 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
Theorem: KVChain.cons_mergeWith_rel
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✝ : β 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]
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✝ : β 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
Theorem: KVChain.cons_mergeWith_rel
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✝ : β 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]
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✝ : β 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
Theorem: KVChain.cons_mergeWith_rel
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✝ : β 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]
Proof state after:
no goals
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} (haxs : boundLeft a xs),
    mergeWith f xs (KVChain.cons a b ys hays) =
      KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))
Tactic:
intro xs a b ys hays haxs
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
haxs : boundLeft a xs
⊢ mergeWith f xs (KVChain.cons a b ys hays) = KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))
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
haxs : boundLeft a xs
⊢ mergeWith f xs (KVChain.cons a b ys hays) = KVChain.cons a b (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)
xs : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : boundLeft a xs
⊢ (mergeWith f xs (KVChain.cons a b ys hays)).toList =
    (KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList
Theorem: KVChain.mergeWith_cons_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 : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : boundLeft a xs
⊢ (mergeWith f xs (KVChain.cons a b ys hays)).toList =
    (KVChain.cons a b (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)
xs : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : boundLeft a xs
⊢ 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 b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList
Theorem: KVChain.mergeWith_cons_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 : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : boundLeft a xs
⊢ 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 b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList
Tactic:
suffices (insertWithAux f KVChain.nil xs True.intro a b True.intro).val = (⟨[⟨a,b⟩],List.Ascending.singleton _⟩,xs) by
  rw [this]; rfl
Proof state after:
case a
α : 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
haxs : 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)
Theorem: KVChain.mergeWith_cons_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 : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : 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)
Tactic:
revert haxs
Proof state after:
case a
α : 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
⊢ 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)
Theorem: KVChain.mergeWith_cons_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 : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
⊢ 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)
Tactic:
apply xs.recOnList (motive:=λ xs=> xs.boundLeft a → (insertWithAux f KVChain.nil xs _ _ _ _).val=_)
Proof state after:
case a.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
⊢ boundLeft a KVChain.nil →
    (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val =
      ({ toList := [{ fst := a, snd := b }],
          ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
        KVChain.nil)

case a.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 =>
          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))
        xs →
      (fun xs =>
          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))
        (KVChain.cons a_1 b_1 xs haxs)
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
⊢ boundLeft a KVChain.nil →
    (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val =
      ({ toList := [{ fst := a, snd := b }],
          ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
        KVChain.nil)
Tactic:
case a.nil => intros; rfl
Proof state after:
no goals
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_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs =>
          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))
        xs →
      (fun xs =>
          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))
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
case a.cons =>
  intro a₁ b₁ xs ha₁xs _ haa₁
  dsimp [boundLeft, List.predHead] at haa₁
  rw [insertWithAux_cons_flip haa₁]
Proof state after:
no goals
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
haxs : boundLeft a xs
this :
  (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)
⊢ 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 b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList
Tactic:
rw [this]
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
haxs : boundLeft a xs
this :
  (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)
⊢ List.reverseAux
      ({ toList := [{ fst := a, snd := b }],
              ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
            xs).fst.toList
      (mergeWith f
          ({ toList := [{ fst := a, snd := b }],
                ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
              xs).snd
          ys).toList =
    (KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList
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
haxs : boundLeft a xs
this :
  (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)
⊢ List.reverseAux
      ({ toList := [{ fst := a, snd := b }],
              ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
            xs).fst.toList
      (mergeWith f
          ({ toList := [{ fst := a, snd := b }],
                ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
              xs).snd
          ys).toList =
    (KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList
Tactic:
rfl
Proof state after:
no goals
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
⊢ boundLeft a KVChain.nil →
    (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val =
      ({ toList := [{ fst := a, snd := b }],
          ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
        KVChain.nil)
Tactic:
intros
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✝ : boundLeft a KVChain.nil
⊢ (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val =
    ({ toList := [{ fst := a, snd := b }],
        ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
      KVChain.nil)
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✝ : boundLeft a KVChain.nil
⊢ (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val =
    ({ toList := [{ fst := a, snd := b }],
        ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
      KVChain.nil)
Tactic:
rfl
Proof state after:
no goals
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_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs =>
          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))
        xs →
      (fun xs =>
          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))
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
intro a₁ b₁ xs ha₁xs _ 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₁ : 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)