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

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
⊢ ∀ (xs : List (κ × ν)) (k : κ), length (matchKey xs k).snd ≤ length xs
Tactic:
intros xs k
State after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ length (matchKey xs k).snd ≤ length xs

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ length (matchKey xs k).snd ≤ length xs
Tactic:
induction xs with
| nil => exact Nat.le.refl
| cons x xs ih =>
  simp only [matchKey]
  apply @Decidable.byCases (x.1=k) _
  . intros heq
    simp only [heq]
    rw [ite_true]
    simp only [Prod.snd]
    apply Nat.le_step
    exact ih
  . intros hneq
    simp only [hneq]
    rw [ite_false]
    simp only [Prod.fst]
    apply Nat.succ_le_succ
    exact ih
State after:
no goals

State before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
⊢ length (matchKey [] k).snd ≤ length []
Tactic:
exact Nat.le.refl
State after:
no goals

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ length (matchKey (x :: xs) k).snd ≤ length (x :: xs)
Tactic:
simp only [matchKey]
State after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ length
      (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 ≤
    length (x :: xs)

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ length
      (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 ≤
    length (x :: xs)
Tactic:
apply @Decidable.byCases (x.1=k) _
State after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ x.fst = k →
    length
        (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 ≤
      length (x :: xs)

case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (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 ≤
      length (x :: xs)

State before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ x.fst = k →
    length
        (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 ≤
      length (x :: xs)

case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (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 ≤
      length (x :: xs)
Tactic:
. intros heq
  simp only [heq]
  rw [ite_true]
  simp only [Prod.snd]
  apply Nat.le_step
  exact ih
State after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (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 ≤
      length (x :: xs)

State before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (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 ≤
      length (x :: xs)
Tactic:
. intros hneq
  simp only [hneq]
  rw [ite_false]
  simp only [Prod.fst]
  apply Nat.succ_le_succ
  exact ih
State after:
no goals

State before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ x.fst = k →
    length
        (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 ≤
      length (x :: xs)
Tactic:
intros heq
State after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length
      (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 ≤
    length (x :: xs)

State before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length
      (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 ≤
    length (x :: xs)
Tactic:
simp only [heq]
State after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length
      (if True then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
        else ((matchKey xs k).fst, (k, x.snd) :: (matchKey xs k).snd)).snd ≤
    length (x :: xs)

State before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length
      (if True then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
        else ((matchKey xs k).fst, (k, x.snd) :: (matchKey xs k).snd)).snd ≤
    length (x :: xs)
Tactic:
rw [ite_true]
State after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd).snd ≤ length (x :: xs)

State before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd).snd ≤ length (x :: xs)
Tactic:
simp only [Prod.snd]
State after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (matchKey xs k).snd ≤ length (x :: xs)

State before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (matchKey xs k).snd ≤ length (x :: xs)
Tactic:
apply Nat.le_step
State after:
case cons.h1.h
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (matchKey xs k).snd ≤ length xs

State before:
case cons.h1.h
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (matchKey xs k).snd ≤ length xs
Tactic:
exact ih
State after:
no goals

State before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (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 ≤
      length (x :: xs)
Tactic:
intros hneq
State after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length
      (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 ≤
    length (x :: xs)

State before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length
      (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 ≤
    length (x :: xs)
Tactic:
simp only [hneq]
State after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length
      (if False 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 ≤
    length (x :: xs)

State before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length
      (if False 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 ≤
    length (x :: xs)
Tactic:
rw [ite_false]
State after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd).snd ≤ length (x :: xs)

State before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd).snd ≤ length (x :: xs)
Tactic:
simp only [Prod.fst]
State after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length ((x.fst, x.snd) :: (matchKey xs k).snd) ≤ length (x :: xs)

State before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length ((x.fst, x.snd) :: (matchKey xs k).snd) ≤ length (x :: xs)
Tactic:
apply Nat.succ_le_succ
State after:
case cons.h2.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length (matchKey xs k).snd ≤ length xs

State before:
case cons.h2.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length (matchKey xs k).snd ≤ length xs
Tactic:
exact ih
State after:
no goals