α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some ((_ : { fst := a', snd := b }.fst = a) ▸ b), l)
    else ((kextract a l).fst, { fst := a', snd := b } :: (kextract a l).snd)) =
    (dlookup a ({ fst := a', snd := b } :: l), kerase a ({ fst := a', snd := b } :: l))
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ kextract a ({ fst := a', snd := b } :: l) =
    (dlookup a ({ fst := a', snd := b } :: l), kerase a ({ fst := a', snd := b } :: l))
simp [kextract]
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some ((_ : a' = a) ▸ b), l)
    else ((kextract a l).fst, { fst := a', snd := b } :: (kextract a l).snd)) =
    (dlookup a ({ fst := a', snd := b } :: l), kerase a ({ fst := a', snd := b } :: l))
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some ((_ : { fst := a', snd := b }.fst = a) ▸ b), l)
    else ((kextract a l).fst, { fst := a', snd := b } :: (kextract a l).snd)) =
    (dlookup a ({ fst := a', snd := b } :: l), kerase a ({ fst := a', snd := b } :: l))
dsimp
case inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a' = a
⊢ (some ((_ : a' = a) ▸ b), l) = (dlookup a ({ fst := a', snd := b } :: l), kerase a ({ fst := a', snd := b } :: l))

case inr
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a' = a
⊢ ((kextract a l).fst, { fst := a', snd := b } :: (kextract a l).snd) =
    (dlookup a ({ fst := a', snd := b } :: l), kerase a ({ fst := a', snd := b } :: l))
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some ((_ : a' = a) ▸ b), l)
    else ((kextract a l).fst, { fst := a', snd := b } :: (kextract a l).snd)) =
    (dlookup a ({ fst := a', snd := b } :: l), kerase a ({ fst := a', snd := b } :: l))
split_ifs with h
case inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (some ((_ : a = a) ▸ b), l) = (dlookup a ({ fst := a, snd := b } :: l), kerase a ({ fst := a, snd := b } :: l))
case inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a' = a
⊢ (some ((_ : a' = a) ▸ b), l) = (dlookup a ({ fst := a', snd := b } :: l), kerase a ({ fst := a', snd := b } :: l))
subst a'
no goals
case inl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (some ((_ : a = a) ▸ b), l) = (dlookup a ({ fst := a, snd := b } :: l), kerase a ({ fst := a, snd := b } :: l))
simp [kerase]
no goals
case inr
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a' = a
⊢ ((kextract a l).fst, { fst := a', snd := b } :: (kextract a l).snd) =
    (dlookup a ({ fst := a', snd := b } :: l), kerase a ({ fst := a', snd := b } :: l))
simp [kextract, Ne.symm h, kextract_eq_dlookup_kerase a l, kerase]