Theorem: KVChain.insertWith_cons_of_rel (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)
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
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))

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

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

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

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

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

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

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

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

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