internlm/Lean-Github huggingface dataset:
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₁
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
Tactic:
cases this
Proof state after:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
ys : KVChain r fun a => β a
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
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁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.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
ys : KVChain r fun a => β a
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
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁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_rfl]
Proof state after:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
ys : KVChain r fun a => β a
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
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁a haa₁ : ¬r a a
⊢ (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
            { val := (KVChain.cons a bf xs haxs, ys),
              property :=
                (_ : hingeable (KVChain.cons a bf xs haxs) (KVChain.cons a bf xs haxs, ys).snd) }).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.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
ys : KVChain r fun a => β a
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
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁a haa₁ : ¬r a a
⊢ (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
            { val := (KVChain.cons a bf xs haxs, ys),
              property :=
                (_ : hingeable (KVChain.cons a bf xs haxs) (KVChain.cons a bf xs haxs, ys).snd) }).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_rfl]
Proof state after:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
ys : KVChain r fun a => β a
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
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁a haa₁ : ¬r a a
⊢ (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
            { val := (KVChain.cons a bf xs haxs, ys),
              property :=
                (_ : hingeable (KVChain.cons a bf xs haxs) (KVChain.cons a bf xs haxs, ys).snd) }).val.fst.toList =
    (Option.casesOn (f a b₁ b)
              { val := (KVChain.nil, ys), property := (_ : hingeable (KVChain.nil, ys).fst (KVChain.nil, ys).snd) }
              fun bf =>
              { val := (KVChain.cons a bf KVChain.nil True.intro, ys),
                property :=
                  (_ :
                    hingeable (KVChain.cons a bf KVChain.nil True.intro)
                      (KVChain.cons a bf KVChain.nil True.intro, ys).snd) }).val.fst.toList ++
      xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
Proof state before:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
ys : KVChain r fun a => β a
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
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁a haa₁ : ¬r a a
⊢ (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
            { val := (KVChain.cons a bf xs haxs, ys),
              property :=
                (_ : hingeable (KVChain.cons a bf xs haxs) (KVChain.cons a bf xs haxs, ys).snd) }).val.fst.toList =
    (Option.casesOn (f a b₁ b)
              { val := (KVChain.nil, ys), property := (_ : hingeable (KVChain.nil, ys).fst (KVChain.nil, ys).snd) }
              fun bf =>
              { val := (KVChain.cons a bf KVChain.nil True.intro, ys),
                property :=
                  (_ :
                    hingeable (KVChain.cons a bf KVChain.nil True.intro)
                      (KVChain.cons a bf KVChain.nil True.intro, ys).snd) }).val.fst.toList ++
      xs.toList
Tactic:
cases f a b₁ b <;> rfl
Proof state after:
no goals
Theorem: KVChain.toList_snd_insertWithAux_inv
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
ys : KVChain r β
hxsys : hingeable xs ys
a : α
b : β a
haxs : boundLeft a xs
⊢ (insertWithAux f xs ys hxsys a b haxs).val.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
Tactic:
revert xs
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
⊢ ∀ {xs : KVChain (flip r) β} {hxsys : hingeable xs ys} {haxs : boundLeft a xs},
    (insertWithAux f xs ys hxsys a b haxs).val.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
Theorem: KVChain.toList_snd_insertWithAux_inv
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
⊢ ∀ {xs : KVChain (flip r) β} {hxsys : hingeable xs ys} {haxs : boundLeft a xs},
    (insertWithAux f xs ys hxsys a b haxs).val.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
Tactic:
apply ys.recOnList (motive:=λ ys =>∀ xs hxsys haxs, (insertWithAux f xs ys hxsys a b haxs).val.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd)
Proof state after:
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
⊢ ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs KVChain.nil) (haxs : boundLeft a xs),
    (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd =
      (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd

case cons
α : 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_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            (insertWithAux f xs ys hxsys a b haxs).val.snd =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd)
        xs →
      (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            (insertWithAux f xs ys hxsys a b haxs).val.snd =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd)
        (KVChain.cons a_1 b_1 xs haxs)
Theorem: KVChain.toList_snd_insertWithAux_inv
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
⊢ ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs KVChain.nil) (haxs : boundLeft a xs),
    (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd =
      (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd
Tactic:
case nil => intros; rfl
Proof state after:
no goals
Theorem: KVChain.toList_snd_insertWithAux_inv
Proof state before:
α : 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_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            (insertWithAux f xs ys hxsys a b haxs).val.snd =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd)
        xs →
      (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            (insertWithAux f xs ys hxsys a b haxs).val.snd =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd)
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
case cons =>
  intro a₁ b₁ ys ha₁ys h_ind xs hxsys haxs
  apply dite (r a₁ a) <;> intro ha₁a
  . rw [insertWithAux_cons_rel ha₁a]
    rw [insertWithAux_cons_rel ha₁a]
    rw [h_ind, h_ind ⟨[⟨a₁,b₁⟩], _⟩]
  . apply dite (r a a₁) <;> intro haa₁
    . rw [insertWithAux_cons_flip haa₁]
      rw [insertWithAux_cons_flip haa₁]
    . 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_snd_insertWithAux_inv
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
⊢ ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs KVChain.nil) (haxs : boundLeft a xs),
    (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd =
      (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd
Tactic:
intros
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
xs✝ : KVChain (flip r) fun a => β a
hxsys✝ : hingeable xs✝ KVChain.nil
haxs✝ : boundLeft a xs✝
⊢ (insertWithAux f xs✝ KVChain.nil hxsys✝ a b haxs✝).val.snd =
    (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd
Theorem: KVChain.toList_snd_insertWithAux_inv
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
xs✝ : KVChain (flip r) fun a => β a
hxsys✝ : hingeable xs✝ KVChain.nil
haxs✝ : boundLeft a xs✝
⊢ (insertWithAux f xs✝ KVChain.nil hxsys✝ a b haxs✝).val.snd =
    (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd
Tactic:
rfl
Proof state after:
no goals
Theorem: KVChain.toList_snd_insertWithAux_inv
Proof state before:
α : 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_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            (insertWithAux f xs ys hxsys a b haxs).val.snd =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd)
        xs →
      (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            (insertWithAux f xs ys hxsys a b haxs).val.snd =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd)
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
intro a₁ b₁ ys ha₁ys h_ind xs hxsys haxs
Proof state after:
α : 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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd
Theorem: KVChain.toList_snd_insertWithAux_inv
Proof state before:
α : 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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd
Tactic:
apply dite (r a₁ a) <;> intro 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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : 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) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd

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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : 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) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd
Theorem: KVChain.toList_snd_insertWithAux_inv
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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : 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) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd

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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : 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) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd
Tactic:
. rw [insertWithAux_cons_rel ha₁a]
  rw [insertWithAux_cons_rel ha₁a]
  rw [h_ind, h_ind ⟨[⟨a₁,b₁⟩], _⟩]
Proof state after:
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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : 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) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd
Theorem: KVChain.toList_snd_insertWithAux_inv
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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : 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) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd
Tactic:
. apply dite (r a a₁) <;> intro haa₁
  . rw [insertWithAux_cons_flip haa₁]
    rw [insertWithAux_cons_flip haa₁]
  . 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_snd_insertWithAux_inv
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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : 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) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd
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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : 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.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd