internlm/Lean-Github huggingface dataset:
Theorem: List.matchKey_snd_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : ¬kv.fst = k
⊢ (if False then (kv.snd :: (matchKey kvs k).fst, (matchKey kvs k).snd)
      else ((matchKey kvs k).fst, (kv.fst, kv.snd) :: (matchKey kvs k).snd)).snd <+
    kv :: kvs
Tactic:
exact Sublist.cons2 _ _ _ ih
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
⊢ ∀ (k : κ) (xs ys : List (κ × ν)), xs <+ ys → (matchKey xs k).snd <+ (matchKey ys k).snd
Tactic:
intro k xs ys h
Proof state after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
h : xs <+ ys
⊢ (matchKey xs k).snd <+ (matchKey ys k).snd
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
h : xs <+ ys
⊢ (matchKey xs k).snd <+ (matchKey ys k).snd
Tactic:
induction h with
| nil => constructor
| cons xs' ys' x' h' ih =>
  simp only [matchKey]
  cases Decidable.em (x'.fst = k) with
  | inl heq => simp only [heq, ite_true]; apply ih
  | inr hneq => simp only [hneq, ite_false]; apply Sublist.cons _ _ _ ih
| cons2 xs' ys' x' h' ih =>
  simp only [matchKey]
  cases Decidable.em (x'.fst = k) with
  | inl heq => simp only [heq, ite_true]; assumption
  | inr hneq =>
    simp only [hneq, ite_false]
    apply Sublist.cons2 _ _ _ ih
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
⊢ (matchKey [] k).snd <+ (matchKey [] k).snd
Tactic:
constructor
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (matchKey xs' k).snd <+ (matchKey (x' :: ys') k).snd
Tactic:
simp only [matchKey]
Proof state after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (matchKey xs' k).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (matchKey xs' k).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
cases Decidable.em (x'.fst = k) with
| inl heq => simp only [heq, ite_true]; apply ih
| inr hneq => simp only [hneq, ite_false]; apply Sublist.cons _ _ _ ih
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
simp only [heq, ite_true]
Proof state after:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+ (matchKey ys' k).snd
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+ (matchKey ys' k).snd
Tactic:
apply ih
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (matchKey xs' k).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
simp only [hneq, ite_false]
Proof state after:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (matchKey xs' k).snd <+ (x'.fst, x'.snd) :: (matchKey ys' k).snd
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (matchKey xs' k).snd <+ (x'.fst, x'.snd) :: (matchKey ys' k).snd
Tactic:
apply Sublist.cons _ _ _ ih
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (matchKey (x' :: xs') k).snd <+ (matchKey (x' :: ys') k).snd
Tactic:
simp only [matchKey]
Proof state after:
case cons2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (if x'.fst = k then (x'.snd :: (matchKey xs' k).fst, (matchKey xs' k).snd)
      else ((matchKey xs' k).fst, (x'.fst, x'.snd) :: (matchKey xs' k).snd)).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (if x'.fst = k then (x'.snd :: (matchKey xs' k).fst, (matchKey xs' k).snd)
      else ((matchKey xs' k).fst, (x'.fst, x'.snd) :: (matchKey xs' k).snd)).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
cases Decidable.em (x'.fst = k) with
| inl heq => simp only [heq, ite_true]; assumption
| inr hneq =>
  simp only [hneq, ite_false]
  apply Sublist.cons2 _ _ _ ih
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons2.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (if x'.fst = k then (x'.snd :: (matchKey xs' k).fst, (matchKey xs' k).snd)
      else ((matchKey xs' k).fst, (x'.fst, x'.snd) :: (matchKey xs' k).snd)).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
simp only [heq, ite_true]
Proof state after:
case cons2.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+ (matchKey ys' k).snd
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons2.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+ (matchKey ys' k).snd
Tactic:
assumption
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons2.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (if x'.fst = k then (x'.snd :: (matchKey xs' k).fst, (matchKey xs' k).snd)
      else ((matchKey xs' k).fst, (x'.fst, x'.snd) :: (matchKey xs' k).snd)).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
simp only [hneq, ite_false]
Proof state after:
case cons2.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (x'.fst, x'.snd) :: (matchKey xs' k).snd <+ (x'.fst, x'.snd) :: (matchKey ys' k).snd
Theorem: List.matchKey_snd_sublist_of_sublist
Proof state before:
case cons2.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (x'.fst, x'.snd) :: (matchKey xs' k).snd <+ (x'.fst, x'.snd) :: (matchKey ys' k).snd
Tactic:
apply Sublist.cons2 _ _ _ ih
Proof state after:
no goals
Theorem: List.fst_groupByKey_sublist
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 → map Prod.fst (groupByKey y) <+ map Prod.fst y
k : κ
v : ν
xs : List (κ × ν)
x✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y ((k, v) :: xs) →
      map Prod.fst (groupByKey y) <+ 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
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)
⊢ x ∈ map Prod.fst (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
      (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_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)
⊢ x ∈
    map Prod.fst
      (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_matchKey_key_or_snd this k
  cases ih with
  | inl => contradiction
  | inr hmem => exact hmem
| inr hkneq =>
  simp only [hkneq, ite_false]
  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_matchKey_key_or_snd this k'
    cases ih with
    | inl => contradiction
    | inr => assumption
Proof state after:
no goals
Theorem: List.mem_fst_matchKey_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
      (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 (matchKey ys k).snd
Theorem: List.mem_fst_matchKey_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 (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 (matchKey ys k).snd
Theorem: List.mem_fst_matchKey_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 (matchKey ys k).snd
Tactic:
have ih := mem_fst_matchKey_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 (matchKey ys k).snd
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Theorem: List.mem_fst_matchKey_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 (matchKey ys k).snd
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Tactic:
cases ih with
| inl => contradiction
| inr hmem => exact hmem
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)
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_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)
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_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)
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_matchKey_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 (matchKey ys k).snd
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_fst_matchKey_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 (matchKey ys k).snd
⊢ x ∈ map Prod.fst (matchKey ys k).snd
Tactic:
exact hmem
Proof state after:
no goals
Theorem: List.mem_fst_matchKey_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
      (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 ((k', v) :: (matchKey ys k).snd)
Theorem: List.mem_fst_matchKey_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 ys 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 (matchKey ys k).snd
Theorem: List.mem_fst_matchKey_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 (matchKey ys 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_matchKey_key_or_snd this k'
  cases ih with
  | inl => contradiction
  | inr => assumption
Proof state after:
no goals
Theorem: List.mem_fst_matchKey_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 (matchKey ys 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 (matchKey ys k).snd
Theorem: List.mem_fst_matchKey_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 (matchKey ys k).snd
Tactic:
apply Mem.head
Proof state after:
no goals
Theorem: List.mem_fst_matchKey_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 (matchKey ys 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 (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'
⊢ Mem x (map Prod.fst (matchKey ys 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 (matchKey ys k).snd)