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

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kvs : List (κ × ν)
⊢ ¬k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
intro hneg
State after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kvs : List (κ × ν)
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ False

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kvs : List (κ × ν)
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ False
Tactic:
induction kvs with
| nil => cases hneg
| cons kv kvs ih =>
  apply ih
  simp only [matchKey] at hneg
  cases Decidable.em (kv.fst = k) with
  | inl heq =>
    simp only [heq, ite_true] at hneg
    assumption
  | inr hneq =>
    simp only [hneq, ite_false] at hneg
    simp only [map] at hneg
    cases hneg with
    | head => exact absurd rfl hneq
    | tail _ h => exact h
State after:
no goals

State before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
hneg : k ∈ map Prod.fst (matchKey [] k).snd
⊢ False
Tactic:
cases hneg
State after:
no goals

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg : k ∈ map Prod.fst (matchKey (kv :: kvs) k).snd
⊢ False
Tactic:
apply ih
State after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg : k ∈ map Prod.fst (matchKey (kv :: kvs) k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg : k ∈ map Prod.fst (matchKey (kv :: kvs) k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
simp only [matchKey] at hneg
State after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg :
  k ∈
    map Prod.fst
      (if kv.fst = k 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
⊢ k ∈ map Prod.fst (matchKey kvs k).snd

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg :
  k ∈
    map Prod.fst
      (if kv.fst = k 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
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
cases Decidable.em (kv.fst = k) with
| inl heq =>
  simp only [heq, ite_true] at hneg
  assumption
| inr hneq =>
  simp only [hneq, ite_false] at hneg
  simp only [map] at hneg
  cases hneg with
  | head => exact absurd rfl hneq
  | tail _ h => exact h
State after:
no goals

State before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg :
  k ∈
    map Prod.fst
      (if kv.fst = k 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
heq : kv.fst = k
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
simp only [heq, ite_true] at hneg
State after:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
heq : kv.fst = k
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd

State before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
heq : kv.fst = k
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
assumption
State after:
no goals

State before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg :
  k ∈
    map Prod.fst
      (if kv.fst = k 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
hneq : ¬kv.fst = k
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
simp only [hneq, ite_false] at hneg
State after:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
hneg : k ∈ map Prod.fst ((kv.fst, kv.snd) :: (matchKey kvs k).snd)
⊢ k ∈ map Prod.fst (matchKey kvs k).snd

State before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
hneg : k ∈ map Prod.fst ((kv.fst, kv.snd) :: (matchKey kvs k).snd)
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
simp only [map] at hneg
State after:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
hneg : k ∈ kv.fst :: map Prod.fst (matchKey kvs k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd

State before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
hneg : k ∈ kv.fst :: map Prod.fst (matchKey kvs k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
cases hneg with
| head => exact absurd rfl hneq
| tail _ h => exact h
State after:
no goals

State before:
case cons.inr.head
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
kv : κ × ν
kvs : List (κ × ν)
ih : kv.fst ∈ map Prod.fst (matchKey kvs kv.fst).snd → False
hneq : ¬kv.fst = kv.fst
⊢ kv.fst ∈ map Prod.fst (matchKey kvs kv.fst).snd
Tactic:
exact absurd rfl hneq
State after:
no goals

State before:
case cons.inr.tail
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
h : Mem k (map Prod.fst (matchKey kvs k).snd)
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
exact h
State after:
no goals