internlm/Lean-Github huggingface dataset:
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case tail
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
x k : κ
h : ¬x = k
k' : κ
v : ν
ys : List (κ × ν)
h_term : length (matchKey ys k).snd < Nat.succ (length ys)
h_term' : length ys < Nat.succ (length ys)
hkneq : ¬k' = k
hxneq : ¬x = k'
htail : Mem x (map Prod.fst ys)
this : x = k ∨ x ∈ map Prod.fst (matchKey ys k).snd
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Tactic:
cases this with
| inl => contradiction
| inr => assumption
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case tail.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
x k : κ
h : ¬x = k
k' : κ
v : ν
ys : List (κ × ν)
h_term : length (matchKey ys k).snd < Nat.succ (length ys)
h_term' : length ys < Nat.succ (length ys)
hkneq : ¬k' = k
hxneq : ¬x = k'
htail : Mem x (map Prod.fst ys)
h✝ : x = k
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case tail.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
x k : κ
h : ¬x = k
k' : κ
v : ν
ys : List (κ × ν)
h_term : length (matchKey ys k).snd < Nat.succ (length ys)
h_term' : length ys < Nat.succ (length ys)
hkneq : ¬k' = k
hxneq : ¬x = k'
htail : Mem x (map Prod.fst ys)
h✝ : x ∈ map Prod.fst (matchKey ys k).snd
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inr.inr.a.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
x k : κ
h : ¬x = k
k' : κ
v : ν
ys : List (κ × ν)
hx : x ∈ map Prod.fst ((k', v) :: ys)
h_term : length (matchKey ys k).snd < Nat.succ (length ys)
h_term' : length ys < Nat.succ (length ys)
hkneq : ¬k' = k
hxneq : ¬x = k'
this : x ∈ map Prod.fst (matchKey ys k).snd
h✝ : x = k'
⊢ Mem x (map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd))
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inr.inr.a.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
x k : κ
h : ¬x = k
k' : κ
v : ν
ys : List (κ × ν)
hx : x ∈ map Prod.fst ((k', v) :: ys)
h_term : length (matchKey ys k).snd < Nat.succ (length ys)
h_term' : length ys < Nat.succ (length ys)
hkneq : ¬k' = k
hxneq : ¬x = k'
this : x ∈ map Prod.fst (matchKey ys k).snd
h✝ : x ∈ map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd)
⊢ Mem x (map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd))
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
_x✝ : (ys : List (κ × ν)) ×' (x : κ) ×' (_ : x ∈ map Prod.fst ys) ×' κ
a✝³ :
  ∀ (y : (ys : List (κ × ν)) ×' (x : κ) ×' (_ : x ∈ map Prod.fst ys) ×' κ),
    (invImage
            (fun a =>
              PSigma.casesOn a fun ys snd => PSigma.casesOn snd fun x snd => PSigma.casesOn snd fun hx snd => length ys)
            instWellFoundedRelation).1
        y _x✝ →
      y.2.1 = y.2.2.2 ∨ y.2.1 ∈ map Prod.fst (groupByKey (matchKey y.1 y.2.2.2).snd)
ys✝ : List (κ × ν)
x✝¹ : (x : κ) ×' (_ : x ∈ map Prod.fst ys✝) ×' κ
a✝² :
  ∀ (y : (ys : List (κ × ν)) ×' (x : κ) ×' (_ : x ∈ map Prod.fst ys) ×' κ),
    (invImage
            (fun a =>
              PSigma.casesOn a fun ys snd => PSigma.casesOn snd fun x snd => PSigma.casesOn snd fun hx snd => length ys)
            instWellFoundedRelation).1
        y { fst := ys✝, snd := x✝¹ } →
      y.2.1 = y.2.2.2 ∨ y.2.1 ∈ map Prod.fst (groupByKey (matchKey y.1 y.2.2.2).snd)
x : κ
hx✝¹ : (_ : x ∈ map Prod.fst ys✝) ×' κ
a✝¹ :
  ∀ (y : (ys : List (κ × ν)) ×' (x : κ) ×' (_ : x ∈ map Prod.fst ys) ×' κ),
    (invImage
            (fun a =>
              PSigma.casesOn a fun ys snd => PSigma.casesOn snd fun x snd => PSigma.casesOn snd fun hx snd => length ys)
            instWellFoundedRelation).1
        y { fst := ys✝, snd := { fst := x, snd := hx✝¹ } } →
      y.2.1 = y.2.2.2 ∨ y.2.1 ∈ map Prod.fst (groupByKey (matchKey y.1 y.2.2.2).snd)
hx✝ : x ∈ map Prod.fst ys✝
k : κ
a✝ :
  ∀ (y : (ys : List (κ × ν)) ×' (x : κ) ×' (_ : x ∈ map Prod.fst ys) ×' κ),
    (invImage
            (fun a =>
              PSigma.casesOn a fun ys snd => PSigma.casesOn snd fun x snd => PSigma.casesOn snd fun hx snd => length ys)
            instWellFoundedRelation).1
        y { fst := ys✝, snd := { fst := x, snd := { fst := hx✝, snd := k } } } →
      y.2.1 = y.2.2.2 ∨ y.2.1 ∈ map Prod.fst (groupByKey (matchKey y.1 y.2.2.2).snd)
h : ¬x = k
k' : κ
v : ν
ys : List (κ × ν)
hx : x ∈ map Prod.fst ((k', v) :: ys)
x✝ :
  ∀ (y : (ys : List (κ × ν)) ×' (x : κ) ×' (_ : x ∈ map Prod.fst ys) ×' κ),
    (invImage
            (fun a =>
              PSigma.casesOn a fun ys snd => PSigma.casesOn snd fun x snd => PSigma.casesOn snd fun hx snd => length ys)
            instWellFoundedRelation).1
        y { fst := (k', v) :: ys, snd := { fst := x, snd := { fst := hx, snd := k } } } →
      y.2.1 = y.2.2.2 ∨ y.2.1 ∈ map Prod.fst (groupByKey (matchKey y.1 y.2.2.2).snd)
h_term : length (matchKey ys k).snd < Nat.succ (length ys)
h_term' : length ys < Nat.succ (length ys)
hkneq : ¬k' = k
h✝¹ : (_ : k' = k ∨ ¬k' = k) = (_ : k' = k ∨ ¬k' = k)
hxneq : ¬x = k'
h✝ : (_ : x = k' ∨ ¬x = k') = (_ : x = k' ∨ ¬x = k')
this : x ∈ map Prod.fst (matchKey ys k).snd
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun ys snd => PSigma.casesOn snd fun x snd => PSigma.casesOn snd fun hx snd => length ys)
        instWellFoundedRelation).1
    { fst := (matchKey ys k).snd, snd := { fst := x, snd := { fst := this, snd := k' } } }
    { fst := (k', v) :: ys, snd := { fst := x, snd := { fst := hx, snd := k } } }
Tactic:
assumption
Proof state after:
no goals
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ map Prod.fst (groupByKey ((k, v) :: xs))
⊢ x ∈ map Prod.fst (groupByKey ((k, v) :: ys))
Tactic:
simp only [groupByKey]
Proof state after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ map Prod.fst (groupByKey ((k, v) :: xs))
⊢ x ∈ map Prod.fst ((k, v :: (matchKey ys k).fst) :: groupByKey (matchKey ys k).snd)
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ map Prod.fst (groupByKey ((k, v) :: xs))
⊢ x ∈ map Prod.fst ((k, v :: (matchKey ys k).fst) :: groupByKey (matchKey ys k).snd)
Tactic:
simp only [map]
Proof state after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ map Prod.fst (groupByKey ((k, v) :: xs))
⊢ x ∈ k :: map Prod.fst (groupByKey (matchKey ys k).snd)
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ map Prod.fst (groupByKey ((k, v) :: xs))
⊢ x ∈ k :: map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
simp only [groupByKey] at hx
Proof state after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ map Prod.fst ((k, v :: (matchKey xs k).fst) :: groupByKey (matchKey xs k).snd)
⊢ x ∈ k :: map Prod.fst (groupByKey (matchKey ys k).snd)
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ map Prod.fst ((k, v :: (matchKey xs k).fst) :: groupByKey (matchKey xs k).snd)
⊢ x ∈ k :: map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
simp only [map] at hx
Proof state after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ k :: map Prod.fst (groupByKey (matchKey xs k).snd)
⊢ x ∈ k :: map Prod.fst (groupByKey (matchKey ys k).snd)
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ k :: map Prod.fst (groupByKey (matchKey xs k).snd)
⊢ x ∈ k :: map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
cases hx with
| head => constructor
| tail _ htail =>
  apply Mem.tail
  have : (matchKey xs k).snd <+ (matchKey ys k).snd :=
    matchKey_snd_sublist_of_sublist _ _ _ hsubl
  have hterm := matchKey_length_lt k ys
  apply all_in_map_fst_groupByKey_of_sublist this
  assumption
Proof state after:
no goals
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
case head
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
⊢ k ∈ k :: map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
constructor
Proof state after:
no goals
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
case tail
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
⊢ x ∈ k :: map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
apply Mem.tail
Proof state after:
case tail.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
⊢ Mem x (map Prod.fst (groupByKey (matchKey ys k).snd))
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
case tail.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
⊢ Mem x (map Prod.fst (groupByKey (matchKey ys k).snd))
Tactic:
have : (matchKey xs k).snd <+ (matchKey ys k).snd :=
  matchKey_snd_sublist_of_sublist _ _ _ hsubl
Proof state after:
case tail.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
this : (matchKey xs k).snd <+ (matchKey ys k).snd
⊢ Mem x (map Prod.fst (groupByKey (matchKey ys k).snd))
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
case tail.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
this : (matchKey xs k).snd <+ (matchKey ys k).snd
⊢ Mem x (map Prod.fst (groupByKey (matchKey ys k).snd))
Tactic:
have hterm := matchKey_length_lt k ys
Proof state after:
case tail.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
this : (matchKey xs k).snd <+ (matchKey ys k).snd
hterm : length (matchKey ys k).snd < Nat.succ (length ys)
⊢ Mem x (map Prod.fst (groupByKey (matchKey ys k).snd))
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
case tail.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
this : (matchKey xs k).snd <+ (matchKey ys k).snd
hterm : length (matchKey ys k).snd < Nat.succ (length ys)
⊢ Mem x (map Prod.fst (groupByKey (matchKey ys k).snd))
Tactic:
apply all_in_map_fst_groupByKey_of_sublist this
Proof state after:
case tail.a.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
this : (matchKey xs k).snd <+ (matchKey ys k).snd
hterm : length (matchKey ys k).snd < Nat.succ (length ys)
⊢ x ∈ map Prod.fst (groupByKey (matchKey xs k).snd)
Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
case tail.a.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
this : (matchKey xs k).snd <+ (matchKey ys k).snd
hterm : length (matchKey ys k).snd < Nat.succ (length ys)
⊢ x ∈ map Prod.fst (groupByKey (matchKey xs k).snd)
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof 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
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof state after:
no goals
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof state after:
no goals
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof state after:
no goals
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof 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)
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof 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)
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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]
Proof 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
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof state after:
no goals
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof state after:
no goals
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof 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)
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof 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)
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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)
Proof 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)
Theorem: List.mem_fsts_of_mem_fsts_groupByKey
Proof 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
Proof state after:
no goals
Theorem: List.groupByKey_fsts_no_duplicates
Proof 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
Proof state after:
no goals
Theorem: List.mem_map
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
⊢ b ∈ map f (x :: xs) ↔ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
have ih := @mem_map α β f b xs
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) ↔ ∃ a, a ∈ x :: xs ∧ f a = b
Theorem: List.mem_map
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) ↔ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) → ∃ a, a ∈ x :: xs ∧ f a = b

case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)
Theorem: List.mem_map
Proof state before:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) → ∃ a, a ∈ x :: xs ∧ f a = b

case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)
Tactic:
. intro h
  cases h with
  | head =>
    exact Exists.intro x (And.intro (List.Mem.head _) rfl)
  | tail x h' =>
    have ih_val := ih.mp h'
    cases ih_val with | intro a ha =>
    exact Exists.intro a (And.intro (Mem.tail _ ha.left) ha.right)
