internlm/Lean-Github huggingface dataset:
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof 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₂
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
⊢ List.predHead (r d ∘ Sigma.fst) (KVChain.cons a₁ b₁ xs ha₁xs).toList
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof 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
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof 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₂
Proof state after:
no goals
Theorem: KVChain.boundLeft_insertWith_of_boundLeft
Proof 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
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
⊢ r d a
Tactic:
exact hda
Proof state after:
no goals
Theorem: KVChain.insertWith_cons_of_rel
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
⊢ ∀ (ha₁a : r a₁ a),
    insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b =
      KVChain.cons a₁ b₁ (insertWith f xs a b) (_ : boundLeft a₁ (insertWith f xs a b))
Tactic:
intro ha₁a
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
ha₁a : r a₁ a
⊢ insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b =
    KVChain.cons a₁ b₁ (insertWith f xs a b) (_ : boundLeft a₁ (insertWith f xs a b))
Theorem: KVChain.insertWith_cons_of_rel
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
ha₁a : r a₁ a
⊢ insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b =
    KVChain.cons a₁ b₁ (insertWith f xs a b) (_ : boundLeft a₁ (insertWith f xs a b))
Tactic:
cases xs
Proof state after:
case mk
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ insertWith f (KVChain.cons a₁ b₁ { toList := toList✝, ascend := ascend✝ } ha₁xs) a b =
    KVChain.cons a₁ b₁ (insertWith f { toList := toList✝, ascend := ascend✝ } a b)
      (_ : boundLeft a₁ (insertWith f { toList := toList✝, ascend := ascend✝ } a b))
Theorem: KVChain.insertWith_cons_of_rel
Proof state before:
case mk
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ insertWith f (KVChain.cons a₁ b₁ { toList := toList✝, ascend := ascend✝ } ha₁xs) a b =
    KVChain.cons a₁ b₁ (insertWith f { toList := toList✝, ascend := ascend✝ } a b)
      (_ : boundLeft a₁ (insertWith f { toList := toList✝, ascend := ascend✝ } a b))
Tactic:
conv => lhs; dsimp [insertWith]; rw [insertWithAux_cons_rel ha₁a]
Proof state after:
case mk
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ hinge
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
            { toList := toList✝, ascend := ascend✝ }
            (_ :
              hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                { toList := toList✝, ascend := ascend✝ })
            a b ha₁a).val.fst
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
            { toList := toList✝, ascend := ascend✝ }
            (_ :
              hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                { toList := toList✝, ascend := ascend✝ })
            a b ha₁a).val.snd
      (_ :
        hingeable
          (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                { toList := toList✝, ascend := ascend✝ }
                (_ :
                  hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                    { toList := toList✝, ascend := ascend✝ })
                a b ha₁a).val.fst
          (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                { toList := toList✝, ascend := ascend✝ }
                (_ :
                  hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                    { toList := toList✝, ascend := ascend✝ })
                a b ha₁a).val.snd) =
    KVChain.cons a₁ b₁ (insertWith f { toList := toList✝, ascend := ascend✝ } a b)
      (_ : boundLeft a₁ (insertWith f { toList := toList✝, ascend := ascend✝ } a b))
Theorem: KVChain.insertWith_cons_of_rel
Proof state before:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ (hinge
        (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
              { toList := toList✝, ascend := ascend✝ }
              (_ :
                hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                  { toList := toList✝, ascend := ascend✝ })
              a b ha₁a).val.fst
        (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
              { toList := toList✝, ascend := ascend✝ }
              (_ :
                hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                  { toList := toList✝, ascend := ascend✝ })
              a b ha₁a).val.snd
        (_ :
          hingeable
            (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                  { toList := toList✝, ascend := ascend✝ }
                  (_ :
                    hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                      { toList := toList✝, ascend := ascend✝ })
                  a b ha₁a).val.fst
            (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                  { toList := toList✝, ascend := ascend✝ }
                  (_ :
                    hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil))
                      { toList := toList✝, ascend := ascend✝ })
                  a b ha₁a).val.snd)).toList =
    (KVChain.cons a₁ b₁ (insertWith f { toList := toList✝, ascend := ascend✝ } a b)
        (_ : boundLeft a₁ (insertWith f { toList := toList✝, ascend := ascend✝ } a b))).toList
Tactic:
dsimp
Proof state after:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverseAux
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }) a b
              ha₁a).val.fst.toList
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }) a b
              ha₁a).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Theorem: KVChain.insertWith_cons_of_rel
Proof state before:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverseAux
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }) a b
              ha₁a).val.fst.toList
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }) a b
              ha₁a).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Tactic:
rw [toList_fst_insertWithAux_eq_append]
Proof state after:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b
                True.intro).val.fst.toList ++
        (KVChain.cons a₁ b₁ KVChain.nil True.intro).toList)
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }) a b
              ha₁a).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Theorem: KVChain.insertWith_cons_of_rel
