induction kvs with
| nil => contradiction
| cons kv kvs ih =>
  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
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
h : k ∈ map Prod.fst (groupByKey kvs)
⊢ k ∈ map Prod.fst kvs
no goals