Proof state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)
Theorem: List.mem_map
Proof state before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)
Tactic:
. intro h
  cases h with | intro a ha =>
  simp only [map]
  cases ha.left with
  | head => rw [ha.right]; constructor
  | tail x h' =>
    have h_in_tail := ih.mpr (Exists.intro a ⟨h', ha.right⟩)
    exact Mem.tail _ h_in_tail
Proof state after:
no goals
Theorem: List.mem_map
Proof state before:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) → ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h : b ∈ map f (x :: xs)
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Theorem: List.mem_map
Proof state before:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h : b ∈ map f (x :: xs)
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
cases h with
| head =>
  exact Exists.intro x (And.intro (List.Mem.head _) rfl)
| tail x h' =>
  have ih_val := ih.mp h'
  cases ih_val with | intro a ha =>
  exact Exists.intro a (And.intro (Mem.tail _ ha.left) ha.right)
Proof state after:
no goals
Theorem: List.mem_map
Proof state before:
case mp.head
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : f x ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = f x
⊢ ∃ a, a ∈ x :: xs ∧ f a = f x
Tactic:
exact Exists.intro x (And.intro (List.Mem.head _) rfl)
Proof state after:
no goals
Theorem: List.mem_map
Proof state before:
case mp.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h' : Mem b (map f xs)
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
have ih_val := ih.mp h'
Proof state after:
case mp.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h' : Mem b (map f xs)
ih_val : ∃ a, a ∈ xs ∧ f a = b
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Theorem: List.mem_map
Proof state before:
case mp.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h' : Mem b (map f xs)
ih_val : ∃ a, a ∈ xs ∧ f a = b
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
cases ih_val with | intro a ha =>
exact Exists.intro a (And.intro (Mem.tail _ ha.left) ha.right)
Proof state after:
no goals