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

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
kvs : List (κ × ν)
a✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y kvs → NoDuplicates (map Prod.fst (groupByKey y))
k : κ
v : ν
xs : List (κ × ν)
x✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y ((k, v) :: xs) →
      NoDuplicates (map Prod.fst (groupByKey y))
h_help : length (matchKey xs k).snd < Nat.succ (length xs)
⊢ (invImage (fun a => length a) instWellFoundedRelation).1 (matchKey xs k).snd ((k, v) :: xs)
Tactic:
assumption
State after:
no goals