Theorem: List.mem_fst_matchKey_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 (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
Proof state after:
no goals