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

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
⊢ ∀ (k : κ) (xs ys : List (κ × ν)), xs <+ ys → (matchKey xs k).snd <+ (matchKey ys k).snd
Tactic:
intro k xs ys h
State after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
h : xs <+ ys
⊢ (matchKey xs k).snd <+ (matchKey ys k).snd

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
h : xs <+ ys
⊢ (matchKey xs k).snd <+ (matchKey ys k).snd
Tactic:
induction h with
| nil => constructor
| cons xs' ys' x' h' ih =>
  simp only [matchKey]
  cases Decidable.em (x'.fst = k) with
  | inl heq => simp only [heq, ite_true]; apply ih
  | inr hneq => simp only [hneq, ite_false]; apply Sublist.cons _ _ _ ih
| cons2 xs' ys' x' h' ih =>
  simp only [matchKey]
  cases Decidable.em (x'.fst = k) with
  | inl heq => simp only [heq, ite_true]; assumption
  | inr hneq =>
    simp only [hneq, ite_false]
    apply Sublist.cons2 _ _ _ ih
State after:
no goals

State before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
⊢ (matchKey [] k).snd <+ (matchKey [] k).snd
Tactic:
constructor
State after:
no goals

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (matchKey xs' k).snd <+ (matchKey (x' :: ys') k).snd
Tactic:
simp only [matchKey]
State after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (matchKey xs' k).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (matchKey xs' k).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
cases Decidable.em (x'.fst = k) with
| inl heq => simp only [heq, ite_true]; apply ih
| inr hneq => simp only [hneq, ite_false]; apply Sublist.cons _ _ _ ih
State after:
no goals

State before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
simp only [heq, ite_true]
State after:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+ (matchKey ys' k).snd

State before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+ (matchKey ys' k).snd
Tactic:
apply ih
State after:
no goals

State before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (matchKey xs' k).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
simp only [hneq, ite_false]
State after:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (matchKey xs' k).snd <+ (x'.fst, x'.snd) :: (matchKey ys' k).snd

State before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (matchKey xs' k).snd <+ (x'.fst, x'.snd) :: (matchKey ys' k).snd
Tactic:
apply Sublist.cons _ _ _ ih
State after:
no goals

State before:
case cons2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (matchKey (x' :: xs') k).snd <+ (matchKey (x' :: ys') k).snd
Tactic:
simp only [matchKey]
State after:
case cons2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (if x'.fst = k then (x'.snd :: (matchKey xs' k).fst, (matchKey xs' k).snd)
      else ((matchKey xs' k).fst, (x'.fst, x'.snd) :: (matchKey xs' k).snd)).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd

State before:
case cons2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (if x'.fst = k then (x'.snd :: (matchKey xs' k).fst, (matchKey xs' k).snd)
      else ((matchKey xs' k).fst, (x'.fst, x'.snd) :: (matchKey xs' k).snd)).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
cases Decidable.em (x'.fst = k) with
| inl heq => simp only [heq, ite_true]; assumption
| inr hneq =>
  simp only [hneq, ite_false]
  apply Sublist.cons2 _ _ _ ih
State after:
no goals

State before:
case cons2.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (if x'.fst = k then (x'.snd :: (matchKey xs' k).fst, (matchKey xs' k).snd)
      else ((matchKey xs' k).fst, (x'.fst, x'.snd) :: (matchKey xs' k).snd)).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
simp only [heq, ite_true]
State after:
case cons2.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+ (matchKey ys' k).snd

State before:
case cons2.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
heq : x'.fst = k
⊢ (matchKey xs' k).snd <+ (matchKey ys' k).snd
Tactic:
assumption
State after:
no goals

State before:
case cons2.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (if x'.fst = k then (x'.snd :: (matchKey xs' k).fst, (matchKey xs' k).snd)
      else ((matchKey xs' k).fst, (x'.fst, x'.snd) :: (matchKey xs' k).snd)).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd
Tactic:
simp only [hneq, ite_false]
State after:
case cons2.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (x'.fst, x'.snd) :: (matchKey xs' k).snd <+ (x'.fst, x'.snd) :: (matchKey ys' k).snd

State before:
case cons2.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
hneq : ¬x'.fst = k
⊢ (x'.fst, x'.snd) :: (matchKey xs' k).snd <+ (x'.fst, x'.snd) :: (matchKey ys' k).snd
Tactic:
apply Sublist.cons2 _ _ _ ih
State after:
no goals