case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ Option.map (Sigma.mk a) (dlookup a ({ fst := a', snd := b' } :: l)) =
    find? (fun s => decide (a = s.fst)) ({ fst := a', snd := b' } :: l)

case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ Option.map (Sigma.mk a) (dlookup a ({ fst := a', snd := b' } :: l)) =
    find? (fun s => decide (a = s.fst)) ({ fst := a', snd := b' } :: l)
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ Option.map (Sigma.mk a) (dlookup a ({ fst := a', snd := b' } :: l)) =
    find? (fun s => decide (a = s.fst)) ({ fst := a', snd := b' } :: l)
by_cases h : a = a'
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ Option.map (Sigma.mk a) (dlookup a ({ fst := a, snd := b' } :: l)) =
    find? (fun s => decide (a = s.fst)) ({ fst := a, snd := b' } :: l)
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ Option.map (Sigma.mk a) (dlookup a ({ fst := a', snd := b' } :: l)) =
    find? (fun s => decide (a = s.fst)) ({ fst := a', snd := b' } :: l)
subst a'
no goals
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ Option.map (Sigma.mk a) (dlookup a ({ fst := a, snd := b' } :: l)) =
    find? (fun s => decide (a = s.fst)) ({ fst := a, snd := b' } :: l)
simp
case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ Option.map (Sigma.mk a) (dlookup a l) = find? (fun s => decide (a = s.fst)) l
case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ Option.map (Sigma.mk a) (dlookup a ({ fst := a', snd := b' } :: l)) =
    find? (fun s => decide (a = s.fst)) ({ fst := a', snd := b' } :: l)
simp [h]
no goals
case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ Option.map (Sigma.mk a) (dlookup a l) = find? (fun s => decide (a = s.fst)) l
exact map_dlookup_eq_find a l