cases Decidable.em (x.fst ∈ acc) with
| inl hin =>
  simp only [hin, ite_true, matchKey]
  rw [ih _ hk]
  cases Decidable.em (x.1 = k) with
  | inl heq => simp only [heq, ite_true]
  | inr hneq => simp only [hneq, ite_false, map, uniqueAux, hin, ite_true]
| inr hout =>
  simp only [hout, ite_false, matchKey]
  cases Decidable.em (x.1 = k) with
  | inl heq =>
    apply absurd hk
    rw [heq] at hout
    exact hout
  | inr hneq =>
    rw [ih _ (List.Mem.tail _ hk)]
    simp only [hneq, ite_false, uniqueAux, hout]
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
⊢ length (if x.fst ∈ acc then uniqueAux (map Prod.fst xs) acc else uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)
no goals