Theorem: List.all_in_map_fst_groupByKey_of_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
_x✝ : (xs : List (κ × ν)) ×' (ys : List (κ × ν)) ×' (_ : xs <+ ys) ×' (x : κ) ×' x ∈ map Prod.fst (groupByKey xs)
a✝⁵ :
  ∀ (y : (xs : List (κ × ν)) ×' (ys : List (κ × ν)) ×' (_ : xs <+ ys) ×' (x : κ) ×' x ∈ map Prod.fst (groupByKey xs)),
    (invImage
            (fun a =>
              PSigma.casesOn a fun xs snd =>
                PSigma.casesOn snd fun ys snd =>
                  PSigma.casesOn snd fun hsubl snd => PSigma.casesOn snd fun x snd => length ys)
            instWellFoundedRelation).1
        y _x✝ →
      y.2.2.2.1 ∈ map Prod.fst (groupByKey y.2.1)
xs✝ : List (κ × ν)
ys✝¹ : (ys : List (κ × ν)) ×' (_ : xs✝ <+ ys) ×' (x : κ) ×' x ∈ map Prod.fst (groupByKey xs✝)
a✝⁴ :
  ∀ (y : (xs : List (κ × ν)) ×' (ys : List (κ × ν)) ×' (_ : xs <+ ys) ×' (x : κ) ×' x ∈ map Prod.fst (groupByKey xs)),
    (invImage
            (fun a =>
              PSigma.casesOn a fun xs snd =>
                PSigma.casesOn snd fun ys snd =>
                  PSigma.casesOn snd fun hsubl snd => PSigma.casesOn snd fun x snd => length ys)
            instWellFoundedRelation).1
        y { fst := xs✝, snd := ys✝¹ } →
      y.2.2.2.1 ∈ map Prod.fst (groupByKey y.2.1)
ys✝ : List (κ × ν)
x✝⁶ : (_ : xs✝ <+ ys✝) ×' (x : κ) ×' x ∈ map Prod.fst (groupByKey xs✝)
a✝³ :
  ∀ (y : (xs : List (κ × ν)) ×' (ys : List (κ × ν)) ×' (_ : xs <+ ys) ×' (x : κ) ×' x ∈ map Prod.fst (groupByKey xs)),
    (invImage
            (fun a =>
              PSigma.casesOn a fun xs snd =>
                PSigma.casesOn snd fun ys snd =>
                  PSigma.casesOn snd fun hsubl snd => PSigma.casesOn snd fun x snd => length ys)
            instWellFoundedRelation).1
        y { fst := xs✝, snd := { fst := ys✝, snd := x✝⁶ } } →
      y.2.2.2.1 ∈ map Prod.fst (groupByKey y.2.1)
x✝⁵ : xs✝ <+ ys✝
x✝⁴ : (x : κ) ×' x ∈ map Prod.fst (groupByKey xs✝)
a✝² :
  ∀ (y : (xs : List (κ × ν)) ×' (ys : List (κ × ν)) ×' (_ : xs <+ ys) ×' (x : κ) ×' x ∈ map Prod.fst (groupByKey xs)),
    (invImage
            (fun a =>
              PSigma.casesOn a fun xs snd =>
                PSigma.casesOn snd fun ys snd =>
                  PSigma.casesOn snd fun hsubl snd => PSigma.casesOn snd fun x snd => length ys)
            instWellFoundedRelation).1
        y { fst := xs✝, snd := { fst := ys✝, snd := { fst := x✝⁵, snd := x✝⁴ } } } →
      y.2.2.2.1 ∈ map Prod.fst (groupByKey y.2.1)
x✝³ : κ
x✝² : x✝³ ∈ map Prod.fst (groupByKey xs✝)
a✝¹ :
  ∀ (y : (xs : List (κ × ν)) ×' (ys : List (κ × ν)) ×' (_ : xs <+ ys) ×' (x : κ) ×' x ∈ map Prod.fst (groupByKey xs)),
    (invImage
            (fun a =>
              PSigma.casesOn a fun xs snd =>
                PSigma.casesOn snd fun ys snd =>
                  PSigma.casesOn snd fun hsubl snd => PSigma.casesOn snd fun x snd => length ys)
            instWellFoundedRelation).1
        y { fst := xs✝, snd := { fst := ys✝, snd := { fst := x✝⁵, snd := { fst := x✝³, snd := x✝² } } } } →
      y.2.2.2.1 ∈ map Prod.fst (groupByKey y.2.1)
xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x✝¹ : κ
hx : x✝¹ ∈ map Prod.fst (groupByKey ((k, v) :: xs))
x✝ :
  ∀ (y : (xs : List (κ × ν)) ×' (ys : List (κ × ν)) ×' (_ : xs <+ ys) ×' (x : κ) ×' x ∈ map Prod.fst (groupByKey xs)),
    (invImage
            (fun a =>
              PSigma.casesOn a fun xs snd =>
                PSigma.casesOn snd fun ys snd =>
                  PSigma.casesOn snd fun hsubl snd => PSigma.casesOn snd fun x snd => length ys)
            instWellFoundedRelation).1
        y
        { fst := (k, v) :: xs,
          snd :=
            { fst := (k, v) :: ys,
              snd := { fst := (_ : (k, v) :: xs <+ (k, v) :: ys), snd := { fst := x✝¹, snd := hx } } } } →
      y.2.2.2.1 ∈ map Prod.fst (groupByKey y.2.1)
b✝ : κ
as✝ : List κ
htail✝ : Mem x✝¹ as✝
h✝¹ : k :: map Prod.fst (groupByKey (matchKey xs k).snd) = b✝ :: as✝
head_eq✝ : k = b✝
tail_eq✝ : map Prod.fst (groupByKey (matchKey xs k).snd) = as✝
htail : Mem x✝¹ (map Prod.fst (groupByKey (matchKey xs k).snd))
h✝ :
  HEq
    (_ :
      x✝¹ ∈
        map Prod.fst
          (let_fun h_help := (_ : length (matchKey xs k).snd < Nat.succ (length xs));
          let fms := matchKey xs k;
          (k, v :: fms.fst) :: groupByKey fms.snd))
    (_ : Mem x✝¹ (k :: map Prod.fst (groupByKey (matchKey xs k).snd)))
this : (matchKey xs k).snd <+ (matchKey ys k).snd
hterm : length (matchKey ys k).snd < Nat.succ (length ys)
x : κ
a✝ : x ∈ map Prod.fst (groupByKey (matchKey xs k).snd)
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun xs snd =>
            PSigma.casesOn snd fun ys snd =>
              PSigma.casesOn snd fun hsubl snd => PSigma.casesOn snd fun x snd => length ys)
        instWellFoundedRelation).1
    { fst := (matchKey xs k).snd,
      snd := { fst := (matchKey ys k).snd, snd := { fst := this, snd := { fst := x, snd := a✝ } } } }
    { fst := (k, v) :: xs,
      snd :=
        { fst := (k, v) :: ys,
          snd := { fst := (_ : (k, v) :: xs <+ (k, v) :: ys), snd := { fst := x✝¹, snd := hx } } } }
Tactic:
assumption
Proof state after:
no goals