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

State before:
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
⊢ k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
Tactic:
intro h
State after:
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
h : k ∈ map Prod.fst (groupByKey kvs)
⊢ k ∈ map Prod.fst kvs

State before:
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
h : k ∈ map Prod.fst (groupByKey kvs)
⊢ k ∈ map Prod.fst kvs
Tactic:
induction kvs with
| nil => contradiction
| cons kv kvs ih =>
  cases kv with | mk k₀ v₀ =>
  simp only [groupByKey] at h
  simp only [map] at h
  simp only [map]
  cases h with
  | head => apply Mem.head
  | tail _ htail =>
    apply Mem.tail
    apply ih
    apply all_in_map_fst_groupByKey_of_sublist (matchKey_snd_sublist k₀ kvs)
    assumption
State after:
no goals

State before:
case nil
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
h : k ∈ map Prod.fst (groupByKey [])
⊢ k ∈ map Prod.fst []
Tactic:
contradiction
State after:
no goals

State before:
case cons
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
h : k ∈ map Prod.fst (groupByKey (kv :: kvs))
⊢ k ∈ map Prod.fst (kv :: kvs)
Tactic:
cases kv with | mk k₀ v₀ =>
simp only [groupByKey] at h
simp only [map] at h
simp only [map]
cases h with
| head => apply Mem.head
| tail _ htail =>
  apply Mem.tail
  apply ih
  apply all_in_map_fst_groupByKey_of_sublist (matchKey_snd_sublist k₀ kvs)
  assumption
State after:
no goals

State before:
case cons.mk
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
h : k ∈ map Prod.fst (groupByKey ((k₀, v₀) :: kvs))
⊢ k ∈ map Prod.fst ((k₀, v₀) :: kvs)
Tactic:
simp only [groupByKey] at h
State after:
case cons.mk
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
h : k ∈ map Prod.fst ((k₀, v₀ :: (matchKey kvs k₀).fst) :: groupByKey (matchKey kvs k₀).snd)
⊢ k ∈ map Prod.fst ((k₀, v₀) :: kvs)

State before:
case cons.mk
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
h : k ∈ map Prod.fst ((k₀, v₀ :: (matchKey kvs k₀).fst) :: groupByKey (matchKey kvs k₀).snd)
⊢ k ∈ map Prod.fst ((k₀, v₀) :: kvs)
Tactic:
simp only [map] at h
State after:
case cons.mk
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
h : k ∈ k₀ :: map Prod.fst (groupByKey (matchKey kvs k₀).snd)
⊢ k ∈ map Prod.fst ((k₀, v₀) :: kvs)

State before:
case cons.mk
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
h : k ∈ k₀ :: map Prod.fst (groupByKey (matchKey kvs k₀).snd)
⊢ k ∈ map Prod.fst ((k₀, v₀) :: kvs)
Tactic:
simp only [map]
State after:
case cons.mk
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
h : k ∈ k₀ :: map Prod.fst (groupByKey (matchKey kvs k₀).snd)
⊢ k ∈ k₀ :: map Prod.fst kvs

State before:
case cons.mk
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
h : k ∈ k₀ :: map Prod.fst (groupByKey (matchKey kvs k₀).snd)
⊢ k ∈ k₀ :: map Prod.fst kvs
Tactic:
cases h with
| head => apply Mem.head
| tail _ htail =>
  apply Mem.tail
  apply ih
  apply all_in_map_fst_groupByKey_of_sublist (matchKey_snd_sublist k₀ kvs)
  assumption
State after:
no goals

State before:
case cons.mk.head
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
v₀ : ν
⊢ k ∈ k :: map Prod.fst kvs
Tactic:
apply Mem.head
State after:
no goals

State before:
case cons.mk.tail
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
htail : Mem k (map Prod.fst (groupByKey (matchKey kvs k₀).snd))
⊢ k ∈ k₀ :: map Prod.fst kvs
Tactic:
apply Mem.tail
State after:
case cons.mk.tail.a
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
htail : Mem k (map Prod.fst (groupByKey (matchKey kvs k₀).snd))
⊢ Mem k (map Prod.fst kvs)

State before:
case cons.mk.tail.a
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
htail : Mem k (map Prod.fst (groupByKey (matchKey kvs k₀).snd))
⊢ Mem k (map Prod.fst kvs)
Tactic:
apply ih
State after:
case cons.mk.tail.a
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
htail : Mem k (map Prod.fst (groupByKey (matchKey kvs k₀).snd))
⊢ k ∈ map Prod.fst (groupByKey kvs)

State before:
case cons.mk.tail.a
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
htail : Mem k (map Prod.fst (groupByKey (matchKey kvs k₀).snd))
⊢ k ∈ map Prod.fst (groupByKey kvs)
Tactic:
apply all_in_map_fst_groupByKey_of_sublist (matchKey_snd_sublist k₀ kvs)
State after:
case cons.mk.tail.a.a
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
htail : Mem k (map Prod.fst (groupByKey (matchKey kvs k₀).snd))
⊢ k ∈ map Prod.fst (groupByKey (matchKey kvs k₀).snd)

State before:
case cons.mk.tail.a.a
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
htail : Mem k (map Prod.fst (groupByKey (matchKey kvs k₀).snd))
⊢ k ∈ map Prod.fst (groupByKey (matchKey kvs k₀).snd)
Tactic:
assumption
State after:
no goals