cases kv with | mk k₀ v₀ =>
simp only [groupByKey] at h
simp only [map] at h
simp only [map]
cases h with
| head => apply Mem.head
| tail _ htail =>
  apply Mem.tail
  apply ih
  apply all_in_map_fst_groupByKey_of_sublist (matchKey_snd_sublist k₀ kvs)
  assumption
case cons
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
h : k ∈ map Prod.fst (groupByKey (kv :: kvs))
⊢ k ∈ map Prod.fst (kv :: kvs)
no goals