rw [ih]
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (groupByKey (matchKey xs k).snd) + 1 = length (uniqueAux (map Prod.fst (matchKey xs k).snd) [k])
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (unique (map Prod.fst (matchKey xs k).snd)) + 1 = length (uniqueAux (map Prod.fst (matchKey xs k).snd) [k])