no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
⊢ b ∈ lookupAll a [] ↔ { fst := a, snd := b } ∈ []
simp
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ b ∈ lookupAll a ({ fst := a', snd := b' } :: 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 : ¬a = a'
⊢ b ∈ lookupAll a ({ fst := a', snd := b' } :: l) ↔ { 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 β)
⊢ b ∈ lookupAll a ({ fst := a', snd := b' } :: l) ↔ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
by_cases h : a = a'
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'
⊢ b ∈ lookupAll a ({ fst := a', snd := b' } :: l) ↔ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
. simp [*, mem_lookupAll]
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
⊢ b ∈ lookupAll 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 : a = a'
⊢ b ∈ lookupAll a ({ fst := a', snd := b' } :: l) ↔ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
subst h
no goals
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
⊢ b ∈ lookupAll a ({ fst := a, snd := b' } :: l) ↔ { fst := a, snd := b } ∈ { fst := a, snd := b' } :: l
simp [*, mem_lookupAll]
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'
⊢ b ∈ lookupAll a ({ fst := a', snd := b' } :: l) ↔ { fst := a, snd := b } ∈ { fst := a', snd := b' } :: l
simp [*, mem_lookupAll]