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

State before:
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
⊢ ∀ (xs : List (κ × ν)) (k : κ), (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
Tactic:
intros xs k
State after:
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)

State before:
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
Tactic:
induction xs with
| nil => rfl
| cons x xs ih =>
  simp only [matchKey]
  cases inst x.1 k with
  | isFalse hfalse =>
    simp only [hfalse, ite_false, ih, filter]
    exact rfl
  | isTrue htrue =>
    simp [htrue, ite_true, filter, ih, map]
State after:
no goals

State before:
case nil
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
⊢ (matchKey [] k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) [])
Tactic:
rfl
State after:
no goals

State before:
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
⊢ (matchKey (x :: xs) k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
Tactic:
simp only [matchKey]
State after:
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
⊢ (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 =
    map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))

State before:
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
⊢ (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 =
    map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
Tactic:
cases inst x.1 k with
| isFalse hfalse =>
  simp only [hfalse, ite_false, ih, filter]
  exact rfl
| isTrue htrue =>
  simp [htrue, ite_true, filter, ih, map]
State after:
no goals

State before:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
hfalse : ¬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)).fst =
    map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
Tactic:
simp only [hfalse, ite_false, ih, filter]
State after:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
hfalse : ¬x.fst = k
⊢ map Prod.snd (filter (fun x => decide (x.fst = k)) xs) =
    map Prod.snd
      (match decide False with
      | true => x :: filter (fun x => decide (x.fst = k)) xs
      | false => filter (fun x => decide (x.fst = k)) xs)

State before:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
hfalse : ¬x.fst = k
⊢ map Prod.snd (filter (fun x => decide (x.fst = k)) xs) =
    map Prod.snd
      (match decide False with
      | true => x :: filter (fun x => decide (x.fst = k)) xs
      | false => filter (fun x => decide (x.fst = k)) xs)
Tactic:
exact rfl
State after:
no goals

State before:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
htrue : 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)).fst =
    map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
Tactic:
simp [htrue, ite_true, filter, ih, map]
State after:
no goals