Theorem: List.groupByKey_matchKey_snd_length_cons (Table/BuiltinExtensions.lean)

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
v : ν
xs : List (κ × ν)
⊢ 1 + length (groupByKey (matchKey ((k, v) :: xs) k).snd) = 1 + length (groupByKey (matchKey xs k).snd)
Tactic:
simp only [matchKey, length, ite_true]
State after:
no goals