no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
⊢ map (Sigma.mk a) (lookupAll a []) <+ []
simp
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ map (Sigma.mk a) (lookupAll a ({ fst := a', snd := b' } :: l)) <+ { 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'
⊢ map (Sigma.mk a) (lookupAll a ({ fst := a', snd := b' } :: l)) <+ { fst := a', snd := b' } :: l
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ map (Sigma.mk a) (lookupAll a ({ fst := a', snd := b' } :: l)) <+ { 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
⊢ map (Sigma.mk a) (lookupAll a ({ fst := a, snd := b' } :: l)) <+ { 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'
⊢ map (Sigma.mk a) (lookupAll a ({ fst := a', snd := b' } :: l)) <+ { fst := a', snd := b' } :: l
subst h
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ { fst := a, snd := b' } :: map (Sigma.mk a) (lookupAll a l) <+ { fst := a, snd := b' } :: l
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ map (Sigma.mk a) (lookupAll a ({ fst := a, snd := b' } :: l)) <+ { fst := a, snd := b' } :: l
simp only [ne_eq, not_true, lookupAll_cons_eq, List.map]
no goals
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ { fst := a, snd := b' } :: map (Sigma.mk a) (lookupAll a l) <+ { fst := a, snd := b' } :: l
exact (lookupAll_sublist a l).cons₂ _
case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a l) <+ { 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'
⊢ map (Sigma.mk a) (lookupAll a ({ fst := a', snd := b' } :: l)) <+ { fst := a', snd := b' } :: l
simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]
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'
⊢ map (Sigma.mk a) (lookupAll a l) <+ { fst := a', snd := b' } :: l
exact (lookupAll_sublist a l).cons _