α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
this : Nodup (map Sigma.fst (map (Sigma.mk a) (lookupAll a l)))
⊢ length (lookupAll a l) ≤ 1
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
⊢ length (lookupAll a l) ≤ 1
have := Nodup.sublist ((lookupAll_sublist a l).map _) h
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
this : Nodup (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l))
⊢ length (lookupAll a l) ≤ 1
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
this : Nodup (map Sigma.fst (map (Sigma.mk a) (lookupAll a l)))
⊢ length (lookupAll a l) ≤ 1
rw [map_map] at this
no goals
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
this : Nodup (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l))
⊢ length (lookupAll a l) ≤ 1
rwa [← nodup_replicate, ← map_const]