Theorem: KVChain.boundLeft_insertWith_of_boundLeft (Algdata/Data/KVChain/MergeWith.lean)

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)
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)

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
State after:
no goals

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
State after:
no goals

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
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)

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]
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 }]) }

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
State after:
no goals

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
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)

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
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)

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]
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)

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
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)

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]
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

State before:
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
Tactic:
. exact λ _ _ h₁ h₂ => trans (t:=r) h₁ h₂
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
⊢ List.predHead (r d ∘ Sigma.fst) (KVChain.cons a₁ b₁ xs ha₁xs).toList

State before:
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
Tactic:
. exact hdxs
State after:
no goals

State before:
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
Tactic:
exact λ _ _ h₁ h₂ => trans (t:=r) h₁ h₂
State after:
no goals

State before:
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
Tactic:
exact hdxs
State after:
no goals

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
State after:
no goals