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
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
bf : β a
⊢ boundLeft c
    (Option.casesOn (some bf) { 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 some bf => exact hac
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
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:
apply boundLeft_descend _ 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
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
⊢ ∀ (a' : α), flip r a a' → flip r c a'
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
⊢ ∀ (a' : α), flip r a a' → flip r c a'
Tactic:
exact λ _ => flip (trans (r:=r) (s:=r) (t:=r)) hac
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
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
bf : β a
⊢ boundLeft c
    (Option.casesOn (some bf) { 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:
exact hac
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
⊢ ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
Tactic:
apply xs.recOnList (motive:=λ xs=>∀ d, xs.boundLeft d → r d a → (xs.insertWith f a b).boundLeft d)
Proof state after:
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
⊢ ∀ (d : α), boundLeft d KVChain.nil → r d a → boundLeft d (insertWith f KVChain.nil a b)

case cons
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs => ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)) xs →
      (fun xs => ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)) (KVChain.cons a_1 b_1 xs haxs)
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
⊢ ∀ (d : α), boundLeft d KVChain.nil → r d a → boundLeft d (insertWith f KVChain.nil a b)
Tactic:
case nil =>
  intro a _ hab
  rw [insertWith_nil]
  exact hab
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs => ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)) xs →
      (fun xs => ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)) (KVChain.cons a_1 b_1 xs haxs)
Tactic:
case cons =>
  intro a₁ b₁ xs ha₁xs _ d hdxs hda
  unfold insertWith
  dsimp [boundLeft]
  apply List.predHead_of_forAll
  rw [List.forAll_reverseAux]
  apply forAll_fst_insertWithAux
  . exact True.intro
  . apply (xs.cons a₁ b₁ ha₁xs).ascend.forAll_of_predHead
    . exact λ _ _ h₁ h₂ => trans (t:=r) h₁ h₂
    . exact hdxs
  . exact hda
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
⊢ ∀ (d : α), boundLeft d KVChain.nil → r d a → boundLeft d (insertWith f KVChain.nil a b)
Tactic:
intro a _ hab
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a✝¹ : α
b : β a✝¹
a : α
a✝ : boundLeft a KVChain.nil
hab : r a a✝¹
⊢ boundLeft a (insertWith f KVChain.nil a✝¹ b)
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a✝¹ : α
b : β a✝¹
a : α
a✝ : boundLeft a KVChain.nil
hab : r a a✝¹
⊢ boundLeft a (insertWith f KVChain.nil a✝¹ b)
Tactic:
rw [insertWith_nil]
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a✝¹ : α
b : β a✝¹
a : α
a✝ : boundLeft a KVChain.nil
hab : r a a✝¹
⊢ boundLeft a
    { toList := [{ fst := a✝¹, snd := b }],
      ascend := (_ : List.Ascending (Sigma.relOnFst r) [{ fst := a✝¹, snd := b }]) }
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a✝¹ : α
b : β a✝¹
a : α
a✝ : boundLeft a KVChain.nil
hab : r a a✝¹
⊢ boundLeft a
    { toList := [{ fst := a✝¹, snd := b }],
      ascend := (_ : List.Ascending (Sigma.relOnFst r) [{ fst := a✝¹, snd := b }]) }
Tactic:
exact hab
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs => ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)) xs →
      (fun xs => ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)) (KVChain.cons a_1 b_1 xs haxs)
Tactic:
intro a₁ b₁ xs ha₁xs _ d hdxs hda
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ boundLeft d (insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b)
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ boundLeft d (insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b)
Tactic:
unfold insertWith
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ boundLeft d
    (match insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro with
    | { val := z, property := hz } => hinge z.fst z.snd hz)
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ boundLeft d
    (match insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro with
    | { val := z, property := hz } => hinge z.fst z.snd hz)
Tactic:
dsimp [boundLeft]
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.fst.toList
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.snd.toList)
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.fst.toList
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.snd.toList)
Tactic:
apply List.predHead_of_forAll
Proof state after:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst)
    (List.reverseAux
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.fst.toList
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.snd.toList)
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst)
    (List.reverseAux
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.fst.toList
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.snd.toList)
Tactic:
rw [List.forAll_reverseAux]
Proof state after:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst)
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.fst.toList ∧
    List.forAll (r d ∘ Sigma.fst)
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.snd.toList
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst)
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.fst.toList ∧
    List.forAll (r d ∘ Sigma.fst)
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a b True.intro).val.snd.toList
Tactic:
apply forAll_fst_insertWithAux
Proof state after:
case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst) KVChain.nil.toList

case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst) (KVChain.cons a₁ b₁ xs ha₁xs).toList

case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ r d a
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst) KVChain.nil.toList

case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst) (KVChain.cons a₁ b₁ xs ha₁xs).toList

case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ r d a
Tactic:
. exact True.intro
Proof state after:
case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst) (KVChain.cons a₁ b₁ xs ha₁xs).toList

case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ r d a
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst) (KVChain.cons a₁ b₁ xs ha₁xs).toList

case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ r d a
Tactic:
. apply (xs.cons a₁ b₁ ha₁xs).ascend.forAll_of_predHead
  . exact λ _ _ h₁ h₂ => trans (t:=r) h₁ h₂
  . exact hdxs
Proof state after:
case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ r d a
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ r d a
Tactic:
. exact hda
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst) KVChain.nil.toList
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof state before:
case a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.forAll (r d ∘ Sigma.fst) (KVChain.cons a₁ b₁ xs ha₁xs).toList
Tactic:
apply (xs.cons a₁ b₁ ha₁xs).ascend.forAll_of_predHead
Proof state after:
case a.a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ ∀ (a b : Sigma β), (r d ∘ Sigma.fst) a → Sigma.relOnFst r a b → (r d ∘ Sigma.fst) b

case a.a.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ : ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)
d : α
hdxs : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
hda : r d a
⊢ List.predHead (r d ∘ Sigma.fst) (KVChain.cons a₁ b₁ xs ha₁xs).toList