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

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : kv.fst = k
⊢ (matchKey (kv :: kvs) k).snd <+ kv :: kvs
Tactic:
simp only [matchKey, h, ite_true]
State after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : kv.fst = k
⊢ (matchKey kvs k).snd <+ kv :: kvs

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : kv.fst = k
⊢ (matchKey kvs k).snd <+ kv :: kvs
Tactic:
exact Sublist.cons _ _ _ ih
State after:
no goals

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : ¬kv.fst = k
⊢ (matchKey (kv :: kvs) k).snd <+ kv :: kvs
Tactic:
simp only [matchKey, h, ite_true]
State after:
κ : 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

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