cases Decidable.em (k' = k) with
| inl hkeq =>
  simp only [hkeq, ite_true]
  have : x ∈ map Prod.fst ys := by
    cases hx with
    | head => contradiction
    | tail => assumption
  have ih := mem_fst_matchKey_key_or_snd this k
  cases ih with
  | inl => contradiction
  | inr hmem => exact hmem
| inr hkneq =>
  simp only [hkneq, ite_false]
  simp only [map]
  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_matchKey_key_or_snd this k'
    cases ih with
    | inl => contradiction
    | inr => assumption
κ : 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)
⊢ x ∈
    map Prod.fst
      (if k' = k then (v :: (matchKey ys k).fst, (matchKey ys k).snd)
        else ((matchKey ys k).fst, (k', v) :: (matchKey ys k).snd)).snd
no goals