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

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
⊢ (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
Tactic:
rw [insertWithAux_cons_rfl]
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
      Option.casesOn (f a b₁ b)
        { val := (KVChain.nil, xs), property := (_ : hingeable (KVChain.nil, xs).fst (KVChain.nil, xs).snd) } fun bf =>
        { val := (KVChain.cons a bf KVChain.nil True.intro, xs),
          property :=
            (_ :
              hingeable (KVChain.cons a bf KVChain.nil True.intro)
                (KVChain.cons a bf KVChain.nil True.intro, xs).snd) } 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

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
⊢ (match
      Option.casesOn (f a b₁ b)
        { val := (KVChain.nil, xs), property := (_ : hingeable (KVChain.nil, xs).fst (KVChain.nil, xs).snd) } fun bf =>
        { val := (KVChain.cons a bf KVChain.nil True.intro, xs),
          property :=
            (_ :
              hingeable (KVChain.cons a bf KVChain.nil True.intro)
                (KVChain.cons a bf KVChain.nil True.intro, xs).snd) } 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
Tactic:
cases f a b₁ b <;> rfl
State after:
no goals