Proof state before:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b
                True.intro).val.fst.toList ++
        (KVChain.cons a₁ b₁ KVChain.nil True.intro).toList)
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil True.intro) { toList := toList✝, ascend := ascend✝ }) a b
              ha₁a).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Tactic:
rw [toList_snd_insertWithAux_inv]
Proof state after:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b
                True.intro).val.fst.toList ++
        (KVChain.cons a₁ b₁ KVChain.nil True.intro).toList)
      (insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b True.intro).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Theorem: KVChain.insertWith_cons_of_rel
Proof state before:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b
                True.intro).val.fst.toList ++
        (KVChain.cons a₁ b₁ KVChain.nil True.intro).toList)
      (insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b True.intro).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Tactic:
dsimp
Proof state after:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b
                True.intro).val.fst.toList ++
        [{ fst := a₁, snd := b₁ }])
      (insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b True.intro).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Theorem: KVChain.insertWith_cons_of_rel
Proof state before:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b
                True.intro).val.fst.toList ++
        [{ fst := a₁, snd := b₁ }])
      (insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b True.intro).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Tactic:
rw [List.reverseAux_append_left]
Proof state after:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverse [{ fst := a₁, snd := b₁ }] ++
      List.reverseAux
        (insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b True.intro).val.fst.toList
        (insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b
                True.intro).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Theorem: KVChain.insertWith_cons_of_rel
Proof state before:
case mk.a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
a : α
b : β a
ha₁a : r a₁ a
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
ha₁xs : boundLeft a₁ { toList := toList✝, ascend := ascend✝ }
⊢ List.reverse [{ fst := a₁, snd := b₁ }] ++
      List.reverseAux
        (insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b True.intro).val.fst.toList
        (insertWithAux f KVChain.nil { toList := toList✝, ascend := ascend✝ } True.intro a b
                True.intro).val.snd.toList =
    { fst := a₁, snd := b₁ } :: (insertWith f { toList := toList✝, ascend := ascend✝ } a b).toList
Tactic:
rfl
Proof state after:
no goals
Theorem: KVChain.insertWith_cons_of_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
⊢ ∀ (haa₁ : r a a₁),
    insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b = KVChain.cons a b (KVChain.cons a₁ b₁ xs ha₁xs) haa₁
Tactic:
intro haa₁
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
haa₁ : r a a₁
⊢ insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b = KVChain.cons a b (KVChain.cons a₁ b₁ xs ha₁xs) haa₁
Theorem: KVChain.insertWith_cons_of_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
haa₁ : r a a₁
⊢ insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b = KVChain.cons a b (KVChain.cons a₁ b₁ xs ha₁xs) haa₁
Tactic:
unfold insertWith
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
haa₁ : r a a₁
⊢ (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) =
    KVChain.cons a b (KVChain.cons a₁ b₁ xs ha₁xs) haa₁
Theorem: KVChain.insertWith_cons_of_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
haa₁ : r a a₁
⊢ (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) =
    KVChain.cons a b (KVChain.cons a₁ b₁ xs ha₁xs) haa₁
Tactic:
rw [insertWithAux_cons_flip haa₁]
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
haa₁ : r a a₁
⊢ (match { val := (KVChain.cons a b KVChain.nil True.intro, KVChain.cons a₁ b₁ xs ha₁xs), property := haa₁ } with
    | { val := z, property := hz } => hinge z.fst z.snd hz) =
    KVChain.cons a b (KVChain.cons a₁ b₁ xs ha₁xs) haa₁
Theorem: KVChain.insertWith_cons_of_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
haa₁ : r a a₁
⊢ (match { val := (KVChain.cons a b KVChain.nil True.intro, KVChain.cons a₁ b₁ xs ha₁xs), property := haa₁ } with
    | { val := z, property := hz } => hinge z.fst z.snd hz) =
    KVChain.cons a b (KVChain.cons a₁ b₁ xs ha₁xs) haa₁
Tactic:
rfl
Proof state after:
no goals
Theorem: KVChain.insertWith_cons_of_eq
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
haxs : boundLeft a xs
b : β a
⊢ insertWith f (KVChain.cons a b₁ xs haxs) a b = Option.casesOn (f a b₁ b) xs fun bf => KVChain.cons a bf xs haxs
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
haxs : boundLeft a xs
b : β a
⊢ (match insertWithAux f KVChain.nil (KVChain.cons a b₁ xs haxs) True.intro a b True.intro with
    | { val := z, property := hz } => hinge z.fst z.snd hz) =
    Option.casesOn (f a b₁ b) xs fun bf => KVChain.cons a bf xs haxs