internlm/Lean-Github huggingface dataset:
Theorem: List.mem_fst_matchKey_key_or_snd
Proof state before:
case inr.inr.a
κ : 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
⊢ Mem x (map Prod.fst (matchKey ys k).snd)
Tactic:
have ih := mem_fst_matchKey_key_or_snd this k'
Proof state after:
case inr.inr.a
κ : 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
ih : x = k' ∨ x ∈ map Prod.fst (matchKey (matchKey ys k).snd k').snd
⊢ Mem x (map Prod.fst (matchKey ys k).snd)
Theorem: List.mem_fst_matchKey_key_or_snd
Proof state before:
case inr.inr.a
κ : 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
ih : x = k' ∨ x ∈ map Prod.fst (matchKey (matchKey ys k).snd k').snd
⊢ Mem x (map Prod.fst (matchKey ys k).snd)
Tactic:
cases ih with
| inl => contradiction
| inr => assumption
Proof state after:
no goals
Theorem: List.mem_fst_matchKey_key_or_snd
Proof state before:
κ : 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'
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Tactic:
cases hx with
| head => contradiction
| tail _ htail =>
  have := mem_fst_matchKey_key_or_snd htail k
  cases this with
  | inl => contradiction
  | inr => assumption
Proof state after:
no goals
Theorem: List.mem_fst_matchKey_key_or_snd
Proof state before:
case head
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
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
h : ¬(k', v).fst = k
hxneq : ¬(k', v).fst = k'
⊢ (k', v).fst ∈ map Prod.fst (matchKey ys k).snd
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_fst_matchKey_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)
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Tactic:
have := mem_fst_matchKey_key_or_snd htail k
Proof state after:
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
Theorem: List.mem_fst_matchKey_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_matchKey_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_matchKey_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_matchKey_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 (matchKey ys k).snd)
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_fst_matchKey_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 (matchKey (matchKey ys k).snd k').snd
⊢ Mem 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:
κ : 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)
⊢ x ∈ map Prod.fst (groupByKey (matchKey ((k', v) :: ys) k).snd)
Tactic:
simp only [matchKey]
Proof state after:
κ : 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)
⊢ x ∈
    map Prod.fst
      (groupByKey
        (if k' = k then (v :: (matchKey ys k).fst, (matchKey ys k).snd)
          else ((matchKey ys k).fst, (k', v) :: (matchKey ys k).snd)).snd)
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
κ : 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)
⊢ x ∈
    map Prod.fst
      (groupByKey
        (if k' = k then (v :: (matchKey ys k).fst, (matchKey ys k).snd)
          else ((matchKey ys k).fst, (k', v) :: (matchKey ys k).snd)).snd)
Tactic:
cases Decidable.em (k' = k) with
| inl hkeq =>
  simp only [hkeq, ite_true]
  have : x ∈ map Prod.fst ys := by
    cases hx with
    | head => contradiction
    | tail => assumption
  have ih := mem_fst_groupByKey_key_or_snd this k
  cases ih with
  | inl => contradiction
  | inr hmem => exact hmem
| inr hkneq =>
  simp only [hkneq, ite_false]
  simp only [groupByKey]
  simp only [map]
  cases Decidable.em (x = k') with
  | inl hxeq => rw [hxeq]; apply Mem.head
  | inr hxneq =>
    apply Mem.tail
    have : x ∈ map Prod.fst (matchKey ys k).snd := by
      cases hx with
      | head => contradiction
      | tail _ htail =>
        have := mem_fst_matchKey_key_or_snd htail k
        cases this with
        | inl => contradiction
        | inr => assumption
    have ih := mem_fst_groupByKey_key_or_snd this k'
    cases ih with
    | inl => contradiction
    | inr => assumption
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case 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)
hkeq : k' = k
⊢ x ∈
    map Prod.fst
      (groupByKey
        (if k' = k then (v :: (matchKey ys k).fst, (matchKey ys k).snd)
          else ((matchKey ys k).fst, (k', v) :: (matchKey ys k).snd)).snd)
Tactic:
simp only [hkeq, ite_true]
Proof state after:
case 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)
hkeq : k' = k
⊢ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case 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)
hkeq : k' = k
⊢ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
have : x ∈ map Prod.fst ys := by
  cases hx with
  | head => contradiction
  | tail => assumption
Proof state after:
case 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)
hkeq : k' = k
this : x ∈ map Prod.fst ys
⊢ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case 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)
hkeq : k' = k
this : x ∈ map Prod.fst ys
⊢ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
have ih := mem_fst_groupByKey_key_or_snd this k
Proof state after:
case 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)
hkeq : k' = k
this : x ∈ map Prod.fst ys
ih : x = k ∨ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
⊢ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case 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)
hkeq : k' = k
this : x ∈ map Prod.fst ys
ih : x = k ∨ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
⊢ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
cases ih with
| inl => contradiction
| inr hmem => exact hmem
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
κ : 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)
hkeq : k' = k
⊢ x ∈ map Prod.fst ys
Tactic:
cases hx with
| head => contradiction
| tail => assumption
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case head
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
k k' : κ
v : ν
ys : List (κ × ν)
h_term : length (matchKey ys k).snd < Nat.succ (length ys)
h_term' : length ys < Nat.succ (length ys)
hkeq : k' = k
h : ¬(k', v).fst = k
⊢ (k', v).fst ∈ map Prod.fst ys
Tactic:
contradiction
Proof state after:
no goals
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)
hkeq : k' = k
a✝ : Mem x (map Prod.fst ys)
⊢ x ∈ map Prod.fst ys
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inl.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)
hkeq : k' = k
this : x ∈ map Prod.fst ys
h✝ : x = k
⊢ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inl.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)
hkeq : k' = k
this : x ∈ map Prod.fst ys
hmem : x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
⊢ x ∈ map Prod.fst (groupByKey (matchKey ys k).snd)
Tactic:
exact hmem
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case 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
⊢ x ∈
    map Prod.fst
      (groupByKey
        (if k' = k then (v :: (matchKey ys k).fst, (matchKey ys k).snd)
          else ((matchKey ys k).fst, (k', v) :: (matchKey ys k).snd)).snd)
Tactic:
simp only [hkneq, ite_false]
Proof state after:
case 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
⊢ x ∈ map Prod.fst (groupByKey ((k', v) :: (matchKey ys k).snd))
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case 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
⊢ x ∈ map Prod.fst (groupByKey ((k', v) :: (matchKey ys k).snd))
Tactic:
simp only [groupByKey]
Proof state after:
case 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
⊢ x ∈
    map Prod.fst ((k', v :: (matchKey (matchKey ys k).snd k').fst) :: groupByKey (matchKey (matchKey ys k).snd k').snd)
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case 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
⊢ x ∈
    map Prod.fst ((k', v :: (matchKey (matchKey ys k).snd k').fst) :: groupByKey (matchKey (matchKey ys k).snd k').snd)
Tactic:
simp only [map]
Proof state after:
case 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
⊢ x ∈ k' :: map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd)
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case 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
⊢ x ∈ k' :: map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd)
Tactic:
cases Decidable.em (x = k') with
| inl hxeq => rw [hxeq]; apply Mem.head
| inr hxneq =>
  apply Mem.tail
  have : x ∈ map Prod.fst (matchKey ys k).snd := by
    cases hx with
    | head => contradiction
    | tail _ htail =>
      have := mem_fst_matchKey_key_or_snd htail k
      cases this with
      | inl => contradiction
      | inr => assumption
  have ih := mem_fst_groupByKey_key_or_snd this k'
  cases ih with
  | inl => contradiction
  | inr => assumption
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inr.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
hxeq : x = k'
⊢ x ∈ k' :: map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd)
Tactic:
rw [hxeq]
Proof state after:
case inr.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
hxeq : x = k'
⊢ k' ∈ k' :: map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd)
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inr.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
hxeq : x = k'
⊢ k' ∈ k' :: map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd)
Tactic:
apply Mem.head
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inr.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'
⊢ x ∈ k' :: map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd)
Tactic:
apply Mem.tail
Proof state after:
case inr.inr.a
κ : 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'
⊢ Mem x (map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd))
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inr.inr.a
κ : 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'
⊢ Mem x (map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd))
Tactic:
have : x ∈ map Prod.fst (matchKey ys k).snd := by
  cases hx with
  | head => contradiction
  | tail _ htail =>
    have := mem_fst_matchKey_key_or_snd htail k
    cases this with
    | inl => contradiction
    | inr => assumption
Proof state after:
case inr.inr.a
κ : 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
⊢ Mem x (map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd))
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inr.inr.a
κ : 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
⊢ Mem x (map Prod.fst (groupByKey (matchKey (matchKey ys k).snd k').snd))
Tactic:
have ih := mem_fst_groupByKey_key_or_snd this k'
Proof state after:
case inr.inr.a
κ : 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
ih : x = k' ∨ 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))
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case inr.inr.a
κ : 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
ih : x = k' ∨ 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:
cases ih with
| inl => contradiction
| inr => 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 κ
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'
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Tactic:
cases hx with
| head => contradiction
| tail _ htail =>
  have := mem_fst_matchKey_key_or_snd htail k
  cases this with
  | inl => contradiction
  | inr => assumption
Proof state after:
no goals
Theorem: List.mem_fst_groupByKey_key_or_snd
Proof state before:
case head
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
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
h : ¬(k', v).fst = k
hxneq : ¬(k', v).fst = k'
⊢ (k', v).fst ∈ 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
κ : 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)
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Tactic:
have := mem_fst_matchKey_key_or_snd htail k
Proof state after:
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