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

State before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))
Tactic:
have hterm : length (matchKey xs k).snd < Nat.succ (length xs) :=
  Nat.lt_of_succ_le $ Nat.succ_le_succ $ matchKey_snd_length xs k
State after:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))

State before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))
Tactic:
have ih := length_groupByKey (matchKey xs k).2
State after:
κ : 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 ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))

State before:
κ : 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 ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))
Tactic:
simp only [map, unique, uniqueAux, List.not_mem_nil, ite_false, groupByKey]
State after:
κ : 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 ((k, v :: (matchKey xs k).fst) :: groupByKey (matchKey xs k).snd) = length (uniqueAux (map Prod.fst xs) [k])

State before:
κ : 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 ((k, v :: (matchKey xs k).fst) :: groupByKey (matchKey xs k).snd) = length (uniqueAux (map Prod.fst xs) [k])
Tactic:
simp only [length]
State after:
κ : 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 xs) [k])

State before:
κ : 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 xs) [k])
Tactic:
rw [length_uniqueAux_matchKey _ k _ $ List.Mem.head _]
State after:
κ : 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])

State before:
κ : 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])
Tactic:
rw [ih]
State after:
κ : 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])

State before:
κ : 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])
Tactic:
apply Eq.symm
State after:
case h
κ : 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 (uniqueAux (map Prod.fst (matchKey xs k).snd) [k]) = length (unique (map Prod.fst (matchKey xs k).snd)) + 1

State before:
case h
κ : 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 (uniqueAux (map Prod.fst (matchKey xs k).snd) [k]) = length (unique (map Prod.fst (matchKey xs k).snd)) + 1
Tactic:
apply List.length_uniqueAux (acc := [k])
State after:
case h.h
κ : 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))
⊢ ∀ (x : κ), x ∈ map Prod.fst (matchKey xs k).snd → ¬x ∈ [k]

State before:
case h.h
κ : 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))
⊢ ∀ (x : κ), x ∈ map Prod.fst (matchKey xs k).snd → ¬x ∈ [k]
Tactic:
intro x
State after:
case h.h
κ : 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))
x : κ
⊢ x ∈ map Prod.fst (matchKey xs k).snd → ¬x ∈ [k]

State before:
case h.h
κ : 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))
x : κ
⊢ x ∈ map Prod.fst (matchKey xs k).snd → ¬x ∈ [k]
Tactic:
rw [mem_singleton_iff]
State after:
case h.h
κ : 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))
x : κ
⊢ x ∈ map Prod.fst (matchKey xs k).snd → ¬x = k

State before:
case h.h
κ : 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))
x : κ
⊢ x ∈ map Prod.fst (matchKey xs k).snd → ¬x = k
Tactic:
intro hmem hneg
State after:
case h.h
κ : 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))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs k).snd
hneg : x = k
⊢ False

State before:
case h.h
κ : 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))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs k).snd
hneg : x = k
⊢ False
Tactic:
have := not_mem_matchKey_self_map_snd x xs
State after:
case h.h
κ : 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))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs k).snd
hneg : x = k
this : ¬x ∈ map Prod.fst (matchKey xs x).snd
⊢ False

State before:
case h.h
κ : 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))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs k).snd
hneg : x = k
this : ¬x ∈ map Prod.fst (matchKey xs x).snd
⊢ False
Tactic:
rw [←hneg] at hmem
State after:
case h.h
κ : 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))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs x).snd
hneg : x = k
this : ¬x ∈ map Prod.fst (matchKey xs x).snd
⊢ False

State before:
case h.h
κ : 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))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs x).snd
hneg : x = k
this : ¬x ∈ map Prod.fst (matchKey xs x).snd
⊢ False
Tactic:
exact this hmem
State after:
no goals

State before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
xs✝ : List (κ × ν)
a✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y xs✝ →
      length (groupByKey y) = length (unique (map Prod.fst y))
k : κ
v : ν
xs : List (κ × ν)
x✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y ((k, v) :: xs) →
      length (groupByKey y) = length (unique (map Prod.fst y))
hterm : 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