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

State before:
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
⊢ ∀ (xs : List (κ × ν)) (k : κ), length (matchKey xs k).fst + 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).fst + length (matchKey xs k).snd = length xs

State before:
case nil
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
⊢ length (matchKey [] k).fst + length (matchKey [] k).snd = length []
Tactic:
rfl
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).fst + length (matchKey xs k).snd = length xs
⊢ length (matchKey (x :: xs) k).fst + 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).fst + 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)).fst +
      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.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
hfalse : ¬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)).fst +
      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 [hfalse, ite_false, List.length]
State after:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
hfalse : ¬x.fst = k
⊢ length (matchKey xs k).fst + (length (matchKey xs k).snd + 1) = length xs + 1

State before:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
hfalse : ¬x.fst = k
⊢ length (matchKey xs k).fst + (length (matchKey xs k).snd + 1) = length xs + 1
Tactic:
rw [←Nat.add_assoc]
State after:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
hfalse : ¬x.fst = k
⊢ length (matchKey xs k).fst + length (matchKey xs k).snd + 1 = length xs + 1

State before:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : 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)).fst +
      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 [htrue, ite_true, List.length]
State after:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : x.fst = k
⊢ length (matchKey xs k).fst + 1 + length (matchKey xs k).snd = length xs + 1

State before:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : x.fst = k
⊢ length (matchKey xs k).fst + 1 + length (matchKey xs k).snd = length xs + 1
Tactic:
rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
State after:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : x.fst = k
⊢ length (matchKey xs k).fst + length (matchKey xs k).snd + 1 = length xs + 1