simp only [matchKey]
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
⊢ length (matchKey (x :: xs) k).fst + length (matchKey (x :: xs) k).snd = length (x :: xs)
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
⊢ length
        (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 +
      length
        (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)).snd =
    length (x :: xs)