cases Decidable.em (x = k') with
| inl hxeq => rw [hxeq]; apply Mem.head
| inr hxneq =>
  apply Mem.tail
  have : x ∈ map Prod.fst (matchKey ys k).snd := by
    cases hx with
    | head => contradiction
    | tail _ htail =>
      have := mem_fst_matchKey_key_or_snd htail k
      cases this with
      | inl => contradiction
      | inr => assumption
  have ih := mem_fst_groupByKey_key_or_snd this k'
  cases ih with
  | inl => contradiction
  | inr => assumption
case inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
x k : κ
h : ¬x = k
k' : κ
v : ν
ys : List (κ × ν)
hx : x ∈ map Prod.fst ((k', v) :: ys)
h_term : length (matchKey ys k).snd < Nat.succ (length ys)
h_term' : length ys < Nat.succ (length ys)
hkneq : ¬k' = k
⊢ x ∈ k' :: map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd)
no goals