case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a ({ fst := a', snd := b' } :: l)
h : a = a'
⊢ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l

case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a ({ fst := a', snd := b' } :: l)
h : ¬a = a'
⊢ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a ({ fst := a', snd := b' } :: l)
⊢ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
by_cases h : a = a'
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b ∈ dlookup a ({ fst := a, snd := b' } :: l)
⊢ { fst := a, snd := b } ∈ { fst := a, snd := b' } :: l
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a ({ fst := a', snd := b' } :: l)
h : a = a'
⊢ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
subst a'
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b' = b
⊢ { fst := a, snd := b } ∈ { fst := a, snd := b' } :: l
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b ∈ dlookup a ({ fst := a, snd := b' } :: l)
⊢ { fst := a, snd := b } ∈ { fst := a, snd := b' } :: l
simp at H
no goals
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b' = b
⊢ { fst := a, snd := b } ∈ { fst := a, snd := b' } :: l
simp [H]
case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
H : b ∈ dlookup a l
⊢ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a ({ fst := a', snd := b' } :: l)
h : ¬a = a'
⊢ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
simp only [ne_eq, h, not_false_iff, dlookup_cons_ne] at H
no goals
case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
H : b ∈ dlookup a l
⊢ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
simp [of_mem_dlookup H]