internlm/Lean-Github huggingface dataset:
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
rw [insertWithAux_cons_rel ha₁a]
Proof state after:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
            (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
            (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
rw [insertWithAux_cons_rel ha₁a]
Proof state after:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
            (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a).val.fst.toList =
    (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) ys
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) ys) a b
              ha₁a).val.fst.toList ++
      xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
            (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a).val.fst.toList =
    (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) ys
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) ys) a b
              ha₁a).val.fst.toList ++
      xs.toList
Tactic:
rw [h_ind (xs.cons a₁ b₁ _), h_ind ⟨[⟨a₁,b₁⟩], _⟩]
Proof state after:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++
      (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)).toList =
    (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++
        { toList := [{ fst := a₁, snd := b₁ }],
            ascend :=
              (_ :
                List.Ascending (Sigma.relOnFst (flip r)) ({ fst := a₁, snd := b₁ } :: KVChain.nil.toList)) }.toList ++
      xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++
      (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)).toList =
    (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++
        { toList := [{ fst := a₁, snd := b₁ }],
            ascend :=
              (_ :
                List.Ascending (Sigma.relOnFst (flip r)) ({ fst := a₁, snd := b₁ } :: KVChain.nil.toList)) }.toList ++
      xs.toList
Tactic:
rw [KVChain.toList_cons]
Proof state after:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ { fst := a₁, snd := b₁ } :: xs.toList =
    (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++
        { toList := [{ fst := a₁, snd := b₁ }],
            ascend :=
              (_ :
                List.Ascending (Sigma.relOnFst (flip r)) ({ fst := a₁, snd := b₁ } :: KVChain.nil.toList)) }.toList ++
      xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ { fst := a₁, snd := b₁ } :: xs.toList =
    (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++
        { toList := [{ fst := a₁, snd := b₁ }],
            ascend :=
              (_ :
                List.Ascending (Sigma.relOnFst (flip r)) ({ fst := a₁, snd := b₁ } :: KVChain.nil.toList)) }.toList ++
      xs.toList
Tactic:
dsimp
Proof state after:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ { fst := a₁, snd := b₁ } :: xs.toList =
    (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ [{ fst := a₁, snd := b₁ }] ++ xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : r a₁ a
⊢ (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ { fst := a₁, snd := b₁ } :: xs.toList =
    (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ [{ fst := a₁, snd := b₁ }] ++ xs.toList
Tactic:
rw [List.append_cons]
Proof state after:
no goals
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
apply dite (r a a₁) <;> intro haa₁
Proof state after:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList

case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList

case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
. rw [insertWithAux_cons_flip haa₁]
  rw [insertWithAux_cons_flip haa₁]
  rfl
Proof state after:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
. have : a = a₁ := Trichotomous.eq_of_incomp ⟨haa₁, ha₁a⟩
  cases this
  rw [insertWithAux_cons_rfl]
  rw [insertWithAux_cons_rfl]
  cases f a b₁ b <;> rfl
Proof state after:
no goals
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
rw [insertWithAux_cons_flip haa₁]
Proof state after:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
rw [insertWithAux_cons_flip haa₁]
Proof state after:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.fst.toList =
    { val := (KVChain.cons a b KVChain.nil True.intro, KVChain.cons a₁ b₁ ys ha₁ys),
              property := haa₁ }.val.fst.toList ++
      xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.fst.toList =
    { val := (KVChain.cons a b KVChain.nil True.intro, KVChain.cons a₁ b₁ ys ha₁ys),
              property := haa₁ }.val.fst.toList ++
      xs.toList
Tactic:
rfl
Proof state after:
no goals
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
have : a = a₁ := Trichotomous.eq_of_incomp ⟨haa₁, ha₁a⟩
Proof state after:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
this : a = a₁
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList