internlm/Lean-Github huggingface dataset:
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst

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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst

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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Tactic:
. rw [insertWithAux_cons_rel ha₁a]
  exact h_ind _ (cons_hingeable.symm ▸ ha₁ys) (by exact ha₁a)
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Tactic:
. apply dite (r a a₁) <;> intro haa₁
  . rw [insertWithAux_cons_flip haa₁]
    exact hac
  . have : a = a₁ := Trichotomous.eq_of_incomp ⟨haa₁, ha₁a⟩
    cases this
    rw [insertWithAux_cons_rfl]
    cases f a b₁ b
    case none =>
      apply boundLeft_descend _ haxs
      exact λ _ => flip (trans (r:=r) (s:=r) (t:=r)) hac
    case some bf => exact hac
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c
    (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
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c
    (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
Tactic:
exact h_ind _ (cons_hingeable.symm ▸ ha₁ys) (by exact ha₁a)
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft a (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs))
Tactic:
exact ha₁a
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst

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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst

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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Tactic:
. rw [insertWithAux_cons_flip haa₁]
  exact hac
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Tactic:
. have : a = a₁ := Trichotomous.eq_of_incomp ⟨haa₁, ha₁a⟩
  cases this
  rw [insertWithAux_cons_rfl]
  cases f a b₁ b
  case none =>
    apply boundLeft_descend _ haxs
    exact λ _ => flip (trans (r:=r) (s:=r) (t:=r)) hac
  case some bf => exact hac
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.fst
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.fst
Tactic:
exact hac
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
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),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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₁
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
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
c : α
hac : r a c
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c (insertWithAux f xs (KVChain.cons a b₁ ys ha₁ys) ha₁xs a b haxs).val.fst
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
c : α
hac : r a c
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c
    (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
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c
    (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
Tactic:
cases f a b₁ b
Proof state after:
case e.e.refl.none
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
c : α
hac : r a c
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c
    (Option.casesOn none { 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

case e.e.refl.some
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
c : α
hac : r a c
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
val✝ : β a
⊢ boundLeft c
    (Option.casesOn (some val✝) { 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
Theorem: KVChain.boundLeft_insertWithAux_fst
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
c : α
hac : r a c
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
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
⊢ boundLeft c
    (Option.casesOn none { 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
Tactic:
case none =>
  apply boundLeft_descend _ haxs
  exact λ _ => flip (trans (r:=r) (s:=r) (t:=r)) hac
Proof state after:
no goals