simp [htrue, ite_true, filter, ih, map]
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
htrue : x.fst = k
⊢ (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
      else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).fst =
    map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
no goals