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✝ }
⊢ 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))
Tactic:
apply KVChain.eq_of_toList_eq
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✝ }
⊢ (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