internlm/Lean-Github huggingface dataset:
Theorem: KVChain.insertWithAux_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 (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
haa₁ : r a a₁
⊢ (if hya : r a₁ a then
      insertWithAux.loop f a b
        (KVChain.cons a₁ b₁ xs
          (_ :
            List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
              (KVChain.cons a₁ b₁ ys ha₁ys).toList))
        ys.toList (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
        (_ : List.predHead (Sigma.relOnFst r { fst := a₁, snd := b₁ }) ys.toList) hya
    else
      if hay : r a a₁ then
        {
          val :=
            (KVChain.cons a b xs haxs,
              { toList := { fst := a₁, snd := b₁ } :: ys.toList,
                ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }),
          property :=
            (_ :
              hingeable
                (KVChain.cons a b xs haxs,
                    { toList := { fst := a₁, snd := b₁ } :: ys.toList,
                      ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }).fst
                (KVChain.cons a b xs haxs,
                    { toList := { fst := a₁, snd := b₁ } :: ys.toList,
                      ascend :=
                        (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }).snd) }
      else
        match f a₁ b₁ ((_ : a = { fst := a₁, snd := b₁ }.fst) ▸ b) with
        | none =>
          { val := (xs, { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
            property :=
              (_ : hingeable xs { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }
        | some z =>
          {
            val :=
              (KVChain.cons a₁ z xs
                  (_ :
                    List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                      (KVChain.cons a₁ b₁ ys ha₁ys).toList),
                { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
            property :=
              (_ :
                hingeable
                  (KVChain.cons a₁ z xs
                    (_ :
                      List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                        (KVChain.cons a₁ b₁ ys ha₁ys).toList))
                  { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }) =
    { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }
Tactic:
rw [dif_neg (Asymmetry.asymm _ _ haa₁), dif_pos haa₁]
Proof state after:
no goals
Theorem: KVChain.insertWithAux_cons_rfl
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) β
a : α
b₁ : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : hingeable xs (KVChain.cons a b₁ ys hays)
b : β a
haxs' : boundLeft a xs
⊢ insertWithAux f xs (KVChain.cons a b₁ ys hays) haxs a b haxs' =
    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) }
Tactic:
unfold insertWithAux
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a : α
b₁ : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : hingeable xs (KVChain.cons a b₁ ys hays)
b : β a
haxs' : boundLeft a xs
⊢ insertWithAux.loop f a b xs (KVChain.cons a b₁ ys hays).toList
      (_ : List.Ascending (Sigma.relOnFst r) (KVChain.cons a b₁ ys hays).toList)
      (_ :
        List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
          (KVChain.cons a b₁ ys hays).toList)
      haxs' =
    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) }
Theorem: KVChain.insertWithAux_cons_rfl
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) β
a : α
b₁ : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : hingeable xs (KVChain.cons a b₁ ys hays)
b : β a
haxs' : boundLeft a xs
⊢ insertWithAux.loop f a b xs (KVChain.cons a b₁ ys hays).toList
      (_ : List.Ascending (Sigma.relOnFst r) (KVChain.cons a b₁ ys hays).toList)
      (_ :
        List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
          (KVChain.cons a b₁ ys hays).toList)
      haxs' =
    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) }
Tactic:
conv in KVChain.cons a b₁ ys => unfold KVChain.cons
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a : α
b₁ : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : hingeable xs (KVChain.cons a b₁ ys hays)
b : β a
haxs' : boundLeft a xs
⊢ insertWithAux.loop f a b xs
      { toList := { fst := a, snd := b₁ } :: ys.toList,
          ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a, snd := b₁ } :: ys.toList)) }.toList
      (_ :
        List.Ascending (Sigma.relOnFst r)
          { toList := { fst := a, snd := b₁ } :: ys.toList,
              ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a, snd := b₁ } :: ys.toList)) }.toList)
      (_ :
        List.predHead ((fun a => boundLeft a xs) ∘ Sigma.fst)
          { toList := { fst := a, snd := b₁ } :: ys.toList,
              ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a, snd := b₁ } :: ys.toList)) }.toList)
      haxs' =
    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) }
Theorem: KVChain.insertWithAux_cons_rfl
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) β
a : α
b₁ : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : hingeable xs (KVChain.cons a b₁ ys hays)
b : β a
haxs' : boundLeft a xs
⊢ (match f a b₁ b with
    | none =>
      { val := (xs, { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
        property :=
          (_ : hingeable xs { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }
    | some z =>
      {
        val :=
          (KVChain.cons a z xs
              (_ :
                List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                  (KVChain.cons a b₁ ys hays).toList),
            { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
        property :=
          (_ :
            hingeable
              (KVChain.cons a z xs
                (_ :
                  List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                    (KVChain.cons a b₁ ys hays).toList))
              { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }) =
    Option.rec { val := (xs, ys), property := (_ : hingeable xs ys) }
      (fun val =>
        { val := (KVChain.cons a val xs haxs', ys), property := (_ : hingeable (KVChain.cons a val xs haxs') ys) })
      (f a b₁ b)
Tactic:
cases hf : f a b₁ b <;> rfl
Proof state after:
no goals
Theorem: KVChain.toList_fst_insertWithAux_eq_append
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.fst.toList =
    (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
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.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
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.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
apply ys.recOnList (motive:=λ ys=>∀ xs hxsys haxs, (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)
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.fst.toList =
      (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList ++ xs.toList

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.fst.toList =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList)
        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.fst.toList =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList)
        (KVChain.cons a_1 b_1 xs haxs)
Theorem: KVChain.toList_fst_insertWithAux_eq_append
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.fst.toList =
      (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList ++ xs.toList
Tactic:
case nil => intros; rfl
Proof state after:
no goals
Theorem: KVChain.toList_fst_insertWithAux_eq_append
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.fst.toList =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList)
        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.fst.toList =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList)
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
case cons =>
  intro a₁ b₁ ys ha₁ys h_ind xs ha₁xs haxs
  apply dite (r a₁ a) <;> intro ha₁a
  . rw [insertWithAux_cons_rel ha₁a]
    rw [insertWithAux_cons_rel ha₁a]
    rw [h_ind (xs.cons a₁ b₁ _), h_ind ⟨[⟨a₁,b₁⟩], _⟩]
    rw [KVChain.toList_cons]
    dsimp
    rw [List.append_cons]
  . apply dite (r a a₁) <;> intro haa₁
    . rw [insertWithAux_cons_flip haa₁]
      rw [insertWithAux_cons_flip haa₁]
      rfl
    . 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:
α : 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.fst.toList =
      (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList ++ xs.toList
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.fst.toList =
    (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList ++ xs✝.toList
Theorem: KVChain.toList_fst_insertWithAux_eq_append
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.fst.toList =
    (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList ++ xs✝.toList
Tactic:
rfl
Proof state after:
no goals
Theorem: KVChain.toList_fst_insertWithAux_eq_append
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.fst.toList =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList)
        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.fst.toList =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList)
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
intro a₁ b₁ ys ha₁ys h_ind xs ha₁xs 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.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
⊢ (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:
α : 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
⊢ (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 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 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
α : 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
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

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:
. rw [insertWithAux_cons_rel ha₁a]
  rw [insertWithAux_cons_rel ha₁a]
  rw [h_ind (xs.cons a₁ b₁ _), h_ind ⟨[⟨a₁,b₁⟩], _⟩]
  rw [KVChain.toList_cons]
  dsimp
  rw [List.append_cons]
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.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
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₁
  . rw [insertWithAux_cons_flip haa₁]
    rw [insertWithAux_cons_flip haa₁]
    rfl
  . 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