case intro
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
b' : β { fst := a, snd := b }.fst
h' : dlookup { fst := a, snd := b }.fst l = some b'
⊢ b ∈ dlookup a l
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
⊢ b ∈ dlookup a l
cases' Option.isSome_iff_exists.mp (dlookup_isSome.mpr (mem_keys_of_mem h)) with b' h'
case intro.refl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
h' : dlookup { fst := a, snd := b }.fst l = some b
⊢ b ∈ dlookup a l
case intro
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
b' : β { fst := a, snd := b }.fst
h' : dlookup { fst := a, snd := b }.fst l = some b'
⊢ b ∈ dlookup a l
cases nd.eq_of_mk_mem h (of_mem_dlookup h')
no goals
case intro.refl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
h' : dlookup { fst := a, snd := b }.fst l = some b
⊢ b ∈ dlookup a l
exact h'