Theorem: KVChain.insertWith_cons_of_flip (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
⊢ ∀ (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₁
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₁

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

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

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