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

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]
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

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
State after:
no goals

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]
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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)

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]
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

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
State after:
no goals

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]
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

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
State after:
no goals

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
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)

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
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)

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'
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)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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 (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 (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 (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 (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 (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')
b✝ : κ
as✝ : List κ
htail✝ : Mem x as✝
h✝¹ : map Prod.fst ((k', v) :: ys) = b✝ :: as✝
head_eq✝ : (k', v).fst = b✝
tail_eq✝ : map Prod.fst ys = as✝
htail : Mem x (map Prod.fst ys)
h✝ : HEq hx (_ : Mem x ((k', v).fst :: 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
    { fst := ys, snd := { fst := x, snd := { fst := htail, snd := k } } }
    { fst := (k', v) :: ys, snd := { fst := x, snd := { fst := hx, snd := k } } }
Tactic:
assumption
State after:
no goals