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